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  8022  addgt0sr  8142  axmulass  8240  axdistr  8241  negeu  8517  ltaddnegr  8753  nnsub  9344  zltnle  9692  ltsubnn0  9714  elz2  9718  uzaddcl  9988  qaddcl  10037  xltneg  10240  xleneg  10241  iccneg  10393  uzsubsubfz  10454  fzsplit2  10457  fzsplit3  10460  fzss1  10471  uzsplit  10501  fz0fzdiffz0  10539  difelfzle  10543  difelfznle  10544  fzonlt0  10578  fzouzsplit  10590  fzo0addelr  10609  eluzgtdifelfzo  10617  elfzodifsumelfzo  10621  ssfzo12  10644  infssfzcldc  10671  infssfzledc  10672  qltnle  10680  modfzo0difsn  10834  nn0ennn  10872  seqfveq2g  10916  ser3mono  10926  iseqf1olemjpcl  10947  iseqf1olemqpcl  10948  seqf1oglem1  10958  seqf1oglem2  10959  seqf1og  10960  fser0const  10974  mulsubdivbinom2ap  11151  faclbnd  11181  bcval4  11192  bcpasc  11206  hashfibclem  11284  hashfacen  11286  seq3coll  11296  ccatval1  11367  ccatval21sw  11375  ccatrn  11379  ccatalpha  11383  swrd0g  11434  swrdfv2  11437  swrdspsleq  11441  addlenpfx  11465  ccatpfx  11475  swrdswrd  11479  pfxccatin12lem2  11505  pfxccat3  11508  swrdccat  11509  crim  11625  mingeb  12010  fsumshftm  12214  isumshft  12259  cvgratgt0  12302  mertenslemi1  12304  prod1dc  12355  fprod1p  12368  fprodmodd  12410  negdvdsb  12576  dvdsnegb  12577  dvdsmul1  12582  dvdsabseq  12616  dvdsssfz1  12621  odd2np1  12642  ndvdsadd  12700  dvdssqim  12803  nn0seqcvgd  12821  algcvgblem  12829  cncongr2  12884  prmind2  12900  prmdvdsfz  12919  prmndvdsfaclt  12936  dvdsfi  13019  modprm0  13035  modprmn0modprm0  13037  pythagtriplem1  13046  pythagtriplem4  13049  pythagtriplem8  13053  pythagtriplem9  13054  pythagtriplem12  13056  pythagtriplem14  13058  pythagtriplem16  13060  pcexp  13090  pc2dvds  13111  pcz  13113  fldivp1  13129  pcfac  13131  oddprmdvds  13135  pockthg  13138  infpnlem1  13140  1arith  13148  4sqlem11  13182  ballotfilemimin  13251  ballotfilemsdom  13257  ismgmid  13699  mhmpropd  13775  grpsubid1  13892  mulgnnp1  13935  mulgsubcl  13941  mulgnn0z  13954  mulgnndir  13956  mulgneg2  13961  ghmco  14069  pwsval  14206  resttopon  15274  cnovex  15299  iscn  15300  iscnp  15302  cnco  15324  cndis  15344  hmeoco  15419  bl2in  15506  metss2lem  15600  metss2  15601  bdxmet  15604  metrest  15609  ioo2bl  15654  expcn  15672  elcncf  15676  dvexp  15814  plypow  15847  relogexp  15977  logcxp  16005  birthdaylem2  16094  wilthlem1  16100  sgmnncl  16108  mpodvdsmulf1o  16110  lgsdirnn0  16178  gausslemma2dlem1a  16189  lgsquadlem1  16208  lgsquad2  16214  lgsquad3  16215  uspgrupgrushgr  16435  usgrumgruspgr  16438  wksfval  16575  wlkex  16578  supfz  17133