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  820  xoranor  1397  19.41h  1709  sbimi  1788  equs5e  1819  exdistrfor  1824  equs45f  1826  sbidm  1875  eu3h  2100  eupickb  2136  2exeu  2147  darii  2155  festino  2161  baroco  2162  r19.27v  2634  r19.27av  2642  rspc2ev  2893  reu3  2964  difdif  3299  ssddif  3408  inssdif  3410  difin  3411  difindiss  3428  indifdir  3430  difrab  3448  iundif2ss  3995  trssord  4431  ordsuc  4615  find  4651  imainss  5103  dffun5r  5288  fof  5505  f1ocnv  5542  fv3  5606  relelfvdm  5615  funimass4  5636  fvelimab  5642  funconstss  5705  dff2  5731  dffo5  5736  dff1o6  5852  oprabid  5983  ssoprab2i  6041  uchoice  6230  releldm2  6278  ixpf  6814  recexgt0sr  7893  map2psrprg  7925  lediv2a  8975  lbreu  9025  elfzp12  10228  fihashf1rn  10940  ccatsymb  11066  swrdpfx  11166  pfxpfx  11167  cau3lem  11469  fsumcl2lem  11753  dvdsnegb  12163  dvds2add  12180  dvds2sub  12181  ndvdssub  12285  gcd2n0cl  12334  divgcdcoprmex  12468  cncongr1  12469  ctinfom  12843  qusecsub  13711  istopfin  14516  toponcom  14543  cnptoprest  14755  dvmptfsum  15241  elply2  15251