Theorem syl2anr 290

Description: A double syllogism inference. (Contributed by NM, 17-Sep-2013.)

Hypotheses

Ref	Expression
syl2an.1	⊢ (𝜑 → 𝜓)
syl2an.2	⊢ (𝜏 → 𝜒)
syl2an.3	⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
syl2anr	⊢ ((𝜏 ∧ 𝜑) → 𝜃)

Proof of Theorem syl2anr

Step	Hyp	Ref	Expression
1		syl2an.1	. . 3 ⊢ (𝜑 → 𝜓)
2		syl2an.2	. . 3 ⊢ (𝜏 → 𝜒)
3		syl2an.3	. . 3 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	1, 2, 3	syl2an 289	. 2 ⊢ ((𝜑 ∧ 𝜏) → 𝜃)
5	4	ancoms 268	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:  swopo  4397  opswapg  5215  coexg  5273  iotass  5296  resdif  5594  fvexg  5646  isotr  5940  xpexgALT  6278  ixpssmapg  6875  mapen  7007  mapdom1g  7008  elfir  7140  cauappcvgprlemladdfl  7842  addgt0sr  7962  axmulass  8060  axdistr  8061  negeu  8337  ltaddnegr  8572  nnsub  9149  zltnle  9492  ltsubnn0  9514  elz2  9518  uzaddcl  9781  qaddcl  9830  xltneg  10032  xleneg  10033  iccneg  10185  uzsubsubfz  10243  fzsplit2  10246  fzss1  10259  uzsplit  10288  fz0fzdiffz0  10326  difelfzle  10330  difelfznle  10331  fzonlt0  10365  fzouzsplit  10377  fzo0addelr  10395  eluzgtdifelfzo  10403  elfzodifsumelfzo  10407  ssfzo12  10430  qltnle  10463  modfzo0difsn  10617  nn0ennn  10655  seqfveq2g  10699  ser3mono  10709  iseqf1olemjpcl  10730  iseqf1olemqpcl  10731  seqf1oglem1  10741  seqf1oglem2  10742  seqf1og  10743  fser0const  10757  mulsubdivbinom2ap  10933  faclbnd  10963  bcval4  10974  bcpasc  10988  hashfacen  11058  seq3coll  11064  ccatval1  11132  ccatval21sw  11140  ccatrn  11144  swrd0g  11192  swrdfv2  11195  swrdspsleq  11199  addlenpfx  11223  ccatpfx  11233  swrdswrd  11237  pfxccatin12lem2  11263  pfxccat3  11266  swrdccat  11267  crim  11369  mingeb  11753  fsumshftm  11956  isumshft  12001  cvgratgt0  12044  mertenslemi1  12046  prod1dc  12097  fprod1p  12110  fprodmodd  12152  negdvdsb  12318  dvdsnegb  12319  dvdsmul1  12324  dvdsabseq  12358  dvdsssfz1  12363  odd2np1  12384  ndvdsadd  12442  dvdssqim  12545  nn0seqcvgd  12563  algcvgblem  12571  cncongr2  12626  prmind2  12642  prmdvdsfz  12661  prmndvdsfaclt  12678  dvdsfi  12761  modprm0  12777  modprmn0modprm0  12779  pythagtriplem1  12788  pythagtriplem4  12791  pythagtriplem8  12795  pythagtriplem9  12796  pythagtriplem12  12798  pythagtriplem14  12800  pythagtriplem16  12802  pcexp  12832  pc2dvds  12853  pcz  12855  fldivp1  12871  pcfac  12873  oddprmdvds  12877  pockthg  12880  infpnlem1  12882  1arith  12890  4sqlem11  12924  pwsval  13324  ismgmid  13410  mhmpropd  13499  grpsubid1  13618  mulgnnp1  13667  mulgsubcl  13673  mulgnn0z  13686  mulgnndir  13688  mulgneg2  13693  ghmco  13801  gsumfzfsumlemm  14551  resttopon  14845  cnovex  14870  iscn  14871  iscnp  14873  cnco  14895  cndis  14915  hmeoco  14990  bl2in  15077  metss2lem  15171  metss2  15172  bdxmet  15175  metrest  15180  ioo2bl  15225  expcn  15243  elcncf  15247  dvexp  15385  plypow  15418  relogexp  15546  logcxp  15571  wilthlem1  15654  sgmnncl  15662  mpodvdsmulf1o  15664  lgsdirnn0  15726  gausslemma2dlem1a  15737  lgsquadlem1  15756  lgsquad2  15762  lgsquad3  15763  uspgrupgrushgr  15980  usgrumgruspgr  15983  wksfval  16035  supfz  16439