MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl31anc Structured version   Visualization version   GIF version

Theorem syl31anc 1327
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
syl12anc.1 (𝜑𝜓)
syl12anc.2 (𝜑𝜒)
syl12anc.3 (𝜑𝜃)
syl22anc.4 (𝜑𝜏)
syl31anc.5 (((𝜓𝜒𝜃) ∧ 𝜏) → 𝜂)
Assertion
Ref Expression
syl31anc (𝜑𝜂)

Proof of Theorem syl31anc
StepHypRef Expression
1 syl12anc.1 . . 3 (𝜑𝜓)
2 syl12anc.2 . . 3 (𝜑𝜒)
3 syl12anc.3 . . 3 (𝜑𝜃)
41, 2, 33jca 1240 . 2 (𝜑 → (𝜓𝜒𝜃))
5 syl22anc.4 . 2 (𝜑𝜏)
6 syl31anc.5 . 2 (((𝜓𝜒𝜃) ∧ 𝜏) → 𝜂)
74, 5, 6syl2anc 692 1 (𝜑𝜂)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1038
This theorem is referenced by:  syl32anc  1332  stoic4b  1701  elovmpt3rab1  6878  smo11  7446  omeulem2  7648  oeeui  7667  oaabs2  7710  omabs  7712  omxpenlem  8046  map2xp  8115  mapdom2  8116  fsuppsssupp  8276  cantnflt  8554  cnfcom  8582  mapcdaen  8991  pwsdompw  9011  cofsmo  9076  fin1a2lem4  9210  ltmul12a  10864  lt2msq1  10892  ledivp1  10910  lemul1ad  10948  lemul2ad  10949  suprubd  10970  supaddc  10975  supadd  10976  supmul1  10977  supmul  10980  rpnnen1lem3  11801  rpnnen1lem5  11803  rpnnen1lem3OLD  11807  rpnnen1lem5OLD  11809  lediv2ad  11879  xaddge0  12073  xadddi  12110  xadddi2  12112  supicc  12305  supiccub  12306  supicclub  12307  difelfznle  12437  flval3  12599  expcan  12896  ltexp2  12897  ltexp2r  12900  expubnd  12904  ltexp2rd  13016  ltexp2d  13021  leexp2d  13022  expcand  13023  swrdid  13410  swrd0fv  13421  swrds1  13433  ccatswrd  13438  swrdccat2  13440  swrdccatin2  13468  swrdccatin12lem2  13470  swrdccatin12lem3  13471  splfv1  13487  cshwidxmod  13530  wrdl3s3  13686  o1fsum  14526  mertenslem1  14597  eftlub  14820  rpnnen2lem4  14927  ruclem12  14951  dvdsadd  15005  3dvds  15033  3dvdsOLD  15034  divalgmod  15110  divalgmodOLD  15111  bitsmod  15139  bitsinv1lem  15144  bezoutlem4  15240  gcdzeq  15252  rplpwr  15257  sqgcd  15259  bezoutr  15262  rpmulgcd2  15351  rpdvds  15355  coprmproddvdslem  15357  isprm5  15400  divgcdodd  15403  divnumden  15437  crth  15464  phimullem  15465  modprm0  15491  modprmn0modprm0  15493  coprimeprodsq2  15495  pythagtriplem19  15519  pockthlem  15590  prmunb  15599  prmreclem3  15603  prmreclem6  15606  ramub  15698  ramz  15710  pmtrprfv  17854  pmtrprfv3  17855  mndodcong  17942  odngen  17973  pgpfi  18001  pgpssslw  18010  sylow2blem3  18018  lsmless1  18055  lsmless2  18056  lsmless12  18057  lsmmod2  18070  pj1id  18093  odadd2  18233  gexexlem  18236  ablfacrplem  18445  ablfacrp  18446  ablfac1b  18450  ablfac1eu  18453  pgpfac1lem2  18455  kerf1hrm  18724  lsmssspx  19069  lspsncv0  19127  coe1subfv  19617  coe1fzgsumdlem  19652  znunit  19893  uvcvvcl2  20108  uvcvv1  20109  uvcvv0  20110  scmate  20297  mdetunilem2  20400  pmatcoe1fsupp  20487  mat2pmatlin  20521  decpmatmullem  20557  pmatcollpw1lem1  20560  pmatcollpw1lem2  20561  pm2mpghm  20602  chpscmat  20628  chp0mat  20632  chpidmat  20633  cpmadugsumlemB  20660  cpmadugsumlemC  20661  cpmadugsumlemF  20662  clsndisj  20860  neiptopnei  20917  rnelfm  21738  fmfnfmlem2  21740  fmfnfm  21743  flimss1  21758  isfcf  21819  cnextfun  21849  cnextfvval  21850  cnextf  21851  cnextcn  21852  cnextfres1  21853  ustuqtop1  22026  utopsnneiplem  22032  xblss2ps  22187  xblss2  22188  stdbdxmet  22301  metcnpi3  22332  metustexhalf  22342  nmoi  22513  nmoi2  22515  nmoco  22522  blcvx  22582  icccmplem2  22607  icccmplem3  22608  reconnlem2  22611  xrge0gsumle  22617  metds0  22634  metdstri  22635  metdseq0  22638  lebnumlem3  22743  nmoleub2lem  22895  bcthlem5  23106  minveclem2  23178  minveclem3b  23180  minveclem4  23184  minveclem6  23186  icombl  23313  cncombf  23406  mbflimsup  23414  itg2monolem1  23498  itg2mono  23501  itg2cnlem1  23509  itg2cnlem2  23510  bddmulibl  23586  ellimc2  23622  cpnord  23679  cpnres  23681  dvmulbr  23683  dvcobr  23690  dvlipcn  23738  dvlip2  23739  c1liplem1  23740  dvivthlem1  23752  lhop1lem  23757  lhop1  23758  dvfsumlem2  23771  itgsubstlem  23792  deg1add  23844  deg1sublt  23851  ply1remlem  23903  plyeq0lem  23947  taylthlem2  24109  ulmdvlem3  24137  abelthlem7  24173  pilem2  24187  pilem3  24188  pige3  24250  logccv  24390  cxpaddlelem  24473  cvxcl  24692  fsumharmonic  24719  ftalem5  24784  dvdsmulf1o  24901  bposlem1  24990  lgsqr  25057  lgsquad2lem2  25091  2lgsoddprmlem1  25114  2sqlem8a  25131  2sqlem8  25132  dchrmusum2  25164  dchrvmasumiflem1  25171  dchrisum0flblem1  25178  dchrisum0lem1b  25185  pntlem3  25279  tgdim01  25383  axsegcon  25788  ax5seglem1  25789  ax5seglem2  25790  axlowdimlem6  25808  axeuclidlem  25823  axcontlem7  25831  axcontlem9  25833  axcontlem10  25834  nbupgr  26221  nbumgrvtx  26223  cusgrsize2inds  26330  upgriswlk  26518  2pthnloop  26608  numclwwlk2lem1  27206  frgrreg  27222  nmoub3i  27598  ubthlem3  27698  minvecolem2  27701  minvecolem4  27706  minvecolem5  27707  minvecolem6  27708  htthlem  27744  pjpjpre  28248  chscllem1  28466  chscllem2  28467  chscllem3  28468  cnlnadjlem2  28897  leopnmid  28967  br8d  29394  ogrpaddlt  29692  archirngz  29717  ornglmullt  29781  orngrmullt  29782  elrhmunit  29794  qqhval2lem  29999  qqhnm  30008  qqhucn  30010  esumcst  30099  esumpcvgval  30114  measunl  30253  dya2iocbrsiga  30311  dya2icobrsiga  30312  omssubadd  30336  inelcarsg  30347  carsgclctunlem2  30355  sibfof  30376  sitgaddlemb  30384  oddpwdc  30390  eulerpartlemgc  30398  bayesth  30475  ftc2re  30650  breprexplemc  30684  tgoldbachgt  30715  erdszelem8  31154  br8  31621  noetalem3  31839  noetalem5  31841  matunitlindflem2  33377  totbndbnd  33559  prdsbnd  33563  rrncmslem  33602  rrntotbnd  33606  isdrngo2  33728  lsatcmp  34109  lcvexchlem2  34141  lcvexchlem3  34142  ncvr1  34378  cvrletrN  34379  cvrnbtwn3  34382  cvrnrefN  34388  cvrcmp  34389  0ltat  34397  atnle0  34415  atlen0  34416  cvlcvr1  34445  cvrval3  34518  atle  34541  athgt  34561  1cvratex  34578  ps-2  34583  ps-2b  34587  llnnleat  34618  2atneat  34620  llnle  34623  atcvrlln  34625  llncmp  34627  2llnmat  34629  2at0mat0  34630  2atm  34632  ps-2c  34633  lplnle  34645  lplnnle2at  34646  llncvrlpln2  34662  llncvrlpln  34663  2lplnmN  34664  2llnmj  34665  2atmat  34666  lplncmp  34667  lplnexllnN  34669  2llnm2N  34673  2llnm4  34675  lvolnle3at  34687  4atlem3a  34702  4atlem3b  34703  4atlem10  34711  4atlem11  34714  4atlem12  34717  lplncvrlvol2  34720  lplncvrlvol  34721  lvolcmp  34722  2lplnm2N  34726  2lplnmj  34727  dalempjsen  34758  dalemcea  34765  dalem2  34766  dalemdea  34767  dalem9  34777  dalem16  34784  dalemcjden  34797  dalem21  34799  dalem23  34801  dalem39  34816  dalem54  34831  dalem60  34837  cdlemb  34899  elpadd2at  34911  paddasslem4  34928  paddasslem7  34931  paddasslem15  34939  paddasslem16  34940  pmodlem1  34951  pmodlem2  34952  llnexchb2  34974  pclfinclN  35055  osumcllem9N  35069  pmapojoinN  35073  pexmidN  35074  pl42lem1N  35084  lhp0lt  35108  lhpexle1  35113  lhpexle2lem  35114  lhpexle3lem  35116  lhprelat3N  35145  ltrnid  35240  trlval3  35293  arglem1N  35296  cdlemc5  35301  cdleme3b  35335  cdleme3c  35336  cdleme3h  35341  cdleme7e  35353  cdleme7ga  35354  cdleme20l1  35427  cdleme20l2  35428  cdleme20l  35429  cdleme22b  35448  cdlemefrs29clN  35506  cdlemefrs32fva  35507  cdlemeg46fvcl  35613  cdlemeg46c  35620  cdlemeg46fvaw  35623  cdlemeg46req  35636  cdleme48fgv  35645  cdlemf1  35668  cdlemg1cex  35695  cdlemg2dN  35697  cdlemg2ce  35699  cdlemg12e  35754  cdlemg35  35820  cdlemh  35924  tendocan  35931  cdlemk28-3  36015  tendoex  36082  dih1  36394  dihmeetlem9N  36423  dihlspsnssN  36440  dihlspsnat  36441  lcfrlem23  36673  mzpsubst  37130  rencldnfi  37204  irrapx1  37211  pellexlem3  37214  pellexlem5  37216  infmrgelbi  37261  pellqrex  37262  pellfundge  37265  rmspecfund  37293  congtr  37351  acongeq  37369  jm2.20nn  37383  jm2.25lem1  37384  jm2.26  37388  expdiophlem1  37407  hbtlem2  37513  suprleubrd  38286  suprlubrd  38290  suprnmpt  39171  wessf1ornlem  39187  mpct  39209  upbdrech  39332  ssfiunibd  39336  uzfissfz  39355  xleadd2d  39356  suprltrp  39357  xleadd1d  39358  suprleubrnmpt  39462  iccintsng  39552  limcrecl  39661  fnlimfvre  39706  dvmulcncf  39903  dvdivcncf  39905  dvbdfbdioolem1  39906  ioodvbdlimc1lem2  39910  ioodvbdlimc2lem  39912  stoweidlem1  39981  stoweidlem20  40000  stoweidlem24  40004  stoweidlem34  40014  stoweidlem45  40025  stoweidlem60  40040  fourierdlem20  40107  fourierdlem31  40118  fourierdlem38  40125  fourierdlem64  40150  fourierdlem79  40165  fourierdlem94  40180  fourierdlem113  40199  fouriersw  40211  fouriercn  40212  sge0isum  40407  hoicvr  40525  ovnsubaddlem2  40548  hoidmv1lelem1  40568  hoidmv1lelem3  40570  hoidmvlelem1  40572  hoidmvlelem4  40575  smflimlem2  40743  pfxfv  41164  fmtnof1  41212  lighneallem2  41288  upgrwlkupwlk  41486  lincresunit3  42035  elbigolo1  42116
  Copyright terms: Public domain W3C validator