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

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

Proof of Theorem syl112anc
StepHypRef Expression
1 syl12anc.1 . 2 (𝜑𝜓)
2 syl12anc.2 . 2 (𝜑𝜒)
3 syl12anc.3 . . 3 (𝜑𝜃)
4 syl22anc.4 . . 3 (𝜑𝜏)
53, 4jca 553 . 2 (𝜑 → (𝜃𝜏))
6 syl112anc.5 . 2 ((𝜓𝜒 ∧ (𝜃𝜏)) → 𝜂)
71, 2, 5, 6syl3anc 1366 1 (𝜑𝜂)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054
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 385  df-3an 1056
This theorem is referenced by:  rmob2  3564  fveqf1o  6597  enfixsn  8110  gruina  9678  grur1  9680  enqeq  9794  recrec  10760  rec11r  10762  divdivdiv  10764  dmdcan  10773  ddcan  10777  rereccl  10781  div2neg  10786  divmuld  10861  divmul2d  10872  divmul3d  10873  divassd  10874  div12d  10875  div23d  10876  divdird  10877  divsubdird  10878  div11d  10879  ltmul12a  10917  ltdiv1  10925  ltrec  10943  lt2msq1  10945  lediv2  10951  supmul1  11030  qbtwnre  12068  xlemul1a  12156  xlemul1  12158  xadd4d  12171  quoremz  12694  quoremnn0ALT  12696  expgt1  12938  nnlesq  13008  expnbnd  13033  expmulnbnd  13036  discr1  13040  facubnd  13127  hashf1lem1  13277  2swrdeqwrdeq  13499  sqrlem6  14032  mulcn2  14370  climcnds  14627  geomulcvg  14651  cvgrat  14659  eftlub  14883  eflegeo  14895  tanhlt1  14934  sin01bnd  14959  cos01bnd  14960  eirrlem  14976  bitsmod  15205  mulgcd  15312  mulgcddvds  15416  prmind2  15445  qnumgt0  15505  iserodd  15587  pcpremul  15595  fldivp1  15648  pcfaclem  15649  qexpz  15652  prmpwdvds  15655  pockthg  15657  prmreclem1  15667  prmreclem5  15671  4sqlem10  15698  4sqlem12  15707  4sqlem16  15711  4sqlem17  15712  vdwlem3  15734  vdwlem8  15739  vdwlem9  15740  0ram  15771  ramz2  15775  xpsc0  16267  xpsc1  16268  odmulg  18019  dfod2  18027  odf1o1  18033  odf1o2  18034  sylow3lem4  18091  ablsub4  18264  odadd1  18297  odadd2  18298  ablfacrp2  18512  ablfac1b  18515  ablfac1eu  18518  pgpfac1lem3a  18521  pgpfaclem2  18527  chrcong  19925  znrrg  19962  cygznlem1  19963  chpdmatlem3  20693  txdis  21483  txdis1cn  21486  ptunhmeo  21659  qustgplem  21971  blcld  22357  nlmvscnlem2  22536  blcvx  22648  metds0  22700  metdseq0  22704  icopnfcnv  22788  lebnumii  22812  ipcau2  23079  tchcphlem1  23080  ipcnlem2  23089  csbren  23228  trirn  23229  dyadf  23405  dyadovol  23407  dyaddisjlem  23409  dyadmaxlem  23411  opnmbllem  23415  mbfmulc2lem  23459  mbfi1fseqlem4  23530  mbfi1fseqlem5  23531  mbfi1fseqlem6  23532  itg2mulclem  23558  itg2monolem1  23562  itg2monolem3  23564  itg2cnlem2  23574  itgabs  23646  dvlip  23801  dvlt0  23813  dvcvx  23828  ftc1lem4  23847  dgrcolem2  24075  aaliou3lem2  24143  aaliou3lem9  24150  itgulm  24207  radcnvlem1  24212  abelthlem2  24231  abelthlem7  24237  tangtx  24302  cosne0  24321  cosordlem  24322  tanord1  24328  logdivlti  24411  logcnlem4  24436  logf1o2  24441  cxpcn3lem  24533  cxpaddle  24538  ang180lem2  24585  atanlogsublem  24687  atantan  24695  atanbndlem  24697  atans2  24703  leibpi  24714  log2tlbnd  24717  birthdaylem3  24725  efrlim  24741  jensenlem2  24759  zetacvg  24786  ftalem1  24844  ftalem5  24848  basellem1  24852  basellem4  24855  fsumdvdsdiaglem  24954  dvdsflf1o  24958  fsumfldivdiaglem  24960  ppiub  24974  mersenne  24997  dchrptlem1  25034  bposlem1  25054  bposlem2  25055  bposlem4  25057  lgsdilem  25094  lgseisenlem1  25145  lgseisenlem2  25146  lgseisenlem3  25147  lgsquadlem1  25150  lgsquadlem2  25151  2sqlem3  25190  2sqlem8  25196  2sqlem11  25199  2sqblem  25201  chebbnd1lem2  25204  chebbnd1lem3  25205  rplogsumlem1  25218  rplogsumlem2  25219  dchrisumlem1  25223  dchrmusum2  25228  dchrisum0flblem1  25242  mulog2sumlem1  25268  logdivbnd  25290  pntpbnd1a  25319  pntpbnd1  25320  pntpbnd2  25321  pntlemh  25333  pntlemr  25336  pntlemk  25340  pntlemo  25341  ostth2lem1  25352  ostth2lem2  25368  ostth2lem3  25369  ostth3  25372  legov  25525  axsegcon  25852  axpaschlem  25865  0uhgrsubgr  26216  clwwlkf1  27012  upgr4cycl4dv4e  27163  eupth2lem3lem3  27208  nmblolbii  27782  nmbdoplbi  29011  nmcoplbi  29015  nmophmi  29018  nmbdfnlbi  29036  nmcfnlbi  29039  cnlnadjlem7  29060  nmopcoi  29082  resf1o  29633  xdivrec  29763  txomap  30029  unitdivcld  30075  measvunilem  30403  measvuni  30405  measssd  30406  measiuns  30408  measinblem  30411  measdivcst  30416  sibfof  30530  oddpwdc  30544  sseqfv1  30579  sseqfv2  30584  probun  30609  totprobd  30616  dstrvprob  30661  actfunsnrndisj  30811  reprsuc  30821  breprexplema  30836  subfaclim  31296  connpconn  31343  cvmliftlem2  31394  cvmliftlem6  31398  cvmliftlem7  31399  cvmliftlem8  31400  cvmliftlem9  31401  cvmliftlem10  31402  snmlff  31437  noextenddif  31946  noextendlt  31947  noextendgt  31948  nosupbnd1lem3  31981  nosupbnd1lem4  31982  nosupbnd1lem5  31983  nosupbnd1lem6  31984  noetalem3  31990  lineext  32308  hilbert1.1  32386  nn0prpwlem  32442  poimirlem1  33540  opnmbllem0  33575  ismblfin  33580  itgabsnc  33609  ftc1cnnclem  33613  bfplem1  33751  bfp  33753  lfl1  34675  lfladdcl  34676  eqlkr  34704  lkrlsp  34707  atcvrj2b  35036  3dim1  35071  3dim2  35072  llni2  35116  2llnjaN  35170  lvoli3  35181  lvoli2  35185  lncvrelatN  35385  lhpat4N  35648  lhpat3  35650  4atexlemex6  35678  ldilco  35720  ltrnid  35739  ltrnatb  35741  ltrnel  35743  ltrncnvel  35746  ltrncnv  35750  ltrn11at  35751  ltrneq  35753  ltrnmwOLD  35756  trlat  35774  trlator0  35776  ltrnnidn  35779  trlid0  35781  trlnidatb  35782  trlnle  35791  trlval3  35792  trlval4  35793  cdlemc2  35797  cdlemc5  35800  cdlemc6  35801  cdlemc  35802  cdlemd2  35804  cdlemd9  35811  cdleme0e  35822  cdleme02N  35827  cdleme0ex1N  35828  cdleme3e  35837  cdleme3g  35839  cdleme3h  35840  cdleme3  35842  cdleme7aa  35847  cdleme7b  35849  cdleme7c  35850  cdleme7d  35851  cdleme7e  35852  cdleme7ga  35853  cdleme7  35854  cdleme9  35858  cdleme16aN  35864  cdleme11c  35866  cdleme11dN  35867  cdleme11e  35868  cdleme11h  35871  cdleme11j  35872  cdleme11k  35873  cdleme12  35876  cdleme21j  35941  cdleme26eALTN  35966  cdleme26f  35968  cdleme26f2  35970  cdlemefrs29bpre0  36001  cdleme35a  36053  cdleme35b  36055  cdleme35c  36056  cdleme35f  36059  cdleme36a  36065  cdleme38m  36068  cdlemeg46rgv  36133  cdlemeg46req  36134  cdlemf  36168  cdlemg2fvlem  36199  cdlemg2l  36208  cdlemg7N  36231  cdlemg12g  36254  cdlemg15  36261  cdlemg17h  36273  cdlemg17  36282  cdlemg19a  36288  cdlemg24  36293  cdlemg37  36294  cdlemg27a  36297  cdlemg31b0N  36299  cdlemg27b  36301  cdlemg31c  36304  cdlemg31d  36305  cdlemg35  36318  trljco  36345  tgrpgrplem  36354  cdlemh2  36421  tendoconid  36434  tendotr  36435  cdlemk35s-id  36543  cdlemk39s-id  36545  cdlemk53b  36561  cdlemk53  36562  cdlemk54  36563  cdleml3N  36583  cdleml5N  36585  tendospcanN  36629  diclss  36799  dihvalcq2  36853  dihord4  36864  dihord5b  36865  dihord5apre  36868  dihmeetlem1N  36896  dihmeetbclemN  36910  dihmeetlem20N  36932  dihmeetALTN  36933  dihatlat  36940  dihatexv  36944  dochkr1  37084  dochkr1OLDN  37085  lcfl7lem  37105  lclkrlem2m  37125  hdmaplna1  37516  hdmaplns1  37517  hdmaplnm1  37518  eldioph2lem1  37640  fphpdo  37698  irrapxlem1  37703  irrapxlem2  37704  irrapxlem3  37705  irrapxlem5  37707  pellexlem2  37711  pell1234qrreccl  37735  pell1234qrmulcl  37736  pell1234qrdich  37742  pell1qr1  37752  pellqrexplicit  37758  pellfundex  37767  reglogltb  37772  reglogleb  37773  pellfund14  37779  rmspecsqrtnqOLD  37788  rmxycomplete  37799  jm2.24nn  37843  jm2.17b  37845  jm2.17c  37846  jm2.18  37872  jm2.19lem2  37874  jm2.20nn  37881  jm2.16nn0  37888  jm3.1lem2  37902  areaquad  38119  clsk3nimkb  38655  lemuldiv3d  38789  lemuldiv4d  38790  stoweidlem1  40536  stoweidlem11  40546  stoweidlem14  40549  stoweidlem26  40561  stoweidlem34  40569  stoweidlem38  40573  stoweidlem60  40595  fourierdlem52  40693  etransclem38  40807  pfxsuffeqwrdeq  41731  domnmsuppn0  42475  lincvalpr  42532  ldepspr  42587  islindeps2  42597  fldivexpfllog2  42684
  Copyright terms: Public domain W3C validator