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

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

Proof of Theorem syl131anc
StepHypRef Expression
1 syl3anc.1 . 2 (𝜑𝜓)
2 syl3anc.2 . . 3 (𝜑𝜒)
3 syl3anc.3 . . 3 (𝜑𝜃)
4 syl3Xanc.4 . . 3 (𝜑𝜏)
52, 3, 43jca 1124 . 2 (𝜑 → (𝜒𝜃𝜏))
6 syl23anc.5 . 2 (𝜑𝜂)
7 syl131anc.6 . 2 ((𝜓 ∧ (𝜒𝜃𝜏) ∧ 𝜂) → 𝜁)
81, 5, 6, 7syl3anc 1367 1 (𝜑𝜁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1083
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 209  df-an 399  df-3an 1085
This theorem is referenced by:  syl132anc  1384  syl231anc  1386  syl133anc  1389  initoeu2lem1  17253  estrres  17368  mulgdir  18238  umgr2edg  26978  2pthfrgr  28048  omndadd2d  30717  omndadd2rd  30718  submomnd  30719  omndmul2  30721  omndmul3  30722  ogrpinv0le  30724  ogrpsub  30725  ogrpaddltbi  30727  ogrpaddltrd  30728  ogrpinv0lt  30731  isarchi3  30824  archirngz  30826  archiabllem1a  30828  archiabllem1b  30829  archiabllem2a  30831  archiabllem2c  30832  orngsqr  30885  ornglmulle  30886  orngrmulle  30887  ofldchr  30895  lineext  33545  brsegle2  33578  cvrcmp  36455  cvrcmp2  36456  atcvreq0  36486  cvlatexch3  36510  cvlcvr1  36511  cvlsupr2  36515  cvlsupr7  36520  atnlej1  36551  atnlej2  36552  cvrval3  36585  ltltncvr  36595  atcvrneN  36602  atcvrj2b  36604  atbtwnex  36620  3noncolr2  36621  3noncolr1N  36622  4noncolr3  36625  3dimlem2  36631  3dimlem3a  36632  3dimlem3  36633  3dimlem3OLDN  36634  3dimlem4a  36635  3dimlem4  36636  3dimlem4OLDN  36637  ps-1  36649  hlatexch4  36653  3atlem1  36655  3atlem2  36656  3atlem3  36657  3atlem4  36658  3atlem5  36659  3atlem6  36660  3atlem7  36661  2llnmat  36696  ps-2c  36700  lplnri3N  36727  lplnexllnN  36736  2llnmeqat  36743  4atlem0a  36765  4atlem0ae  36766  4atlem0be  36767  4atlem9  36775  4atlem10a  36776  4atlem10b  36777  4atlem10  36778  4atlem11a  36779  4atlem11  36781  4atlem12a  36782  dalemcnes  36822  dalempnes  36823  dalemqnet  36824  dalem1  36831  dalemdea  36834  dalem3  36836  dalem5  36839  dalem-cly  36843  dalem27  36871  dalem28  36872  dalem41  36885  dalem45  36889  dalem48  36892  lneq2at  36950  2lnat  36956  2llnma1  36959  2llnma3r  36960  2llnma2  36961  cdlemblem  36965  paddasslem2  36993  pmodl42N  37023  hlmod1i  37028  atmod1i1m  37030  atmod2i1  37033  atmod2i2  37034  atmod3i1  37036  llnexchb2lem  37040  dalawlem2  37044  dalawlem3  37045  dalawlem6  37048  dalawlem7  37049  dalawlem11  37053  dalawlem12  37054  pexmidlem3N  37144  lhpexle3lem  37183  lhpmcvr3  37197  lhp2at0  37204  lhpelim  37209  lhpmod2i2  37210  lhpmod6i1  37211  4atexlempns  37234  4atexlemunv  37238  4atexlemc  37241  4atexlemnclw  37242  4atexlemex2  37243  4atexlemex6  37246  4atex  37248  4atex3  37253  trljat1  37338  trljat2  37339  ltrnatlw  37355  trlval4  37360  cdlemc1  37363  cdlemc3  37365  cdlemc6  37368  cdlemd3  37372  cdlemd4  37373  cdlemd5  37374  cdlemd6  37375  cdlemd7  37376  cdleme00a  37381  cdleme0cp  37386  cdleme0cq  37387  cdleme0e  37389  cdleme02N  37394  cdleme0ex2N  37396  cdleme0moN  37397  cdleme1  37399  cdleme2  37400  cdleme3e  37404  cdleme3g  37406  cdleme3h  37407  cdleme4  37410  cdleme5  37412  cdleme7aa  37414  cdleme7c  37417  cdleme7d  37418  cdleme7e  37419  cdleme8  37422  cdleme9  37425  cdleme10  37426  cdleme16aN  37431  cdleme11a  37432  cdleme11c  37433  cdleme11dN  37434  cdleme11e  37435  cdleme11g  37437  cdleme11h  37438  cdleme11j  37439  cdleme11k  37440  cdleme12  37443  cdleme15a  37446  cdleme15b  37447  cdleme16b  37451  cdleme17c  37460  cdleme0nex  37462  cdleme18d  37467  cdlemednpq  37471  cdleme20zN  37473  cdleme20y  37474  cdleme19a  37475  cdleme19d  37478  cdleme20aN  37481  cdleme20c  37483  cdleme20i  37489  cdleme20j  37490  cdleme21a  37497  cdleme21b  37498  cdleme21c  37499  cdleme21ct  37501  cdleme22cN  37514  cdleme22d  37515  cdleme22e  37516  cdleme22eALTN  37517  cdleme22f  37518  cdleme22f2  37519  cdleme22g  37520  cdleme23c  37523  cdleme41sn3a  37605  cdleme32le  37619  cdleme35b  37622  cdleme35c  37623  cdleme35d  37624  cdleme35e  37625  cdleme36a  37632  cdleme37m  37634  cdleme39a  37637  cdleme42a  37643  cdleme17d2  37667  cdlemeg46frv  37697  cdlemeg46rgv  37700  cdlemf1  37733  cdlemg2fv2  37772  cdlemg2l  37775  cdlemg2m  37776  cdlemg4d  37785  cdlemg4e  37786  cdlemg4f  37787  cdlemg4  37789  cdlemg6c  37792  cdlemg9a  37804  cdlemg10bALTN  37808  cdlemg12a  37815  cdlemg13  37824  cdlemg14f  37825  cdlemg14g  37826  cdlemg17i  37841  cdlemg17pq  37844  cdlemg19  37856  cdlemg21  37858  cdlemg27b  37868  cdlemg33c  37880  cdlemg33d  37881  trlcoabs2N  37894  cdlemg43  37902  cdlemg44b  37904  cdlemg44  37905  cdlemh1  37987  cdlemh2  37988  cdlemi1  37990  tendo0mul  37998  tendo0mulr  37999  cdlemk4  38006  cdlemk9  38011  cdlemk9bN  38012  cdlemk14  38026  cdlemkfid1N  38093  cdlemkid1  38094  cdlemk35s-id  38110  cdlemk39s-id  38112  cdlemk55a  38131  cdlemk55u  38138  cdlemk39u  38140  cdlemk19u  38142  cdlemk56  38143  cdleml8  38155  dia2dimlem1  38236  dia2dimlem2  38237  dia2dimlem3  38238  cdlemn10  38378  dihjust  38389  dihord1  38390  dihlsscpre  38406  dihvalcqpre  38407  dihglbcpreN  38472  dihmeetlem5  38480  dihmeetlem7N  38482  dihjatc1  38483  lincreslvec3  44682  isldepslvec2  44685
  Copyright terms: Public domain W3C validator