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  2126  eupickb  2162  2exeu  2173  darii  2181  festino  2187  baroco  2188  r19.27v  2670  r19.27av  2678  rspc2ev  2935  reu3  3006  difdif  3343  ssddif  3454  inssdif  3456  difin  3457  difindiss  3474  indifdir  3476  difrab  3494  iundif2ss  4056  trssord  4500  ordsuc  4684  find  4720  imainss  5177  dffun5r  5363  fof  5589  f1ocnv  5626  fv3  5692  relelfvdm  5701  funimass4  5726  fvelimab  5732  funconstss  5795  dff2  5820  dffo5  5825  dff1o6  5948  oprabid  6081  ssoprab2i  6141  uchoice  6330  releldm2  6378  ixpf  6954  recexgt0sr  8084  map2psrprg  8116  lediv2a  9165  lbreu  9215  elfzp12  10429  fihashf1rn  11146  ccatsymb  11283  swrdpfx  11392  pfxpfx  11393  pfxccatin12  11418  cau3lem  11792  fsumcl2lem  12077  dvdsnegb  12487  dvds2add  12504  dvds2sub  12505  ndvdssub  12609  gcd2n0cl  12658  divgcdcoprmex  12792  cncongr1  12793  ctinfom  13168  qusecsub  14037  istopfin  14852  toponcom  14879  cnptoprest  15091  dvmptfsum  15577  elply2  15587  subupgr  16255  uspgr2wlkeqi  16349  clwwlknun  16423