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  819  xoranor  1388  19.41h  1696  sbimi  1775  equs5e  1806  exdistrfor  1811  equs45f  1813  sbidm  1862  eu3h  2087  eupickb  2123  2exeu  2134  darii  2142  festino  2148  baroco  2149  r19.27v  2621  r19.27av  2629  rspc2ev  2880  reu3  2951  difdif  3285  ssddif  3394  inssdif  3396  difin  3397  difindiss  3414  indifdir  3416  difrab  3434  iundif2ss  3979  trssord  4412  ordsuc  4596  find  4632  imainss  5082  dffun5r  5267  fof  5477  f1ocnv  5514  fv3  5578  relelfvdm  5587  funimass4  5608  fvelimab  5614  funconstss  5677  dff2  5703  dffo5  5708  dff1o6  5820  oprabid  5951  ssoprab2i  6008  uchoice  6192  releldm2  6240  ixpf  6776  recexgt0sr  7835  map2psrprg  7867  lediv2a  8916  lbreu  8966  elfzp12  10168  fihashf1rn  10862  cau3lem  11261  fsumcl2lem  11544  dvdsnegb  11954  dvds2add  11971  dvds2sub  11972  ndvdssub  12074  gcd2n0cl  12109  divgcdcoprmex  12243  cncongr1  12244  ctinfom  12588  qusecsub  13404  istopfin  14179  toponcom  14206  cnptoprest  14418  dvmptfsum  14904  elply2  14914