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  4403  opswapg  5223  coexg  5281  iotass  5304  resdif  5605  fvexg  5658  isotr  5957  xpexgALT  6295  ixpssmapg  6897  mapen  7032  mapdom1g  7033  elfir  7172  cauappcvgprlemladdfl  7875  addgt0sr  7995  axmulass  8093  axdistr  8094  negeu  8370  ltaddnegr  8605  nnsub  9182  zltnle  9525  ltsubnn0  9547  elz2  9551  uzaddcl  9820  qaddcl  9869  xltneg  10071  xleneg  10072  iccneg  10224  uzsubsubfz  10282  fzsplit2  10285  fzss1  10298  uzsplit  10327  fz0fzdiffz0  10365  difelfzle  10369  difelfznle  10370  fzonlt0  10404  fzouzsplit  10416  fzo0addelr  10435  eluzgtdifelfzo  10443  elfzodifsumelfzo  10447  ssfzo12  10470  qltnle  10504  modfzo0difsn  10658  nn0ennn  10696  seqfveq2g  10740  ser3mono  10750  iseqf1olemjpcl  10771  iseqf1olemqpcl  10772  seqf1oglem1  10782  seqf1oglem2  10783  seqf1og  10784  fser0const  10798  mulsubdivbinom2ap  10974  faclbnd  11004  bcval4  11015  bcpasc  11029  hashfacen  11101  seq3coll  11107  ccatval1  11175  ccatval21sw  11183  ccatrn  11187  ccatalpha  11191  swrd0g  11242  swrdfv2  11245  swrdspsleq  11249  addlenpfx  11273  ccatpfx  11283  swrdswrd  11287  pfxccatin12lem2  11313  pfxccat3  11316  swrdccat  11317  crim  11420  mingeb  11804  fsumshftm  12008  isumshft  12053  cvgratgt0  12096  mertenslemi1  12098  prod1dc  12149  fprod1p  12162  fprodmodd  12204  negdvdsb  12370  dvdsnegb  12371  dvdsmul1  12376  dvdsabseq  12410  dvdsssfz1  12415  odd2np1  12436  ndvdsadd  12494  dvdssqim  12597  nn0seqcvgd  12615  algcvgblem  12623  cncongr2  12678  prmind2  12694  prmdvdsfz  12713  prmndvdsfaclt  12730  dvdsfi  12813  modprm0  12829  modprmn0modprm0  12831  pythagtriplem1  12840  pythagtriplem4  12843  pythagtriplem8  12847  pythagtriplem9  12848  pythagtriplem12  12850  pythagtriplem14  12852  pythagtriplem16  12854  pcexp  12884  pc2dvds  12905  pcz  12907  fldivp1  12923  pcfac  12925  oddprmdvds  12929  pockthg  12932  infpnlem1  12934  1arith  12942  4sqlem11  12976  pwsval  13376  ismgmid  13462  mhmpropd  13551  grpsubid1  13670  mulgnnp1  13719  mulgsubcl  13725  mulgnn0z  13738  mulgnndir  13740  mulgneg2  13745  ghmco  13853  gsumfzfsumlemm  14604  resttopon  14898  cnovex  14923  iscn  14924  iscnp  14926  cnco  14948  cndis  14968  hmeoco  15043  bl2in  15130  metss2lem  15224  metss2  15225  bdxmet  15228  metrest  15233  ioo2bl  15278  expcn  15296  elcncf  15300  dvexp  15438  plypow  15471  relogexp  15599  logcxp  15624  wilthlem1  15707  sgmnncl  15715  mpodvdsmulf1o  15717  lgsdirnn0  15779  gausslemma2dlem1a  15790  lgsquadlem1  15809  lgsquad2  15815  lgsquad3  15816  uspgrupgrushgr  16036  usgrumgruspgr  16039  wksfval  16176  wlkex  16179  supfz  16696