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  16865  estrres  16980  mulgdir  17774  2pthfrgr  27438  omndadd2d  30017  omndadd2rd  30018  submomnd  30019  omndmul2  30021  omndmul3  30022  ogrpinvOLD  30024  ogrpinv0le  30025  ogrpsub  30026  ogrpaddltbi  30028  ogrpaddltrd  30029  ogrpinv0lt  30032  isarchi3  30050  archirngz  30052  archiabllem1a  30054  archiabllem1b  30055  archiabllem2a  30057  archiabllem2c  30058  orngsqr  30113  ornglmulle  30114  orngrmulle  30115  ofldchr  30123  lineext  32489  brsegle2  32522  cvrcmp  35073  cvrcmp2  35074  atcvreq0  35104  cvlatexch3  35128  cvlcvr1  35129  cvlsupr2  35133  cvlsupr7  35138  atnlej1  35168  atnlej2  35169  cvrval3  35202  ltltncvr  35212  atcvrneN  35219  atcvrj2b  35221  atbtwnex  35237  3noncolr2  35238  3noncolr1N  35239  4noncolr3  35242  3dimlem2  35248  3dimlem3a  35249  3dimlem3  35250  3dimlem3OLDN  35251  3dimlem4a  35252  3dimlem4  35253  3dimlem4OLDN  35254  ps-1  35266  hlatexch4  35270  3atlem1  35272  3atlem2  35273  3atlem3  35274  3atlem4  35275  3atlem5  35276  3atlem6  35277  3atlem7  35278  2llnmat  35313  ps-2c  35317  lplnri3N  35344  lplnexllnN  35353  2llnmeqat  35360  4atlem0a  35382  4atlem0ae  35383  4atlem0be  35384  4atlem9  35392  4atlem10a  35393  4atlem10b  35394  4atlem10  35395  4atlem11a  35396  4atlem11  35398  4atlem12a  35399  dalemcnes  35439  dalempnes  35440  dalemqnet  35441  dalem1  35448  dalemdea  35451  dalem3  35453  dalem5  35456  dalem-cly  35460  dalem27  35488  dalem28  35489  dalem41  35502  dalem45  35506  dalem48  35509  lneq2at  35567  2lnat  35573  2llnma1  35576  2llnma3r  35577  2llnma2  35578  cdlemblem  35582  paddasslem2  35610  pmodl42N  35640  hlmod1i  35645  atmod1i1m  35647  atmod2i1  35650  atmod2i2  35651  atmod3i1  35653  llnexchb2lem  35657  dalawlem2  35661  dalawlem3  35662  dalawlem6  35665  dalawlem7  35666  dalawlem11  35670  dalawlem12  35671  pexmidlem3N  35761  lhpexle3lem  35800  lhpmcvr3  35814  lhp2at0  35821  lhpelim  35826  lhpmod2i2  35827  lhpmod6i1  35828  4atexlempns  35851  4atexlemunv  35855  4atexlemc  35858  4atexlemnclw  35859  4atexlemex2  35860  4atexlemex6  35863  4atex  35865  4atex3  35870  trljat1  35956  trljat2  35957  ltrnatlw  35973  trlval4  35978  cdlemc1  35981  cdlemc3  35983  cdlemc6  35986  cdlemd3  35990  cdlemd4  35991  cdlemd5  35992  cdlemd6  35993  cdlemd7  35994  cdleme00a  35999  cdleme0cp  36004  cdleme0cq  36005  cdleme0e  36007  cdleme02N  36012  cdleme0ex2N  36014  cdleme0moN  36015  cdleme1  36017  cdleme2  36018  cdleme3e  36022  cdleme3g  36024  cdleme3h  36025  cdleme4  36028  cdleme5  36030  cdleme7aa  36032  cdleme7c  36035  cdleme7d  36036  cdleme7e  36037  cdleme8  36040  cdleme9  36043  cdleme10  36044  cdleme16aN  36049  cdleme11a  36050  cdleme11c  36051  cdleme11dN  36052  cdleme11e  36053  cdleme11g  36055  cdleme11h  36056  cdleme11j  36057  cdleme11k  36058  cdleme12  36061  cdleme15a  36064  cdleme15b  36065  cdleme16b  36069  cdleme17c  36078  cdleme0nex  36080  cdleme18d  36085  cdlemednpq  36089  cdleme20zN  36091  cdleme20y  36092  cdleme19a  36093  cdleme19d  36096  cdleme20aN  36099  cdleme20c  36101  cdleme20i  36107  cdleme20j  36108  cdleme21a  36115  cdleme21b  36116  cdleme21c  36117  cdleme21ct  36119  cdleme22cN  36132  cdleme22d  36133  cdleme22e  36134  cdleme22eALTN  36135  cdleme22f  36136  cdleme22f2  36137  cdleme22g  36138  cdleme23c  36141  cdleme41sn3a  36223  cdleme32le  36237  cdleme35b  36240  cdleme35c  36241  cdleme35d  36242  cdleme35e  36243  cdleme36a  36250  cdleme37m  36252  cdleme39a  36255  cdleme42a  36261  cdleme17d2  36285  cdlemeg46frv  36315  cdlemeg46rgv  36318  cdlemf1  36351  cdlemg2fv2  36390  cdlemg2l  36393  cdlemg2m  36394  cdlemg4d  36403  cdlemg4e  36404  cdlemg4f  36405  cdlemg4  36407  cdlemg6c  36410  cdlemg9a  36422  cdlemg10bALTN  36426  cdlemg12a  36433  cdlemg13  36442  cdlemg14f  36443  cdlemg14g  36444  cdlemg17i  36459  cdlemg17pq  36462  cdlemg19  36474  cdlemg21  36476  cdlemg27b  36486  cdlemg33c  36498  cdlemg33d  36499  trlcoabs2N  36512  cdlemg43  36520  cdlemg44b  36522  cdlemg44  36523  cdlemh1  36605  cdlemh2  36606  cdlemi1  36608  tendo0mul  36616  tendo0mulr  36617  cdlemk4  36624  cdlemk9  36629  cdlemk9bN  36630  cdlemk14  36644  cdlemkfid1N  36711  cdlemkid1  36712  cdlemk35s-id  36728  cdlemk39s-id  36730  cdlemk55a  36749  cdlemk55u  36756  cdlemk39u  36758  cdlemk19u  36760  cdlemk56  36761  cdleml8  36773  dia2dimlem1  36855  dia2dimlem2  36856  dia2dimlem3  36857  cdlemn10  36997  dihjust  37008  dihord1  37009  dihlsscpre  37025  dihvalcqpre  37026  dihglbcpreN  37091  dihmeetlem5  37099  dihmeetlem7N  37101  dihjatc1  37102  lincreslvec3  42781  isldepslvec2  42784
  Copyright terms: Public domain W3C validator