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 ⊢ ((𝜏 ∧ 𝜑) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  swopo  4451  opswapg  5274  coexg  5332  iotass  5355  resdif  5661  fvexg  5714  isotr  6022  xpexgALT  6366  mapsnd  6970  ixpssmapg  7010  mapen  7146  mapdom1g  7147  elfir  7307  cauappcvgprlemladdfl  8023  addgt0sr  8143  axmulass  8241  axdistr  8242  negeu  8519  ltaddnegr  8755  nnsub  9346  zltnle  9695  ltsubnn0  9717  elz2  9721  uzaddcl  9996  qaddcl  10045  xltneg  10249  xleneg  10250  iccneg  10402  uzsubsubfz  10463  fzsplit2  10466  fzsplit3  10469  fzss1  10480  uzsplit  10510  fz0fzdiffz0  10548  difelfzle  10552  difelfznle  10553  fzonlt0  10587  fzouzsplit  10599  fzo0addelr  10618  eluzgtdifelfzo  10626  elfzodifsumelfzo  10630  ssfzo12  10653  infssfzcldc  10680  infssfzledc  10681  qltnle  10689  modfzo0difsn  10846  nn0ennn  10884  seqfveq2g  10928  ser3mono  10938  iseqf1olemjpcl  10959  iseqf1olemqpcl  10960  seqf1oglem1  10970  seqf1oglem2  10971  seqf1og  10972  fser0const  10986  mulsubdivbinom2ap  11164  faclbnd  11194  bcval4  11205  bcpasc  11219  hashfibclem  11297  hashfacen  11299  seq3coll  11309  ccatval1  11380  ccatval21sw  11388  ccatrn  11392  ccatalpha  11396  swrd0g  11447  swrdfv2  11450  swrdspsleq  11454  addlenpfx  11478  ccatpfx  11488  swrdswrd  11492  pfxccatin12lem2  11518  pfxccat3  11521  swrdccat  11522  crim  11638  mingeb  12026  fsumshftm  12230  isumshft  12275  cvgratgt0  12318  mertenslemi1  12320  prod1dc  12371  fprod1p  12384  fprodmodd  12426  negdvdsb  12592  dvdsnegb  12593  dvdsmul1  12598  dvdsabseq  12632  dvdsssfz1  12637  odd2np1  12658  ndvdsadd  12716  dvdssqim  12819  nn0seqcvgd  12837  algcvgblem  12845  cncongr2  12900  prmind2  12916  prmdvdsfz  12936  prmndvdsfaclt  12953  dvdsfi  13039  modprm0  13055  modprmn0modprm0  13057  pythagtriplem1  13066  pythagtriplem4  13069  pythagtriplem8  13073  pythagtriplem9  13074  pythagtriplem12  13076  pythagtriplem14  13078  pythagtriplem16  13080  pcexp  13110  pc2dvds  13131  pcz  13133  fldivp1  13149  pcfac  13151  oddprmdvds  13155  pockthg  13158  infpnlem1  13160  1arith  13168  4sqlem11  13202  ballotfilemimin  13300  ballotfilemsdom  13306  ismgmid  13748  mhmpropd  13824  grpsubid1  13941  mulgnnp1  13984  mulgsubcl  13990  mulgnn0z  14003  mulgnndir  14005  mulgneg2  14010  ghmco  14118  pwsval  14255  resttopon  15324  cnovex  15349  iscn  15350  iscnp  15352  cnco  15374  cndis  15394  hmeoco  15469  bl2in  15556  metss2lem  15650  metss2  15651  bdxmet  15654  metrest  15659  ioo2bl  15704  expcn  15722  elcncf  15726  dvexp  15864  plypow  15897  relogexp  16027  logcxp  16055  birthdaylem2  16148  wilthlem1  16154  prmdvdsfi  16165  sgmnncl  16179  mpodvdsmulf1o  16206  chtublem  16217  chtqub  16218  bposlem3  16235  bposlem5  16237  lgsdirnn0  16288  gausslemma2dlem1a  16299  lgsquadlem1  16318  lgsquad2  16324  lgsquad3  16325  uspgrupgrushgr  16545  usgrumgruspgr  16548  wksfval  16685  wlkex  16688  supfz  17243