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  823  xoranor  1419  19.41h  1731  sbimi  1810  equs5e  1841  exdistrfor  1846  equs45f  1848  sbidm  1897  eu3h  2123  eupickb  2159  2exeu  2170  darii  2178  festino  2184  baroco  2185  r19.27v  2658  r19.27av  2666  rspc2ev  2922  reu3  2993  difdif  3329  ssddif  3438  inssdif  3440  difin  3441  difindiss  3458  indifdir  3460  difrab  3478  iundif2ss  4031  trssord  4472  ordsuc  4656  find  4692  imainss  5147  dffun5r  5333  fof  5553  f1ocnv  5590  fv3  5655  relelfvdm  5664  funimass4  5689  fvelimab  5695  funconstss  5758  dff2  5784  dffo5  5789  dff1o6  5909  oprabid  6042  ssoprab2i  6102  uchoice  6292  releldm2  6340  ixpf  6880  recexgt0sr  7976  map2psrprg  8008  lediv2a  9058  lbreu  9108  elfzp12  10312  fihashf1rn  11027  ccatsymb  11155  swrdpfx  11260  pfxpfx  11261  pfxccatin12  11286  cau3lem  11646  fsumcl2lem  11930  dvdsnegb  12340  dvds2add  12357  dvds2sub  12358  ndvdssub  12462  gcd2n0cl  12511  divgcdcoprmex  12645  cncongr1  12646  ctinfom  13020  qusecsub  13889  istopfin  14695  toponcom  14722  cnptoprest  14934  dvmptfsum  15420  elply2  15430  uspgr2wlkeqi  16139