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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  sylanl2  407  sylanr2  409  andi  830  xoranor  1426  19.41h  1737  sbimi  1817  equs5e  1848  exdistrfor  1853  equs45f  1855  sbidm  1904  eu3h  2132  eupickb  2168  2exeu  2179  darii  2187  festino  2193  baroco  2194  r19.27v  2678  r19.27av  2686  rspc2ev  2945  reu3  3016  difdif  3354  ssddif  3465  inssdif  3467  difin  3468  difindiss  3485  indifdir  3487  difrab  3507  iundif2ss  4078  trssord  4525  ordsuc  4710  find  4746  imainss  5203  dffun5r  5389  fof  5615  f1ocnv  5652  fv3  5718  relelfvdm  5727  funimass4  5753  fvelimab  5759  funconstss  5827  dff2  5852  dffo5  5857  dff1o6  5982  oprabid  6117  ssoprab2i  6177  uchoice  6371  releldm2  6419  ixpf  7002  recexgt0sr  8140  map2psrprg  8172  lediv2a  9226  lbreu  9276  elfzp12  10508  fihashf1rn  11229  ccatsymb  11372  swrdpfx  11481  pfxpfx  11482  pfxccatin12  11507  cau3lem  11882  fsumcl2lem  12167  dvdsnegb  12577  dvds2add  12594  dvds2sub  12595  ndvdssub  12699  gcd2n0cl  12748  divgcdcoprmex  12882  cncongr1  12883  ballotfilemirc  13277  ctinfom  13321  qusecsub  14137  istopfin  15103  toponcom  15130  cnptoprest  15342  dvmptfsum  15828  elply2  15838  subupgr  16526  uspgr2wlkeqi  16620  clwwlknun  16694  alseuals  17177  ralseurals  17178