Theorem anim2i 339

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 336	1 ⊢ ((𝜒 ∧ 𝜑) → (𝜒 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  sylanl2  400  sylanr2  402  andi  807  pm4.55dc  922  xoranor  1355  19.41h  1663  sbimi  1737  equs5e  1767  exdistrfor  1772  equs45f  1774  sbidm  1823  eu3h  2042  eupickb  2078  2exeu  2089  darii  2097  festino  2103  baroco  2104  r19.27v  2557  r19.27av  2565  rspc2ev  2799  reu3  2869  difdif  3196  ssddif  3305  inssdif  3307  difin  3308  difindiss  3325  indifdir  3327  difrab  3345  iundif2ss  3873  trssord  4297  ordsuc  4473  find  4508  imainss  4949  dffun5r  5130  fof  5340  f1ocnv  5373  fv3  5437  relelfvdm  5446  funimass4  5465  fvelimab  5470  funconstss  5531  dff2  5557  dffo5  5562  dff1o6  5670  oprabid  5796  ssoprab2i  5853  releldm2  6076  ixpf  6607  recexgt0sr  7574  map2psrprg  7606  lediv2a  8646  lbreu  8696  elfzp12  9872  focdmex  10526  fihashf1rn  10528  cau3lem  10879  fsumcl2lem  11160  dvdsnegb  11499  dvds2add  11516  dvds2sub  11517  ndvdssub  11616  gcd2n0cl  11647  divgcdcoprmex  11772  cncongr1  11773  ctinfom  11930  istopfin  12156  toponcom  12183  cnptoprest  12397