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

Theorem syl131anc 1490
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 1123 . 2 (𝜑 → (𝜒𝜃𝜏))
6 syl23anc.5 . 2 (𝜑𝜂)
7 syl131anc.6 . 2 ((𝜓 ∧ (𝜒𝜃𝜏) ∧ 𝜂) → 𝜁)
81, 5, 6, 7syl3anc 1477 1 (𝜑𝜁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1072
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 1074
This theorem is referenced by:  syl132anc  1495  syl231anc  1497  syl133anc  1500  initoeu2lem1  16885  estrres  17000  mulgdir  17794  2pthfrgr  27459  omndadd2d  30038  omndadd2rd  30039  submomnd  30040  omndmul2  30042  omndmul3  30043  ogrpinvOLD  30045  ogrpinv0le  30046  ogrpsub  30047  ogrpaddltbi  30049  ogrpaddltrd  30050  ogrpinv0lt  30053  isarchi3  30071  archirngz  30073  archiabllem1a  30075  archiabllem1b  30076  archiabllem2a  30078  archiabllem2c  30079  orngsqr  30134  ornglmulle  30135  orngrmulle  30136  ofldchr  30144  lineext  32510  brsegle2  32543  cvrcmp  35091  cvrcmp2  35092  atcvreq0  35122  cvlatexch3  35146  cvlcvr1  35147  cvlsupr2  35151  cvlsupr7  35156  atnlej1  35186  atnlej2  35187  cvrval3  35220  ltltncvr  35230  atcvrneN  35237  atcvrj2b  35239  atbtwnex  35255  3noncolr2  35256  3noncolr1N  35257  4noncolr3  35260  3dimlem2  35266  3dimlem3a  35267  3dimlem3  35268  3dimlem3OLDN  35269  3dimlem4a  35270  3dimlem4  35271  3dimlem4OLDN  35272  ps-1  35284  hlatexch4  35288  3atlem1  35290  3atlem2  35291  3atlem3  35292  3atlem4  35293  3atlem5  35294  3atlem6  35295  3atlem7  35296  2llnmat  35331  ps-2c  35335  lplnri3N  35362  lplnexllnN  35371  2llnmeqat  35378  4atlem0a  35400  4atlem0ae  35401  4atlem0be  35402  4atlem9  35410  4atlem10a  35411  4atlem10b  35412  4atlem10  35413  4atlem11a  35414  4atlem11  35416  4atlem12a  35417  dalemcnes  35457  dalempnes  35458  dalemqnet  35459  dalem1  35466  dalemdea  35469  dalem3  35471  dalem5  35474  dalem-cly  35478  dalem27  35506  dalem28  35507  dalem41  35520  dalem45  35524  dalem48  35527  lneq2at  35585  2lnat  35591  2llnma1  35594  2llnma3r  35595  2llnma2  35596  cdlemblem  35600  paddasslem2  35628  pmodl42N  35658  hlmod1i  35663  atmod1i1m  35665  atmod2i1  35668  atmod2i2  35669  atmod3i1  35671  llnexchb2lem  35675  dalawlem2  35679  dalawlem3  35680  dalawlem6  35683  dalawlem7  35684  dalawlem11  35688  dalawlem12  35689  pexmidlem3N  35779  lhpexle3lem  35818  lhpmcvr3  35832  lhp2at0  35839  lhpelim  35844  lhpmod2i2  35845  lhpmod6i1  35846  4atexlempns  35869  4atexlemunv  35873  4atexlemc  35876  4atexlemnclw  35877  4atexlemex2  35878  4atexlemex6  35881  4atex  35883  4atex3  35888  trljat1  35974  trljat2  35975  ltrnatlw  35991  trlval4  35996  cdlemc1  35999  cdlemc3  36001  cdlemc6  36004  cdlemd3  36008  cdlemd4  36009  cdlemd5  36010  cdlemd6  36011  cdlemd7  36012  cdleme00a  36017  cdleme0cp  36022  cdleme0cq  36023  cdleme0e  36025  cdleme02N  36030  cdleme0ex2N  36032  cdleme0moN  36033  cdleme1  36035  cdleme2  36036  cdleme3e  36040  cdleme3g  36042  cdleme3h  36043  cdleme4  36046  cdleme5  36048  cdleme7aa  36050  cdleme7c  36053  cdleme7d  36054  cdleme7e  36055  cdleme8  36058  cdleme9  36061  cdleme10  36062  cdleme16aN  36067  cdleme11a  36068  cdleme11c  36069  cdleme11dN  36070  cdleme11e  36071  cdleme11g  36073  cdleme11h  36074  cdleme11j  36075  cdleme11k  36076  cdleme12  36079  cdleme15a  36082  cdleme15b  36083  cdleme16b  36087  cdleme17c  36096  cdleme0nex  36098  cdleme18d  36103  cdlemednpq  36107  cdleme20zN  36109  cdleme20y  36110  cdleme19a  36111  cdleme19d  36114  cdleme20aN  36117  cdleme20c  36119  cdleme20i  36125  cdleme20j  36126  cdleme21a  36133  cdleme21b  36134  cdleme21c  36135  cdleme21ct  36137  cdleme22cN  36150  cdleme22d  36151  cdleme22e  36152  cdleme22eALTN  36153  cdleme22f  36154  cdleme22f2  36155  cdleme22g  36156  cdleme23c  36159  cdleme41sn3a  36241  cdleme32le  36255  cdleme35b  36258  cdleme35c  36259  cdleme35d  36260  cdleme35e  36261  cdleme36a  36268  cdleme37m  36270  cdleme39a  36273  cdleme42a  36279  cdleme17d2  36303  cdlemeg46frv  36333  cdlemeg46rgv  36336  cdlemf1  36369  cdlemg2fv2  36408  cdlemg2l  36411  cdlemg2m  36412  cdlemg4d  36421  cdlemg4e  36422  cdlemg4f  36423  cdlemg4  36425  cdlemg6c  36428  cdlemg9a  36440  cdlemg10bALTN  36444  cdlemg12a  36451  cdlemg13  36460  cdlemg14f  36461  cdlemg14g  36462  cdlemg17i  36477  cdlemg17pq  36480  cdlemg19  36492  cdlemg21  36494  cdlemg27b  36504  cdlemg33c  36516  cdlemg33d  36517  trlcoabs2N  36530  cdlemg43  36538  cdlemg44b  36540  cdlemg44  36541  cdlemh1  36623  cdlemh2  36624  cdlemi1  36626  tendo0mul  36634  tendo0mulr  36635  cdlemk4  36642  cdlemk9  36647  cdlemk9bN  36648  cdlemk14  36662  cdlemkfid1N  36729  cdlemkid1  36730  cdlemk35s-id  36746  cdlemk39s-id  36748  cdlemk55a  36767  cdlemk55u  36774  cdlemk39u  36776  cdlemk19u  36778  cdlemk56  36779  cdleml8  36791  dia2dimlem1  36873  dia2dimlem2  36874  dia2dimlem3  36875  cdlemn10  37015  dihjust  37026  dihord1  37027  dihlsscpre  37043  dihvalcqpre  37044  dihglbcpreN  37109  dihmeetlem5  37117  dihmeetlem7N  37119  dihjatc1  37120  lincreslvec3  42799  isldepslvec2  42802
  Copyright terms: Public domain W3C validator