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  2923  reu3  2994  difdif  3330  ssddif  3439  inssdif  3441  difin  3442  difindiss  3459  indifdir  3461  difrab  3479  iundif2ss  4034  trssord  4475  ordsuc  4659  find  4695  imainss  5150  dffun5r  5336  fof  5556  f1ocnv  5593  fv3  5658  relelfvdm  5667  funimass4  5692  fvelimab  5698  funconstss  5761  dff2  5787  dffo5  5792  dff1o6  5912  oprabid  6045  ssoprab2i  6105  uchoice  6295  releldm2  6343  ixpf  6884  recexgt0sr  7986  map2psrprg  8018  lediv2a  9068  lbreu  9118  elfzp12  10327  fihashf1rn  11043  ccatsymb  11172  swrdpfx  11281  pfxpfx  11282  pfxccatin12  11307  cau3lem  11668  fsumcl2lem  11952  dvdsnegb  12362  dvds2add  12379  dvds2sub  12380  ndvdssub  12484  gcd2n0cl  12533  divgcdcoprmex  12667  cncongr1  12668  ctinfom  13042  qusecsub  13911  istopfin  14717  toponcom  14744  cnptoprest  14956  dvmptfsum  15442  elply2  15452  uspgr2wlkeqi  16178  clwwlknun  16250