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  8146  ltaddnegr  8380  nnsub  8956  zltnle  9297  ltsubnn0  9318  elz2  9322  uzaddcl  9584  qaddcl  9633  xltneg  9834  xleneg  9835  iccneg  9987  uzsubsubfz  10044  fzsplit2  10047  fzss1  10060  uzsplit  10089  fz0fzdiffz0  10127  difelfzle  10131  difelfznle  10132  fzonlt0  10164  fzouzsplit  10176  eluzgtdifelfzo  10194  elfzodifsumelfzo  10198  ssfzo12  10221  qltnle  10243  modfzo0difsn  10392  nn0ennn  10430  ser3mono  10475  iseqf1olemjpcl  10492  iseqf1olemqpcl  10493  fser0const  10513  faclbnd  10716  bcval4  10727  bcpasc  10741  hashfacen  10811  seq3coll  10817  crim  10862  mingeb  11245  fsumshftm  11448  isumshft  11493  cvgratgt0  11536  mertenslemi1  11538  prod1dc  11589  fprod1p  11602  fprodmodd  11644  negdvdsb  11809  dvdsnegb  11810  dvdsmul1  11815  dvdsabseq  11847  dvdsssfz1  11852  odd2np1  11872  ndvdsadd  11930  dvdssqim  12019  nn0seqcvgd  12035  algcvgblem  12043  cncongr2  12098  prmind2  12114  prmdvdsfz  12133  prmndvdsfaclt  12150  phisum  12234  modprm0  12248  modprmn0modprm0  12250  pythagtriplem1  12259  pythagtriplem4  12262  pythagtriplem8  12266  pythagtriplem9  12267  pythagtriplem12  12269  pythagtriplem14  12271  pythagtriplem16  12273  pcexp  12303  pc2dvds  12323  pcz  12325  fldivp1  12340  pcfac  12342  oddprmdvds  12346  pockthg  12349  infpnlem1  12351  1arith  12359  ismgmid  12750  mhmpropd  12811  grpsubid1  12909  mulgnnp1  12945  mulgsubcl  12951  mulgnn0z  12963  mulgnndir  12965  mulgneg2  12970  resttopon  13564  cnovex  13589  iscn  13590  iscnp  13592  cnco  13614  cndis  13634  hmeoco  13709  bl2in  13796  metss2lem  13890  metss2  13891  bdxmet  13894  metrest  13899  ioo2bl  13936  elcncf  13953  dvexp  14068  relogexp  14186  logcxp  14211  lgsdirnn0  14341  supfz  14700