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  819  xoranor  1388  19.41h  1696  sbimi  1775  equs5e  1806  exdistrfor  1811  equs45f  1813  sbidm  1862  eu3h  2087  eupickb  2123  2exeu  2134  darii  2142  festino  2148  baroco  2149  r19.27v  2621  r19.27av  2629  rspc2ev  2879  reu3  2950  difdif  3284  ssddif  3393  inssdif  3395  difin  3396  difindiss  3413  indifdir  3415  difrab  3433  iundif2ss  3978  trssord  4411  ordsuc  4595  find  4631  imainss  5081  dffun5r  5266  fof  5476  f1ocnv  5513  fv3  5577  relelfvdm  5586  funimass4  5607  fvelimab  5613  funconstss  5676  dff2  5702  dffo5  5707  dff1o6  5819  oprabid  5950  ssoprab2i  6007  uchoice  6190  releldm2  6238  ixpf  6774  recexgt0sr  7833  map2psrprg  7865  lediv2a  8914  lbreu  8964  elfzp12  10165  fihashf1rn  10859  cau3lem  11258  fsumcl2lem  11541  dvdsnegb  11951  dvds2add  11968  dvds2sub  11969  ndvdssub  12071  gcd2n0cl  12106  divgcdcoprmex  12240  cncongr1  12241  ctinfom  12585  qusecsub  13401  istopfin  14168  toponcom  14195  cnptoprest  14407  elply2  14881