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  8093  map2psrprg  8125  lediv2a  9174  lbreu  9224  elfzp12  10440  fihashf1rn  11159  ccatsymb  11298  swrdpfx  11407  pfxpfx  11408  pfxccatin12  11433  cau3lem  11807  fsumcl2lem  12092  dvdsnegb  12502  dvds2add  12519  dvds2sub  12520  ndvdssub  12624  gcd2n0cl  12673  divgcdcoprmex  12807  cncongr1  12808  ctinfom  13200  qusecsub  14069  istopfin  14914  toponcom  14941  cnptoprest  15153  dvmptfsum  15639  elply2  15649  subupgr  16317  uspgr2wlkeqi  16411  clwwlknun  16485