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  4307  opswapg  5116  coexg  5174  iotass  5196  resdif  5484  fvexg  5535  isotr  5817  xpexgALT  6134  ixpssmapg  6728  mapen  6846  mapdom1g  6847  elfir  6972  cauappcvgprlemladdfl  7654  addgt0sr  7774  axmulass  7872  axdistr  7873  negeu  8148  ltaddnegr  8382  nnsub  8958  zltnle  9299  ltsubnn0  9320  elz2  9324  uzaddcl  9586  qaddcl  9635  xltneg  9836  xleneg  9837  iccneg  9989  uzsubsubfz  10047  fzsplit2  10050  fzss1  10063  uzsplit  10092  fz0fzdiffz0  10130  difelfzle  10134  difelfznle  10135  fzonlt0  10167  fzouzsplit  10179  eluzgtdifelfzo  10197  elfzodifsumelfzo  10201  ssfzo12  10224  qltnle  10246  modfzo0difsn  10395  nn0ennn  10433  ser3mono  10478  iseqf1olemjpcl  10495  iseqf1olemqpcl  10496  fser0const  10516  mulsubdivbinom2ap  10691  faclbnd  10721  bcval4  10732  bcpasc  10746  hashfacen  10816  seq3coll  10822  crim  10867  mingeb  11250  fsumshftm  11453  isumshft  11498  cvgratgt0  11541  mertenslemi1  11543  prod1dc  11594  fprod1p  11607  fprodmodd  11649  negdvdsb  11814  dvdsnegb  11815  dvdsmul1  11820  dvdsabseq  11853  dvdsssfz1  11858  odd2np1  11878  ndvdsadd  11936  dvdssqim  12025  nn0seqcvgd  12041  algcvgblem  12049  cncongr2  12104  prmind2  12120  prmdvdsfz  12139  prmndvdsfaclt  12156  phisum  12240  modprm0  12254  modprmn0modprm0  12256  pythagtriplem1  12265  pythagtriplem4  12268  pythagtriplem8  12272  pythagtriplem9  12273  pythagtriplem12  12275  pythagtriplem14  12277  pythagtriplem16  12279  pcexp  12309  pc2dvds  12329  pcz  12331  fldivp1  12346  pcfac  12348  oddprmdvds  12352  pockthg  12355  infpnlem1  12357  1arith  12365  ismgmid  12796  mhmpropd  12857  grpsubid1  12955  mulgnnp1  12991  mulgsubcl  12997  mulgnn0z  13010  mulgnndir  13012  mulgneg2  13017  resttopon  13674  cnovex  13699  iscn  13700  iscnp  13702  cnco  13724  cndis  13744  hmeoco  13819  bl2in  13906  metss2lem  14000  metss2  14001  bdxmet  14004  metrest  14009  ioo2bl  14046  elcncf  14063  dvexp  14178  relogexp  14296  logcxp  14321  lgsdirnn0  14451  supfz  14821