Theorem anim1i 334

Description: Introduce conjunct to both sides of an implication.

Hypothesis

Ref	Expression
anim1i.1	⊢ (φ → ψ)

Assertion

Ref	Expression
anim1i	⊢ ((φ ⋀ χ) → (ψ ⋀ χ))

Proof of Theorem anim1i

Step	Hyp	Ref	Expression
1		anim1i.1	. 2 ⊢ (φ → ψ)
2		id 59	. 2 ⊢ (χ → χ)
3	1, 2	anim12i 333	1 ⊢ ((φ ⋀ χ) → (ψ ⋀ χ))

Syntax hints:   → wi 3   ⋀ wa 223

This theorem is referenced by:  pm5.61 450  sylanl1 463  sylanr1 465  3anandirs 925  sspr 2489  difex2 2893  mouniss 2906  cores 3515  fun11uni 3581  fabexg 3669  fores 3697  f1o2 3709  f1oabexg 3716  tz6.12-1 3752  ssimaex 3784  exfo 3838  tz7.48lem 3971  tz7.49c 3976  ndmoprass 4064  omass 4227  oewordri 4235  nnaordex 4265  nnawordex 4266  sbthlem9 4474  pssnn 4554  fiint 4575  abfii2 4577  inf1 4624  infeq5 4638  rankuni 4715  ac6s2 4775  brdom5 4819  brdom4 4820  ltexpq 5100  prnmadd 5120  genpnnp 5128  prlem934 5159  prlem936 5175  reclem1pr 5176  reclem2pr 5177  suplem1pr 5181  suppsr2 5243  suppsr3 5244  cnegexlem3 5367  divassOLD 5757  lediv2a 5911  nn2ge 5956  xrsupexmnf 6106  xrinfmexpnf 6107  xrsupsslem 6108  xrinfmsslem 6109  supxrre 6115  supxrun 6117  elnn0nn 6203  btwnz 6250  qnegcl 6272  quoremnn0ALT 6312  iooval2 6334  ioo0 6335  elioo4g 6352  elioc2 6357  elico2 6358  elicc2 6359  elfzlem 6441  elfzp1 6478  expmwordi 6637  expnlbnd2 6687  mulre 6809  faclbnd 6977  faclbnd6 6986  bcval2 6991  climshft2i 7138  iserzshft2i 7139  climmulc2i 7161  climsubc2i 7163  climcmplem 7169  isummulc1iALT 7245  rescncf 7304  abscncflem 7306  mulc1cncf 7311  dfef2i 7339  reeff1olem1 7456  acdc5lem1 7524  infxpidmlem7 7591  infxpidmlem8 7592  infmap2lem1 7612  clscld 7709  islp2 7773  ismsg 7826  blssex 7880  opnin 7895  neibl 7903  lpbl 7906  lmbr 7954  metelcls 7991  metcnp4 7996  bcthlem2 8026  bcthlem14 8038  bcthlem15 8039  bcthlem30 8054  grpidinvlem3 8076  grpidinv 8078  ablmul 8156  isring 8166  nvlmle 8358  sspival 8422  nmobndseqi 8465  ubthlem3 8556  htthlem12 8656  efifolem4 8749  circgrp 8764  axhcompl 8892  hvaddsub4 8969  hhcmpl 9093  hlimcauii 9130  ocsh 9180  chocunii 9196  projlem16 9225  5oalem2 9624  5oalem5 9627  3oalem2 9632  pjjsi 9669  hoadddir 9754  nmopub2tALT 9857  nmfnleub2 9874  nmopcoadji 10058  leopmul 10091  stge1i 10190  hatomistici 10314  mdsymlem2 10356  mdsymlem5 10359  infi 10606  homib 10745

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain