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  4432  opswapg  5254  coexg  5312  iotass  5335  resdif  5641  fvexg  5694  isotr  5995  xpexgALT  6339  mapsnd  6936  ixpssmapg  6976  mapen  7112  mapdom1g  7113  elfir  7273  cauappcvgprlemladdfl  7986  addgt0sr  8106  axmulass  8204  axdistr  8205  negeu  8481  ltaddnegr  8717  nnsub  9296  zltnle  9643  ltsubnn0  9665  elz2  9669  uzaddcl  9939  qaddcl  9988  xltneg  10191  xleneg  10192  iccneg  10344  uzsubsubfz  10404  fzsplit2  10407  fzsplit3  10410  fzss1  10421  uzsplit  10451  fz0fzdiffz0  10489  difelfzle  10493  difelfznle  10494  fzonlt0  10528  fzouzsplit  10540  fzo0addelr  10559  eluzgtdifelfzo  10567  elfzodifsumelfzo  10571  ssfzo12  10594  infssfzcldc  10621  infssfzledc  10622  qltnle  10630  modfzo0difsn  10784  nn0ennn  10822  seqfveq2g  10866  ser3mono  10876  iseqf1olemjpcl  10897  iseqf1olemqpcl  10898  seqf1oglem1  10908  seqf1oglem2  10909  seqf1og  10910  fser0const  10924  mulsubdivbinom2ap  11101  faclbnd  11131  bcval4  11142  bcpasc  11156  hashfibclem  11234  hashfacen  11236  seq3coll  11242  ccatval1  11313  ccatval21sw  11321  ccatrn  11325  ccatalpha  11329  swrd0g  11380  swrdfv2  11383  swrdspsleq  11387  addlenpfx  11411  ccatpfx  11421  swrdswrd  11425  pfxccatin12lem2  11451  pfxccat3  11454  swrdccat  11455  crim  11571  mingeb  11955  fsumshftm  12159  isumshft  12204  cvgratgt0  12247  mertenslemi1  12249  prod1dc  12300  fprod1p  12313  fprodmodd  12355  negdvdsb  12521  dvdsnegb  12522  dvdsmul1  12527  dvdsabseq  12561  dvdsssfz1  12566  odd2np1  12587  ndvdsadd  12645  dvdssqim  12748  nn0seqcvgd  12766  algcvgblem  12774  cncongr2  12829  prmind2  12845  prmdvdsfz  12864  prmndvdsfaclt  12881  dvdsfi  12964  modprm0  12980  modprmn0modprm0  12982  pythagtriplem1  12991  pythagtriplem4  12994  pythagtriplem8  12998  pythagtriplem9  12999  pythagtriplem12  13001  pythagtriplem14  13003  pythagtriplem16  13005  pcexp  13035  pc2dvds  13056  pcz  13058  fldivp1  13074  pcfac  13076  oddprmdvds  13080  pockthg  13083  infpnlem1  13085  1arith  13093  4sqlem11  13127  ballotfilemimin  13196  ballotfilemsdom  13202  ismgmid  13643  mhmpropd  13724  grpsubid1  13843  mulgnnp1  13886  mulgsubcl  13892  mulgnn0z  13905  mulgnndir  13907  mulgneg2  13912  ghmco  14020  pwsval  14149  gsumfzfsumlemm  14864  resttopon  15165  cnovex  15190  iscn  15191  iscnp  15193  cnco  15215  cndis  15235  hmeoco  15310  bl2in  15397  metss2lem  15491  metss2  15492  bdxmet  15495  metrest  15500  ioo2bl  15545  expcn  15563  elcncf  15567  dvexp  15705  plypow  15738  relogexp  15866  logcxp  15891  wilthlem1  15977  sgmnncl  15985  mpodvdsmulf1o  15987  lgsdirnn0  16049  gausslemma2dlem1a  16060  lgsquadlem1  16079  lgsquad2  16085  lgsquad3  16086  uspgrupgrushgr  16306  usgrumgruspgr  16309  wksfval  16446  wlkex  16449  supfz  16996