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

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

Proof of Theorem syl112anc
StepHypRef Expression
1 syl3anc.1 . 2 (𝜑𝜓)
2 syl3anc.2 . 2 (𝜑𝜒)
3 syl3anc.3 . . 3 (𝜑𝜃)
4 syl3Xanc.4 . . 3 (𝜑𝜏)
53, 4jca 512 . 2 (𝜑 → (𝜃𝜏))
6 syl112anc.5 . 2 ((𝜓𝜒 ∧ (𝜃𝜏)) → 𝜂)
71, 2, 5, 6syl3anc 1363 1 (𝜑𝜂)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  rmob2  3875  2nreu  4391  fveqf1o  7049  enfixsn  8615  gruina  10229  grur1  10231  enqeq  10345  recrec  11326  rec11r  11328  divdivdiv  11330  dmdcan  11339  ddcan  11343  rereccl  11347  div2neg  11352  divmuld  11427  divmul2d  11438  divmul3d  11439  divassd  11440  div12d  11441  div23d  11442  divdird  11443  divsubdird  11444  div11d  11445  ltmul12a  11485  ltdiv1  11493  ltrec  11511  lt2msq1  11513  lediv2  11519  supmul1  11599  qbtwnre  12582  xlemul1a  12671  xlemul1  12673  xadd4d  12686  quoremz  13213  quoremnn0ALT  13215  expgt1  13457  nnlesq  13558  expnbnd  13583  expmulnbnd  13586  discr1  13590  facubnd  13650  hashf1lem1  13803  pfxsuffeqwrdeq  14050  sqrlem6  14597  mulcn2  14942  geomulcvg  15222  cvgrat  15229  eftlub  15452  eflegeo  15464  tanhlt1  15503  sin01bnd  15528  cos01bnd  15529  eirrlem  15547  bitsmod  15775  mulgcd  15886  mulgcddvds  15989  prmind2  16019  qnumgt0  16080  pcpremul  16170  fldivp1  16223  pcfaclem  16224  qexpz  16227  prmpwdvds  16230  pockthg  16232  prmreclem1  16242  prmreclem5  16246  4sqlem10  16273  4sqlem12  16282  4sqlem16  16286  4sqlem17  16287  vdwlem3  16309  vdwlem8  16314  vdwlem9  16315  0ram  16346  ramz2  16350  odmulg  18614  dfod2  18622  odf1o1  18628  odf1o2  18629  sylow3lem4  18686  ablsub4  18864  odadd1  18899  odadd2  18900  ablfacrp2  19120  ablfac1b  19123  ablfac1eu  19126  pgpfac1lem3a  19129  pgpfaclem2  19135  ablsimpgfindlem1  19160  chrcong  20606  znrrg  20642  cygznlem1  20643  chpdmatlem3  21378  txdis  22170  txdis1cn  22173  ptunhmeo  22346  qustgplem  22658  blcld  23044  nlmvscnlem2  23223  blcvx  23335  metds0  23387  metdseq0  23391  icopnfcnv  23475  lebnumii  23499  ipcau2  23766  tcphcphlem1  23767  ipcnlem2  23776  csbren  23931  trirn  23932  dyadf  24121  dyadovol  24123  dyaddisjlem  24125  dyadmaxlem  24127  opnmbllem  24131  mbfmulc2lem  24177  mbfi1fseqlem4  24248  mbfi1fseqlem5  24249  mbfi1fseqlem6  24250  itg2mulclem  24276  itg2monolem1  24280  itg2monolem3  24282  itg2cnlem2  24292  itgabs  24364  dvlip  24519  dvlt0  24531  dvcvx  24546  ftc1lem4  24565  dgrcolem2  24793  aaliou3lem2  24861  aaliou3lem9  24868  itgulm  24925  radcnvlem1  24930  abelthlem2  24949  abelthlem7  24955  tangtx  25020  cosne0  25041  cosordlem  25042  tanord1  25048  logdivlti  25130  logcnlem4  25155  logf1o2  25160  cxpcn3lem  25255  cxpaddle  25260  ang180lem2  25315  atanlogsublem  25420  atantan  25428  atanbndlem  25430  atans2  25436  leibpi  25448  log2tlbnd  25451  birthdaylem3  25459  efrlim  25475  jensenlem2  25493  zetacvg  25520  ftalem1  25578  ftalem5  25582  basellem1  25586  basellem4  25589  fsumdvdsdiaglem  25688  dvdsflf1o  25692  fsumfldivdiaglem  25694  ppiub  25708  mersenne  25731  dchrptlem1  25768  bposlem1  25788  bposlem2  25789  bposlem4  25791  lgsdilem  25828  lgseisenlem1  25879  lgseisenlem2  25880  lgseisenlem3  25881  lgsquadlem1  25884  lgsquadlem2  25885  2sqlem3  25924  2sqlem8  25930  2sqlem11  25933  2sqblem  25935  chebbnd1lem2  25974  chebbnd1lem3  25975  rplogsumlem1  25988  rplogsumlem2  25989  dchrisumlem1  25993  dchrmusum2  25998  dchrisum0flblem1  26012  mulog2sumlem1  26038  logdivbnd  26060  pntpbnd1a  26089  pntpbnd1  26090  pntpbnd2  26091  pntlemh  26103  pntlemr  26106  pntlemk  26110  pntlemo  26111  ostth2lem1  26122  ostth2lem2  26138  ostth2lem3  26139  ostth3  26142  legov  26299  axsegcon  26641  axpaschlem  26654  0uhgrsubgr  26989  clwwlkf1  27756  upgr4cycl4dv4e  27892  eupth2lem3lem3  27937  nmblolbii  28504  nmbdoplbi  29729  nmcoplbi  29733  nmophmi  29736  nmbdfnlbi  29754  nmcfnlbi  29757  cnlnadjlem7  29778  nmopcoi  29800  resf1o  30393  xdivrec  30531  cycpmfvlem  30682  cycpmfv3  30685  lbsdiflsp0  30922  txomap  30998  unitdivcld  31044  measvunilem  31371  measvuni  31373  measssd  31374  measiuns  31376  measinblem  31379  measdivcst  31383  sibfof  31498  oddpwdc  31512  sseqfv1  31547  sseqfv2  31552  probun  31577  totprobd  31584  dstrvprob  31629  actfunsnrndisj  31776  reprsuc  31786  breprexplema  31801  subfaclim  32333  connpconn  32380  cvmliftlem2  32431  cvmliftlem6  32435  cvmliftlem7  32436  cvmliftlem8  32437  cvmliftlem9  32438  cvmliftlem10  32439  snmlff  32474  frrlem12  33032  noextenddif  33073  noextendlt  33074  noextendgt  33075  nosupbnd1lem3  33108  nosupbnd1lem4  33109  nosupbnd1lem5  33110  nosupbnd1lem6  33111  noetalem3  33117  lineext  33435  hilbert1.1  33513  nn0prpwlem  33568  poimirlem1  34775  opnmbllem0  34810  ismblfin  34815  itgabsnc  34843  ftc1cnnclem  34847  bfplem1  34983  bfp  34985  lfl1  36088  lfladdcl  36089  eqlkr  36117  lkrlsp  36120  atcvrj2b  36450  3dim1  36485  3dim2  36486  llni2  36530  2llnjaN  36584  lvoli3  36595  lvoli2  36599  lncvrelatN  36799  lhpat4N  37062  lhpat3  37064  4atexlemex6  37092  ldilco  37134  ltrnid  37153  ltrnatb  37155  ltrnel  37157  ltrncnvel  37160  ltrncnv  37164  ltrn11at  37165  ltrneq  37167  trlat  37187  trlator0  37189  ltrnnidn  37192  trlid0  37194  trlnidatb  37195  trlnle  37204  trlval3  37205  trlval4  37206  cdlemc2  37210  cdlemc5  37213  cdlemc6  37214  cdlemc  37215  cdlemd2  37217  cdlemd9  37224  cdleme0e  37235  cdleme02N  37240  cdleme0ex1N  37241  cdleme3e  37250  cdleme3g  37252  cdleme3h  37253  cdleme3  37255  cdleme7aa  37260  cdleme7b  37262  cdleme7c  37263  cdleme7d  37264  cdleme7e  37265  cdleme7ga  37266  cdleme7  37267  cdleme9  37271  cdleme16aN  37277  cdleme11c  37279  cdleme11dN  37280  cdleme11e  37281  cdleme11h  37284  cdleme11j  37285  cdleme11k  37286  cdleme12  37289  cdleme21j  37354  cdleme26eALTN  37379  cdleme26f  37381  cdleme26f2  37383  cdlemefrs29bpre0  37414  cdleme35a  37466  cdleme35b  37468  cdleme35c  37469  cdleme35f  37472  cdleme36a  37478  cdleme38m  37481  cdlemeg46rgv  37546  cdlemeg46req  37547  cdlemf  37581  cdlemg2fvlem  37612  cdlemg2l  37621  cdlemg7N  37644  cdlemg12g  37667  cdlemg15  37674  cdlemg17h  37686  cdlemg17  37695  cdlemg19a  37701  cdlemg24  37706  cdlemg37  37707  cdlemg27a  37710  cdlemg31b0N  37712  cdlemg27b  37714  cdlemg31c  37717  cdlemg31d  37718  cdlemg35  37731  trljco  37758  tgrpgrplem  37767  cdlemh2  37834  tendoconid  37847  tendotr  37848  cdlemk35s-id  37956  cdlemk39s-id  37958  cdlemk53b  37974  cdlemk53  37975  cdlemk54  37976  cdleml3N  37996  cdleml5N  37998  tendospcanN  38041  diclss  38211  dihvalcq2  38265  dihord4  38276  dihord5b  38277  dihord5apre  38280  dihmeetlem1N  38308  dihmeetbclemN  38322  dihmeetlem20N  38344  dihmeetALTN  38345  dihatlat  38352  dihatexv  38356  dochkr1  38496  dochkr1OLDN  38497  lcfl7lem  38517  lclkrlem2m  38537  hdmaplna1  38925  hdmaplns1  38926  hdmaplnm1  38927  eldioph2lem1  39237  fphpdo  39294  irrapxlem1  39299  irrapxlem2  39300  irrapxlem3  39301  irrapxlem5  39303  pellexlem2  39307  pell1234qrreccl  39331  pell1234qrmulcl  39332  pell1234qrdich  39338  pell1qr1  39348  pellqrexplicit  39354  pellfundex  39363  reglogltb  39368  reglogleb  39369  pellfund14  39375  rmxycomplete  39394  jm2.24nn  39436  jm2.17b  39438  jm2.17c  39439  jm2.18  39465  jm2.19lem2  39467  jm2.20nn  39474  jm2.16nn0  39481  jm3.1lem2  39495  areaquad  39703  clsk3nimkb  40270  lemuldiv3d  40403  lemuldiv4d  40404  stoweidlem1  42167  stoweidlem11  42177  stoweidlem14  42180  stoweidlem26  42192  stoweidlem34  42200  stoweidlem38  42204  stoweidlem60  42226  fourierdlem52  42324  etransclem38  42438  reuopreuprim  43535  quad1  43632  requad1  43634  requad2  43635  domnmsuppn0  44315  lincvalpr  44371  ldepspr  44426  islindeps2  44436  fldivexpfllog2  44523  eenglngeehlnmlem1  44622  eenglngeehlnmlem2  44623  rrx2linest  44627
  Copyright terms: Public domain W3C validator