Theorem anim2i 342

Description: Introduce conjunct to both sides of an implication. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
anim1i.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
anim2i	⊢ ((𝜒 ∧ 𝜑) → (𝜒 ∧ 𝜓))

Proof of Theorem anim2i

Step	Hyp	Ref	Expression
1		id 19	. 2 ⊢ (𝜒 → 𝜒)
2		anim1i.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	anim12i 338	1 ⊢ ((𝜒 ∧ 𝜑) → (𝜒 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  sylanl2  403  sylanr2  405  andi  826  xoranor  1422  19.41h  1733  sbimi  1813  equs5e  1844  exdistrfor  1849  equs45f  1851  sbidm  1900  eu3h  2128  eupickb  2164  2exeu  2175  darii  2183  festino  2189  baroco  2190  r19.27v  2672  r19.27av  2680  rspc2ev  2938  reu3  3009  difdif  3346  ssddif  3457  inssdif  3459  difin  3460  difindiss  3477  indifdir  3479  difrab  3497  iundif2ss  4059  trssord  4503  ordsuc  4687  find  4723  imainss  5180  dffun5r  5366  fof  5592  f1ocnv  5629  fv3  5695  relelfvdm  5704  funimass4  5729  fvelimab  5735  funconstss  5798  dff2  5823  dffo5  5828  dff1o6  5951  oprabid  6084  ssoprab2i  6144  uchoice  6333  releldm2  6381  ixpf  6957  recexgt0sr  8090  map2psrprg  8122  lediv2a  9171  lbreu  9221  elfzp12  10437  fihashf1rn  11155  ccatsymb  11294  swrdpfx  11403  pfxpfx  11404  pfxccatin12  11429  cau3lem  11803  fsumcl2lem  12088  dvdsnegb  12498  dvds2add  12515  dvds2sub  12516  ndvdssub  12620  gcd2n0cl  12669  divgcdcoprmex  12803  cncongr1  12804  ctinfom  13196  qusecsub  14065  istopfin  14882  toponcom  14909  cnptoprest  15121  dvmptfsum  15607  elply2  15617  subupgr  16285  uspgr2wlkeqi  16379  clwwlknun  16453