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  407  sylanr2  409  andi  830  xoranor  1426  19.41h  1737  sbimi  1817  equs5e  1848  exdistrfor  1853  equs45f  1855  sbidm  1904  eu3h  2132  eupickb  2168  2exeu  2179  darii  2187  festino  2193  baroco  2194  r19.27v  2678  r19.27av  2686  rspc2ev  2945  reu3  3016  difdif  3354  ssddif  3465  inssdif  3467  difin  3468  difindiss  3485  indifdir  3487  difrab  3507  iundif2ss  4076  trssord  4523  ordsuc  4708  find  4744  imainss  5201  dffun5r  5387  fof  5613  f1ocnv  5650  fv3  5716  relelfvdm  5725  funimass4  5750  fvelimab  5756  funconstss  5821  dff2  5846  dffo5  5851  dff1o6  5976  oprabid  6111  ssoprab2i  6171  uchoice  6365  releldm2  6413  ixpf  6996  recexgt0sr  8134  map2psrprg  8166  lediv2a  9219  lbreu  9269  elfzp12  10489  fihashf1rn  11210  ccatsymb  11353  swrdpfx  11462  pfxpfx  11463  pfxccatin12  11488  cau3lem  11863  fsumcl2lem  12148  dvdsnegb  12558  dvds2add  12575  dvds2sub  12576  ndvdssub  12680  gcd2n0cl  12729  divgcdcoprmex  12863  cncongr1  12864  ballotfilemirc  13258  ctinfom  13302  qusecsub  14118  istopfin  15084  toponcom  15111  cnptoprest  15323  dvmptfsum  15809  elply2  15819  subupgr  16497  uspgr2wlkeqi  16591  clwwlknun  16665