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  822  xoranor  1399  19.41h  1711  sbimi  1790  equs5e  1821  exdistrfor  1826  equs45f  1828  sbidm  1877  eu3h  2103  eupickb  2139  2exeu  2150  darii  2158  festino  2164  baroco  2165  r19.27v  2638  r19.27av  2646  rspc2ev  2902  reu3  2973  difdif  3309  ssddif  3418  inssdif  3420  difin  3421  difindiss  3438  indifdir  3440  difrab  3458  iundif2ss  4010  trssord  4448  ordsuc  4632  find  4668  imainss  5120  dffun5r  5306  fof  5524  f1ocnv  5561  fv3  5626  relelfvdm  5635  funimass4  5657  fvelimab  5663  funconstss  5726  dff2  5752  dffo5  5757  dff1o6  5873  oprabid  6006  ssoprab2i  6064  uchoice  6253  releldm2  6301  ixpf  6837  recexgt0sr  7928  map2psrprg  7960  lediv2a  9010  lbreu  9060  elfzp12  10263  fihashf1rn  10977  ccatsymb  11103  swrdpfx  11205  pfxpfx  11206  pfxccatin12  11231  cau3lem  11591  fsumcl2lem  11875  dvdsnegb  12285  dvds2add  12302  dvds2sub  12303  ndvdssub  12407  gcd2n0cl  12456  divgcdcoprmex  12590  cncongr1  12591  ctinfom  12965  qusecsub  13834  istopfin  14639  toponcom  14666  cnptoprest  14878  dvmptfsum  15364  elply2  15374