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

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

Proof of Theorem syl131anc
StepHypRef Expression
1 syl12anc.1 . 2 (𝜑𝜓)
2 syl12anc.2 . . 3 (𝜑𝜒)
3 syl12anc.3 . . 3 (𝜑𝜃)
4 syl22anc.4 . . 3 (𝜑𝜏)
52, 3, 43jca 1240 . 2 (𝜑 → (𝜒𝜃𝜏))
6 syl23anc.5 . 2 (𝜑𝜂)
7 syl131anc.6 . 2 ((𝜓 ∧ (𝜒𝜃𝜏) ∧ 𝜂) → 𝜁)
81, 5, 6, 7syl3anc 1323 1 (𝜑𝜁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  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:  syl132anc  1341  syl231anc  1343  syl133anc  1346  initoeu2lem1  16585  estrres  16700  mulgdir  17494  2pthfrgr  27012  omndadd2d  29493  omndadd2rd  29494  submomnd  29495  omndmul2  29497  omndmul3  29498  ogrpinvOLD  29500  ogrpinv0le  29501  ogrpsub  29502  ogrpaddltbi  29504  ogrpaddltrd  29505  ogrpinv0lt  29508  isarchi3  29526  archirngz  29528  archiabllem1a  29530  archiabllem1b  29531  archiabllem2a  29533  archiabllem2c  29534  orngsqr  29589  ornglmulle  29590  orngrmulle  29591  ofldchr  29599  lineext  31825  brsegle2  31858  cvrcmp  34050  cvrcmp2  34051  atcvreq0  34081  cvlatexch3  34105  cvlcvr1  34106  cvlsupr2  34110  cvlsupr7  34115  atnlej1  34145  atnlej2  34146  cvrval3  34179  ltltncvr  34189  atcvrneN  34196  atcvrj2b  34198  atbtwnex  34214  3noncolr2  34215  3noncolr1N  34216  4noncolr3  34219  3dimlem2  34225  3dimlem3a  34226  3dimlem3  34227  3dimlem3OLDN  34228  3dimlem4a  34229  3dimlem4  34230  3dimlem4OLDN  34231  ps-1  34243  hlatexch4  34247  3atlem1  34249  3atlem2  34250  3atlem3  34251  3atlem4  34252  3atlem5  34253  3atlem6  34254  3atlem7  34255  2llnmat  34290  ps-2c  34294  lplnri3N  34321  lplnexllnN  34330  2llnmeqat  34337  4atlem0a  34359  4atlem0ae  34360  4atlem0be  34361  4atlem9  34369  4atlem10a  34370  4atlem10b  34371  4atlem10  34372  4atlem11a  34373  4atlem11  34375  4atlem12a  34376  dalemcnes  34416  dalempnes  34417  dalemqnet  34418  dalem1  34425  dalemdea  34428  dalem3  34430  dalem5  34433  dalem-cly  34437  dalem27  34465  dalem28  34466  dalem41  34479  dalem45  34483  dalem48  34486  lneq2at  34544  2lnat  34550  2llnma1  34553  2llnma3r  34554  2llnma2  34555  cdlemblem  34559  paddasslem2  34587  pmodl42N  34617  hlmod1i  34622  atmod1i1m  34624  atmod2i1  34627  atmod2i2  34628  atmod3i1  34630  llnexchb2lem  34634  dalawlem2  34638  dalawlem3  34639  dalawlem6  34642  dalawlem7  34643  dalawlem11  34647  dalawlem12  34648  pexmidlem3N  34738  lhpexle3lem  34777  lhpmcvr3  34791  lhp2at0  34798  lhpelim  34803  lhpmod2i2  34804  lhpmod6i1  34805  4atexlempns  34828  4atexlemunv  34832  4atexlemc  34835  4atexlemnclw  34836  4atexlemex2  34837  4atexlemex6  34840  4atex  34842  4atex3  34847  trljat1  34933  trljat2  34934  ltrnatlw  34950  trlval4  34955  cdlemc1  34958  cdlemc3  34960  cdlemc6  34963  cdlemd3  34967  cdlemd4  34968  cdlemd5  34969  cdlemd6  34970  cdlemd7  34971  cdleme00a  34976  cdleme0cp  34981  cdleme0cq  34982  cdleme0e  34984  cdleme02N  34989  cdleme0ex2N  34991  cdleme0moN  34992  cdleme1  34994  cdleme2  34995  cdleme3e  34999  cdleme3g  35001  cdleme3h  35002  cdleme4  35005  cdleme5  35007  cdleme7aa  35009  cdleme7c  35012  cdleme7d  35013  cdleme7e  35014  cdleme8  35017  cdleme9  35020  cdleme10  35021  cdleme16aN  35026  cdleme11a  35027  cdleme11c  35028  cdleme11dN  35029  cdleme11e  35030  cdleme11g  35032  cdleme11h  35033  cdleme11j  35034  cdleme11k  35035  cdleme12  35038  cdleme15a  35041  cdleme15b  35042  cdleme16b  35046  cdleme17c  35055  cdleme0nex  35057  cdleme18d  35062  cdlemednpq  35066  cdleme20zN  35068  cdleme20y  35069  cdleme20yOLD  35070  cdleme19a  35071  cdleme19d  35074  cdleme20aN  35077  cdleme20c  35079  cdleme20i  35085  cdleme20j  35086  cdleme21a  35093  cdleme21b  35094  cdleme21c  35095  cdleme21ct  35097  cdleme22cN  35110  cdleme22d  35111  cdleme22e  35112  cdleme22eALTN  35113  cdleme22f  35114  cdleme22f2  35115  cdleme22g  35116  cdleme23c  35119  cdleme41sn3a  35201  cdleme32le  35215  cdleme35b  35218  cdleme35c  35219  cdleme35d  35220  cdleme35e  35221  cdleme36a  35228  cdleme37m  35230  cdleme39a  35233  cdleme42a  35239  cdleme17d2  35263  cdlemeg46frv  35293  cdlemeg46rgv  35296  cdlemf1  35329  cdlemg2fv2  35368  cdlemg2l  35371  cdlemg2m  35372  cdlemg4d  35381  cdlemg4e  35382  cdlemg4f  35383  cdlemg4  35385  cdlemg6c  35388  cdlemg9a  35400  cdlemg10bALTN  35404  cdlemg12a  35411  cdlemg13  35420  cdlemg14f  35421  cdlemg14g  35422  cdlemg17i  35437  cdlemg17pq  35440  cdlemg19  35452  cdlemg21  35454  cdlemg27b  35464  cdlemg33c  35476  cdlemg33d  35477  trlcoabs2N  35490  cdlemg43  35498  cdlemg44b  35500  cdlemg44  35501  cdlemh1  35583  cdlemh2  35584  cdlemi1  35586  tendo0mul  35594  tendo0mulr  35595  cdlemk4  35602  cdlemk9  35607  cdlemk9bN  35608  cdlemk14  35622  cdlemkfid1N  35689  cdlemkid1  35690  cdlemk35s-id  35706  cdlemk39s-id  35708  cdlemk55a  35727  cdlemk55u  35734  cdlemk39u  35736  cdlemk19u  35738  cdlemk56  35739  cdleml8  35751  dia2dimlem1  35833  dia2dimlem2  35834  dia2dimlem3  35835  cdlemn10  35975  dihjust  35986  dihord1  35987  dihlsscpre  36003  dihvalcqpre  36004  dihglbcpreN  36069  dihmeetlem5  36077  dihmeetlem7N  36079  dihjatc1  36080  lincreslvec3  41559  isldepslvec2  41562
  Copyright terms: Public domain W3C validator