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  4449  opswapg  5272  coexg  5330  iotass  5353  resdif  5659  fvexg  5712  isotr  6016  xpexgALT  6360  mapsnd  6964  ixpssmapg  7004  mapen  7140  mapdom1g  7141  elfir  7301  cauappcvgprlemladdfl  8016  addgt0sr  8136  axmulass  8234  axdistr  8235  negeu  8511  ltaddnegr  8747  nnsub  9326  zltnle  9673  ltsubnn0  9695  elz2  9699  uzaddcl  9969  qaddcl  10018  xltneg  10221  xleneg  10222  iccneg  10374  uzsubsubfz  10435  fzsplit2  10438  fzsplit3  10441  fzss1  10452  uzsplit  10482  fz0fzdiffz0  10520  difelfzle  10524  difelfznle  10525  fzonlt0  10559  fzouzsplit  10571  fzo0addelr  10590  eluzgtdifelfzo  10598  elfzodifsumelfzo  10602  ssfzo12  10625  infssfzcldc  10652  infssfzledc  10653  qltnle  10661  modfzo0difsn  10815  nn0ennn  10853  seqfveq2g  10897  ser3mono  10907  iseqf1olemjpcl  10928  iseqf1olemqpcl  10929  seqf1oglem1  10939  seqf1oglem2  10940  seqf1og  10941  fser0const  10955  mulsubdivbinom2ap  11132  faclbnd  11162  bcval4  11173  bcpasc  11187  hashfibclem  11265  hashfacen  11267  seq3coll  11277  ccatval1  11348  ccatval21sw  11356  ccatrn  11360  ccatalpha  11364  swrd0g  11415  swrdfv2  11418  swrdspsleq  11422  addlenpfx  11446  ccatpfx  11456  swrdswrd  11460  pfxccatin12lem2  11486  pfxccat3  11489  swrdccat  11490  crim  11606  mingeb  11991  fsumshftm  12195  isumshft  12240  cvgratgt0  12283  mertenslemi1  12285  prod1dc  12336  fprod1p  12349  fprodmodd  12391  negdvdsb  12557  dvdsnegb  12558  dvdsmul1  12563  dvdsabseq  12597  dvdsssfz1  12602  odd2np1  12623  ndvdsadd  12681  dvdssqim  12784  nn0seqcvgd  12802  algcvgblem  12810  cncongr2  12865  prmind2  12881  prmdvdsfz  12900  prmndvdsfaclt  12917  dvdsfi  13000  modprm0  13016  modprmn0modprm0  13018  pythagtriplem1  13027  pythagtriplem4  13030  pythagtriplem8  13034  pythagtriplem9  13035  pythagtriplem12  13037  pythagtriplem14  13039  pythagtriplem16  13041  pcexp  13071  pc2dvds  13092  pcz  13094  fldivp1  13110  pcfac  13112  oddprmdvds  13116  pockthg  13119  infpnlem1  13121  1arith  13129  4sqlem11  13163  ballotfilemimin  13232  ballotfilemsdom  13238  ismgmid  13680  mhmpropd  13756  grpsubid1  13873  mulgnnp1  13916  mulgsubcl  13922  mulgnn0z  13935  mulgnndir  13937  mulgneg2  13942  ghmco  14050  pwsval  14187  resttopon  15255  cnovex  15280  iscn  15281  iscnp  15283  cnco  15305  cndis  15325  hmeoco  15400  bl2in  15487  metss2lem  15581  metss2  15582  bdxmet  15585  metrest  15590  ioo2bl  15635  expcn  15653  elcncf  15657  dvexp  15795  plypow  15828  relogexp  15956  logcxp  15982  birthdaylem2  16071  wilthlem1  16077  sgmnncl  16085  mpodvdsmulf1o  16087  lgsdirnn0  16149  gausslemma2dlem1a  16160  lgsquadlem1  16179  lgsquad2  16185  lgsquad3  16186  uspgrupgrushgr  16406  usgrumgruspgr  16409  wksfval  16546  wlkex  16549  supfz  17095