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  4304  opswapg  5112  coexg  5170  iotass  5192  resdif  5480  fvexg  5531  isotr  5812  xpexgALT  6129  ixpssmapg  6723  mapen  6841  mapdom1g  6842  elfir  6967  cauappcvgprlemladdfl  7649  addgt0sr  7769  axmulass  7867  axdistr  7868  negeu  8142  ltaddnegr  8376  nnsub  8952  zltnle  9293  ltsubnn0  9314  elz2  9318  uzaddcl  9580  qaddcl  9629  xltneg  9830  xleneg  9831  iccneg  9983  uzsubsubfz  10040  fzsplit2  10043  fzss1  10056  uzsplit  10085  fz0fzdiffz0  10123  difelfzle  10127  difelfznle  10128  fzonlt0  10160  fzouzsplit  10172  eluzgtdifelfzo  10190  elfzodifsumelfzo  10194  ssfzo12  10217  qltnle  10239  modfzo0difsn  10388  nn0ennn  10426  ser3mono  10471  iseqf1olemjpcl  10488  iseqf1olemqpcl  10489  fser0const  10509  faclbnd  10712  bcval4  10723  bcpasc  10737  hashfacen  10807  seq3coll  10813  crim  10858  mingeb  11241  fsumshftm  11444  isumshft  11489  cvgratgt0  11532  mertenslemi1  11534  prod1dc  11585  fprod1p  11598  fprodmodd  11640  negdvdsb  11805  dvdsnegb  11806  dvdsmul1  11811  dvdsabseq  11843  dvdsssfz1  11848  odd2np1  11868  ndvdsadd  11926  dvdssqim  12015  nn0seqcvgd  12031  algcvgblem  12039  cncongr2  12094  prmind2  12110  prmdvdsfz  12129  prmndvdsfaclt  12146  phisum  12230  modprm0  12244  modprmn0modprm0  12246  pythagtriplem1  12255  pythagtriplem4  12258  pythagtriplem8  12262  pythagtriplem9  12263  pythagtriplem12  12265  pythagtriplem14  12267  pythagtriplem16  12269  pcexp  12299  pc2dvds  12319  pcz  12321  fldivp1  12336  pcfac  12338  oddprmdvds  12342  pockthg  12345  infpnlem1  12347  1arith  12355  ismgmid  12726  mhmpropd  12785  grpsubid1  12883  mulgnnp1  12919  mulgsubcl  12925  mulgnn0z  12937  mulgnndir  12939  mulgneg2  12944  resttopon  13453  cnovex  13478  iscn  13479  iscnp  13481  cnco  13503  cndis  13523  hmeoco  13598  bl2in  13685  metss2lem  13779  metss2  13780  bdxmet  13783  metrest  13788  ioo2bl  13825  elcncf  13842  dvexp  13957  relogexp  14075  logcxp  14100  lgsdirnn0  14230  supfz  14589