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  4453  opswapg  5277  coexg  5335  iotass  5358  resdif  5664  fvexg  5717  isotr  6025  xpexgALT  6370  mapsnd  6975  ixpssmapg  7015  mapen  7151  mapdom1g  7152  elfir  7313  cauappcvgprlemladdfl  8029  addgt0sr  8149  axmulass  8247  axdistr  8248  negeu  8525  ltaddnegr  8761  nnsub  9353  zltnle  9702  ltsubnn0  9724  elz2  9728  uzaddcl  10003  qaddcl  10052  xltneg  10256  xleneg  10257  iccneg  10409  uzsubsubfz  10470  fzsplit2  10473  fzsplit3  10476  fzss1  10487  uzsplit  10517  fz0fzdiffz0  10555  difelfzle  10559  difelfznle  10560  fzonlt0  10594  fzouzsplit  10606  fzo0addelr  10625  eluzgtdifelfzo  10633  elfzodifsumelfzo  10637  ssfzo12  10660  infssfzcldc  10687  infssfzledc  10688  qltnle  10696  modfzo0difsn  10854  nn0ennn  10892  seqfveq2g  10936  ser3mono  10946  iseqf1olemjpcl  10967  iseqf1olemqpcl  10968  seqf1oglem1  10978  seqf1oglem2  10979  seqf1og  10980  fser0const  10994  mulsubdivbinom2ap  11172  faclbnd  11202  bcval4  11213  bcpasc  11227  hashfibclem  11305  hashfacen  11307  seq3coll  11317  ccatval1  11388  ccatval21sw  11396  ccatrn  11400  ccatalpha  11404  swrd0g  11455  swrdfv2  11458  swrdspsleq  11462  addlenpfx  11486  ccatpfx  11496  swrdswrd  11500  pfxccatin12lem2  11526  pfxccat3  11529  swrdccat  11530  crim  11646  mingeb  12034  fsumshftm  12238  isumshft  12283  cvgratgt0  12326  mertenslemi1  12328  prod1dc  12379  fprod1p  12392  fprodmodd  12434  negdvdsb  12600  dvdsnegb  12601  dvdsmul1  12606  dvdsabseq  12640  dvdsssfz1  12645  odd2np1  12666  ndvdsadd  12724  dvdssqim  12827  nn0seqcvgd  12845  algcvgblem  12853  cncongr2  12908  prmind2  12924  prmdvdsfz  12944  prmndvdsfaclt  12961  dvdsfi  13047  modprm0  13063  modprmn0modprm0  13065  pythagtriplem1  13074  pythagtriplem4  13077  pythagtriplem8  13081  pythagtriplem9  13082  pythagtriplem12  13084  pythagtriplem14  13086  pythagtriplem16  13088  pcexp  13118  pc2dvds  13139  pcz  13141  fldivp1  13157  pcfac  13159  oddprmdvds  13163  pockthg  13166  infpnlem1  13168  1arith  13176  4sqlem11  13210  ballotfilemimin  13308  ballotfilemsdom  13314  ismgmid  13757  mhmpropd  13833  grpsubid1  13950  mulgnnp1  13993  mulgsubcl  13999  mulgnn0z  14012  mulgnndir  14014  mulgneg2  14019  ghmco  14127  pwsval  14312  resttopon  15409  cnovex  15434  iscn  15435  iscnp  15437  cnco  15459  cndis  15479  hmeoco  15554  bl2in  15641  metss2lem  15735  metss2  15736  bdxmet  15739  metrest  15744  ioo2bl  15789  expcn  15807  elcncf  15811  dvexp  15949  plypow  15982  relogexp  16114  logcxp  16142  birthdaylem2  16238  wilthlem1  16244  prmdvdsfi  16255  sgmnncl  16269  mpodvdsmulf1o  16296  chtublem  16307  chtqub  16308  bposlem3  16325  bposlem5  16327  bposlem6  16328  lgsdirnn0  16383  gausslemma2dlem1a  16394  lgsquadlem1  16413  lgsquad2  16419  lgsquad3  16420  uspgrupgrushgr  16640  usgrumgruspgr  16643  wksfval  16780  wlkex  16783  supfz  17340