Theorem syl2anr 288

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 287	. 2 ⊢ ((𝜑 ∧ 𝜏) → 𝜃)
5	4	ancoms 266	1 ⊢ ((𝜏 ∧ 𝜑) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  swopo  4266  opswapg  5071  coexg  5129  iotass  5151  resdif  5435  fvexg  5486  isotr  5763  xpexgALT  6078  ixpssmapg  6670  mapen  6788  mapdom1g  6789  elfir  6914  cauappcvgprlemladdfl  7569  addgt0sr  7689  axmulass  7787  axdistr  7788  negeu  8060  ltaddnegr  8294  nnsub  8866  zltnle  9207  elz2  9229  uzaddcl  9491  qaddcl  9537  xltneg  9733  xleneg  9734  iccneg  9886  uzsubsubfz  9942  fzsplit2  9945  fzss1  9958  uzsplit  9987  fz0fzdiffz0  10022  difelfzle  10026  difelfznle  10027  fzonlt0  10059  fzouzsplit  10071  eluzgtdifelfzo  10089  elfzodifsumelfzo  10093  ssfzo12  10116  qltnle  10138  modfzo0difsn  10287  nn0ennn  10325  ser3mono  10370  iseqf1olemjpcl  10387  iseqf1olemqpcl  10388  fser0const  10408  faclbnd  10608  bcval4  10619  bcpasc  10633  hashfacen  10700  seq3coll  10706  crim  10751  fsumshftm  11335  isumshft  11380  cvgratgt0  11423  mertenslemi1  11425  prod1dc  11476  fprod1p  11489  fprodmodd  11531  negdvdsb  11695  dvdsnegb  11696  dvdsmul1  11701  dvdsabseq  11731  dvdsssfz1  11736  odd2np1  11756  ndvdsadd  11814  dvdssqim  11899  nn0seqcvgd  11909  algcvgblem  11917  cncongr2  11972  prmind2  11988  prmdvdsfz  12006  prmndvdsfaclt  12021  phisum  12103  resttopon  12542  cnovex  12567  iscn  12568  iscnp  12570  cnco  12592  cndis  12612  hmeoco  12687  bl2in  12774  metss2lem  12868  metss2  12869  bdxmet  12872  metrest  12877  ioo2bl  12914  elcncf  12931  dvexp  13046  relogexp  13164  logcxp  13189  supfz  13610