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  4398  opswapg  5218  coexg  5276  iotass  5299  resdif  5599  fvexg  5651  isotr  5949  xpexgALT  6287  ixpssmapg  6888  mapen  7020  mapdom1g  7021  elfir  7156  cauappcvgprlemladdfl  7858  addgt0sr  7978  axmulass  8076  axdistr  8077  negeu  8353  ltaddnegr  8588  nnsub  9165  zltnle  9508  ltsubnn0  9530  elz2  9534  uzaddcl  9798  qaddcl  9847  xltneg  10049  xleneg  10050  iccneg  10202  uzsubsubfz  10260  fzsplit2  10263  fzss1  10276  uzsplit  10305  fz0fzdiffz0  10343  difelfzle  10347  difelfznle  10348  fzonlt0  10382  fzouzsplit  10394  fzo0addelr  10412  eluzgtdifelfzo  10420  elfzodifsumelfzo  10424  ssfzo12  10447  qltnle  10480  modfzo0difsn  10634  nn0ennn  10672  seqfveq2g  10716  ser3mono  10726  iseqf1olemjpcl  10747  iseqf1olemqpcl  10748  seqf1oglem1  10758  seqf1oglem2  10759  seqf1og  10760  fser0const  10774  mulsubdivbinom2ap  10950  faclbnd  10980  bcval4  10991  bcpasc  11005  hashfacen  11076  seq3coll  11082  ccatval1  11150  ccatval21sw  11158  ccatrn  11162  ccatalpha  11166  swrd0g  11213  swrdfv2  11216  swrdspsleq  11220  addlenpfx  11244  ccatpfx  11254  swrdswrd  11258  pfxccatin12lem2  11284  pfxccat3  11287  swrdccat  11288  crim  11390  mingeb  11774  fsumshftm  11977  isumshft  12022  cvgratgt0  12065  mertenslemi1  12067  prod1dc  12118  fprod1p  12131  fprodmodd  12173  negdvdsb  12339  dvdsnegb  12340  dvdsmul1  12345  dvdsabseq  12379  dvdsssfz1  12384  odd2np1  12405  ndvdsadd  12463  dvdssqim  12566  nn0seqcvgd  12584  algcvgblem  12592  cncongr2  12647  prmind2  12663  prmdvdsfz  12682  prmndvdsfaclt  12699  dvdsfi  12782  modprm0  12798  modprmn0modprm0  12800  pythagtriplem1  12809  pythagtriplem4  12812  pythagtriplem8  12816  pythagtriplem9  12817  pythagtriplem12  12819  pythagtriplem14  12821  pythagtriplem16  12823  pcexp  12853  pc2dvds  12874  pcz  12876  fldivp1  12892  pcfac  12894  oddprmdvds  12898  pockthg  12901  infpnlem1  12903  1arith  12911  4sqlem11  12945  pwsval  13345  ismgmid  13431  mhmpropd  13520  grpsubid1  13639  mulgnnp1  13688  mulgsubcl  13694  mulgnn0z  13707  mulgnndir  13709  mulgneg2  13714  ghmco  13822  gsumfzfsumlemm  14572  resttopon  14866  cnovex  14891  iscn  14892  iscnp  14894  cnco  14916  cndis  14936  hmeoco  15011  bl2in  15098  metss2lem  15192  metss2  15193  bdxmet  15196  metrest  15201  ioo2bl  15246  expcn  15264  elcncf  15268  dvexp  15406  plypow  15439  relogexp  15567  logcxp  15592  wilthlem1  15675  sgmnncl  15683  mpodvdsmulf1o  15685  lgsdirnn0  15747  gausslemma2dlem1a  15758  lgsquadlem1  15777  lgsquad2  15783  lgsquad3  15784  uspgrupgrushgr  16001  usgrumgruspgr  16004  wksfval  16094  wlkex  16097  supfz  16553