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  825  xoranor  1421  19.41h  1732  sbimi  1811  equs5e  1842  exdistrfor  1847  equs45f  1849  sbidm  1898  eu3h  2124  eupickb  2160  2exeu  2171  darii  2179  festino  2185  baroco  2186  r19.27v  2659  r19.27av  2667  rspc2ev  2924  reu3  2995  difdif  3331  ssddif  3440  inssdif  3442  difin  3443  difindiss  3460  indifdir  3462  difrab  3480  iundif2ss  4037  trssord  4479  ordsuc  4663  find  4699  imainss  5154  dffun5r  5340  fof  5562  f1ocnv  5599  fv3  5665  relelfvdm  5674  funimass4  5699  fvelimab  5705  funconstss  5768  dff2  5794  dffo5  5799  dff1o6  5922  oprabid  6055  ssoprab2i  6115  uchoice  6305  releldm2  6353  ixpf  6894  recexgt0sr  7998  map2psrprg  8030  lediv2a  9080  lbreu  9130  elfzp12  10339  fihashf1rn  11056  ccatsymb  11188  swrdpfx  11297  pfxpfx  11298  pfxccatin12  11323  cau3lem  11697  fsumcl2lem  11982  dvdsnegb  12392  dvds2add  12409  dvds2sub  12410  ndvdssub  12514  gcd2n0cl  12563  divgcdcoprmex  12697  cncongr1  12698  ctinfom  13072  qusecsub  13941  istopfin  14753  toponcom  14780  cnptoprest  14992  dvmptfsum  15478  elply2  15488  subupgr  16153  uspgr2wlkeqi  16247  clwwlknun  16321