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  4306  opswapg  5115  coexg  5173  iotass  5195  resdif  5483  fvexg  5534  isotr  5816  xpexgALT  6133  ixpssmapg  6727  mapen  6845  mapdom1g  6846  elfir  6971  cauappcvgprlemladdfl  7653  addgt0sr  7773  axmulass  7871  axdistr  7872  negeu  8147  ltaddnegr  8381  nnsub  8957  zltnle  9298  ltsubnn0  9319  elz2  9323  uzaddcl  9585  qaddcl  9634  xltneg  9835  xleneg  9836  iccneg  9988  uzsubsubfz  10046  fzsplit2  10049  fzss1  10062  uzsplit  10091  fz0fzdiffz0  10129  difelfzle  10133  difelfznle  10134  fzonlt0  10166  fzouzsplit  10178  eluzgtdifelfzo  10196  elfzodifsumelfzo  10200  ssfzo12  10223  qltnle  10245  modfzo0difsn  10394  nn0ennn  10432  ser3mono  10477  iseqf1olemjpcl  10494  iseqf1olemqpcl  10495  fser0const  10515  mulsubdivbinom2ap  10690  faclbnd  10720  bcval4  10731  bcpasc  10745  hashfacen  10815  seq3coll  10821  crim  10866  mingeb  11249  fsumshftm  11452  isumshft  11497  cvgratgt0  11540  mertenslemi1  11542  prod1dc  11593  fprod1p  11606  fprodmodd  11648  negdvdsb  11813  dvdsnegb  11814  dvdsmul1  11819  dvdsabseq  11852  dvdsssfz1  11857  odd2np1  11877  ndvdsadd  11935  dvdssqim  12024  nn0seqcvgd  12040  algcvgblem  12048  cncongr2  12103  prmind2  12119  prmdvdsfz  12138  prmndvdsfaclt  12155  phisum  12239  modprm0  12253  modprmn0modprm0  12255  pythagtriplem1  12264  pythagtriplem4  12267  pythagtriplem8  12271  pythagtriplem9  12272  pythagtriplem12  12274  pythagtriplem14  12276  pythagtriplem16  12278  pcexp  12308  pc2dvds  12328  pcz  12330  fldivp1  12345  pcfac  12347  oddprmdvds  12351  pockthg  12354  infpnlem1  12356  1arith  12364  ismgmid  12795  mhmpropd  12856  grpsubid1  12954  mulgnnp1  12990  mulgsubcl  12996  mulgnn0z  13008  mulgnndir  13010  mulgneg2  13015  resttopon  13641  cnovex  13666  iscn  13667  iscnp  13669  cnco  13691  cndis  13711  hmeoco  13786  bl2in  13873  metss2lem  13967  metss2  13968  bdxmet  13971  metrest  13976  ioo2bl  14013  elcncf  14030  dvexp  14145  relogexp  14263  logcxp  14288  lgsdirnn0  14418  supfz  14788