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  826  xoranor  1422  19.41h  1733  sbimi  1813  equs5e  1844  exdistrfor  1849  equs45f  1851  sbidm  1900  eu3h  2128  eupickb  2164  2exeu  2175  darii  2183  festino  2189  baroco  2190  r19.27v  2672  r19.27av  2680  rspc2ev  2939  reu3  3010  difdif  3348  ssddif  3459  inssdif  3461  difin  3462  difindiss  3479  indifdir  3481  difrab  3499  iundif2ss  4062  trssord  4506  ordsuc  4690  find  4726  imainss  5183  dffun5r  5369  fof  5595  f1ocnv  5632  fv3  5698  relelfvdm  5707  funimass4  5732  fvelimab  5738  funconstss  5801  dff2  5826  dffo5  5831  dff1o6  5955  oprabid  6090  ssoprab2i  6150  uchoice  6344  releldm2  6392  ixpf  6968  recexgt0sr  8104  map2psrprg  8136  lediv2a  9189  lbreu  9239  elfzp12  10458  fihashf1rn  11179  ccatsymb  11318  swrdpfx  11427  pfxpfx  11428  pfxccatin12  11453  cau3lem  11827  fsumcl2lem  12112  dvdsnegb  12522  dvds2add  12539  dvds2sub  12540  ndvdssub  12644  gcd2n0cl  12693  divgcdcoprmex  12827  cncongr1  12828  ballotfilemirc  13222  ctinfom  13266  qusecsub  14087  istopfin  14994  toponcom  15021  cnptoprest  15233  dvmptfsum  15719  elply2  15729  subupgr  16397  uspgr2wlkeqi  16491  clwwlknun  16565