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  4401  opswapg  5221  coexg  5279  iotass  5302  resdif  5602  fvexg  5654  isotr  5952  xpexgALT  6290  ixpssmapg  6892  mapen  7027  mapdom1g  7028  elfir  7166  cauappcvgprlemladdfl  7868  addgt0sr  7988  axmulass  8086  axdistr  8087  negeu  8363  ltaddnegr  8598  nnsub  9175  zltnle  9518  ltsubnn0  9540  elz2  9544  uzaddcl  9813  qaddcl  9862  xltneg  10064  xleneg  10065  iccneg  10217  uzsubsubfz  10275  fzsplit2  10278  fzss1  10291  uzsplit  10320  fz0fzdiffz0  10358  difelfzle  10362  difelfznle  10363  fzonlt0  10397  fzouzsplit  10409  fzo0addelr  10427  eluzgtdifelfzo  10435  elfzodifsumelfzo  10439  ssfzo12  10462  qltnle  10496  modfzo0difsn  10650  nn0ennn  10688  seqfveq2g  10732  ser3mono  10742  iseqf1olemjpcl  10763  iseqf1olemqpcl  10764  seqf1oglem1  10774  seqf1oglem2  10775  seqf1og  10776  fser0const  10790  mulsubdivbinom2ap  10966  faclbnd  10996  bcval4  11007  bcpasc  11021  hashfacen  11093  seq3coll  11099  ccatval1  11167  ccatval21sw  11175  ccatrn  11179  ccatalpha  11183  swrd0g  11234  swrdfv2  11237  swrdspsleq  11241  addlenpfx  11265  ccatpfx  11275  swrdswrd  11279  pfxccatin12lem2  11305  pfxccat3  11308  swrdccat  11309  crim  11412  mingeb  11796  fsumshftm  11999  isumshft  12044  cvgratgt0  12087  mertenslemi1  12089  prod1dc  12140  fprod1p  12153  fprodmodd  12195  negdvdsb  12361  dvdsnegb  12362  dvdsmul1  12367  dvdsabseq  12401  dvdsssfz1  12406  odd2np1  12427  ndvdsadd  12485  dvdssqim  12588  nn0seqcvgd  12606  algcvgblem  12614  cncongr2  12669  prmind2  12685  prmdvdsfz  12704  prmndvdsfaclt  12721  dvdsfi  12804  modprm0  12820  modprmn0modprm0  12822  pythagtriplem1  12831  pythagtriplem4  12834  pythagtriplem8  12838  pythagtriplem9  12839  pythagtriplem12  12841  pythagtriplem14  12843  pythagtriplem16  12845  pcexp  12875  pc2dvds  12896  pcz  12898  fldivp1  12914  pcfac  12916  oddprmdvds  12920  pockthg  12923  infpnlem1  12925  1arith  12933  4sqlem11  12967  pwsval  13367  ismgmid  13453  mhmpropd  13542  grpsubid1  13661  mulgnnp1  13710  mulgsubcl  13716  mulgnn0z  13729  mulgnndir  13731  mulgneg2  13736  ghmco  13844  gsumfzfsumlemm  14594  resttopon  14888  cnovex  14913  iscn  14914  iscnp  14916  cnco  14938  cndis  14958  hmeoco  15033  bl2in  15120  metss2lem  15214  metss2  15215  bdxmet  15218  metrest  15223  ioo2bl  15268  expcn  15286  elcncf  15290  dvexp  15428  plypow  15461  relogexp  15589  logcxp  15614  wilthlem1  15697  sgmnncl  15705  mpodvdsmulf1o  15707  lgsdirnn0  15769  gausslemma2dlem1a  15780  lgsquadlem1  15799  lgsquad2  15805  lgsquad3  15806  uspgrupgrushgr  16026  usgrumgruspgr  16029  wksfval  16133  wlkex  16136  supfz  16625