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

Theorem syl131anc 1381
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 1126 . 2 (𝜑 → (𝜒𝜃𝜏))
6 syl23anc.5 . 2 (𝜑𝜂)
7 syl131anc.6 . 2 ((𝜓 ∧ (𝜒𝜃𝜏) ∧ 𝜂) → 𝜁)
81, 5, 6, 7syl3anc 1369 1 (𝜑𝜁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1085
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 206  df-an 396  df-3an 1087
This theorem is referenced by:  syl132anc  1386  syl231anc  1388  syl133anc  1391  initoeu2lem1  17645  estrres  17772  mulgdir  18650  umgr2edg  27479  2pthfrgr  28549  omndadd2d  31236  omndadd2rd  31237  submomnd  31238  omndmul2  31240  omndmul3  31241  ogrpinv0le  31243  ogrpsub  31244  ogrpaddltbi  31246  ogrpaddltrd  31247  ogrpinv0lt  31250  isarchi3  31343  archirngz  31345  archiabllem1a  31347  archiabllem1b  31348  archiabllem2a  31350  archiabllem2c  31351  orngsqr  31405  ornglmulle  31406  orngrmulle  31407  ofldchr  31415  lineext  34305  brsegle2  34338  cvrcmp  37224  cvrcmp2  37225  atcvreq0  37255  cvlatexch3  37279  cvlcvr1  37280  cvlsupr2  37284  cvlsupr7  37289  atnlej1  37320  atnlej2  37321  cvrval3  37354  ltltncvr  37364  atcvrneN  37371  atcvrj2b  37373  atbtwnex  37389  3noncolr2  37390  3noncolr1N  37391  4noncolr3  37394  3dimlem2  37400  3dimlem3a  37401  3dimlem3  37402  3dimlem3OLDN  37403  3dimlem4a  37404  3dimlem4  37405  3dimlem4OLDN  37406  ps-1  37418  hlatexch4  37422  3atlem1  37424  3atlem2  37425  3atlem3  37426  3atlem4  37427  3atlem5  37428  3atlem6  37429  3atlem7  37430  2llnmat  37465  ps-2c  37469  lplnri3N  37496  lplnexllnN  37505  2llnmeqat  37512  4atlem0a  37534  4atlem0ae  37535  4atlem0be  37536  4atlem9  37544  4atlem10a  37545  4atlem10b  37546  4atlem10  37547  4atlem11a  37548  4atlem11  37550  4atlem12a  37551  dalemcnes  37591  dalempnes  37592  dalemqnet  37593  dalem1  37600  dalemdea  37603  dalem3  37605  dalem5  37608  dalem-cly  37612  dalem27  37640  dalem28  37641  dalem41  37654  dalem45  37658  dalem48  37661  lneq2at  37719  2lnat  37725  2llnma1  37728  2llnma3r  37729  2llnma2  37730  cdlemblem  37734  paddasslem2  37762  pmodl42N  37792  hlmod1i  37797  atmod1i1m  37799  atmod2i1  37802  atmod2i2  37803  atmod3i1  37805  llnexchb2lem  37809  dalawlem2  37813  dalawlem3  37814  dalawlem6  37817  dalawlem7  37818  dalawlem11  37822  dalawlem12  37823  pexmidlem3N  37913  lhpexle3lem  37952  lhpmcvr3  37966  lhp2at0  37973  lhpelim  37978  lhpmod2i2  37979  lhpmod6i1  37980  4atexlempns  38003  4atexlemunv  38007  4atexlemc  38010  4atexlemnclw  38011  4atexlemex2  38012  4atexlemex6  38015  4atex  38017  4atex3  38022  trljat1  38107  trljat2  38108  ltrnatlw  38124  trlval4  38129  cdlemc1  38132  cdlemc3  38134  cdlemc6  38137  cdlemd3  38141  cdlemd4  38142  cdlemd5  38143  cdlemd6  38144  cdlemd7  38145  cdleme00a  38150  cdleme0cp  38155  cdleme0cq  38156  cdleme0e  38158  cdleme02N  38163  cdleme0ex2N  38165  cdleme0moN  38166  cdleme1  38168  cdleme2  38169  cdleme3e  38173  cdleme3g  38175  cdleme3h  38176  cdleme4  38179  cdleme5  38181  cdleme7aa  38183  cdleme7c  38186  cdleme7d  38187  cdleme7e  38188  cdleme8  38191  cdleme9  38194  cdleme10  38195  cdleme16aN  38200  cdleme11a  38201  cdleme11c  38202  cdleme11dN  38203  cdleme11e  38204  cdleme11g  38206  cdleme11h  38207  cdleme11j  38208  cdleme11k  38209  cdleme12  38212  cdleme15a  38215  cdleme15b  38216  cdleme16b  38220  cdleme17c  38229  cdleme0nex  38231  cdleme18d  38236  cdlemednpq  38240  cdleme20zN  38242  cdleme20y  38243  cdleme19a  38244  cdleme19d  38247  cdleme20aN  38250  cdleme20c  38252  cdleme20i  38258  cdleme20j  38259  cdleme21a  38266  cdleme21b  38267  cdleme21c  38268  cdleme21ct  38270  cdleme22cN  38283  cdleme22d  38284  cdleme22e  38285  cdleme22eALTN  38286  cdleme22f  38287  cdleme22f2  38288  cdleme22g  38289  cdleme23c  38292  cdleme41sn3a  38374  cdleme32le  38388  cdleme35b  38391  cdleme35c  38392  cdleme35d  38393  cdleme35e  38394  cdleme36a  38401  cdleme37m  38403  cdleme39a  38406  cdleme42a  38412  cdleme17d2  38436  cdlemeg46frv  38466  cdlemeg46rgv  38469  cdlemf1  38502  cdlemg2fv2  38541  cdlemg2l  38544  cdlemg2m  38545  cdlemg4d  38554  cdlemg4e  38555  cdlemg4f  38556  cdlemg4  38558  cdlemg6c  38561  cdlemg9a  38573  cdlemg10bALTN  38577  cdlemg12a  38584  cdlemg13  38593  cdlemg14f  38594  cdlemg14g  38595  cdlemg17i  38610  cdlemg17pq  38613  cdlemg19  38625  cdlemg21  38627  cdlemg27b  38637  cdlemg33c  38649  cdlemg33d  38650  trlcoabs2N  38663  cdlemg43  38671  cdlemg44b  38673  cdlemg44  38674  cdlemh1  38756  cdlemh2  38757  cdlemi1  38759  tendo0mul  38767  tendo0mulr  38768  cdlemk4  38775  cdlemk9  38780  cdlemk9bN  38781  cdlemk14  38795  cdlemkfid1N  38862  cdlemkid1  38863  cdlemk35s-id  38879  cdlemk39s-id  38881  cdlemk55a  38900  cdlemk55u  38907  cdlemk39u  38909  cdlemk19u  38911  cdlemk56  38912  cdleml8  38924  dia2dimlem1  39005  dia2dimlem2  39006  dia2dimlem3  39007  cdlemn10  39147  dihjust  39158  dihord1  39159  dihlsscpre  39175  dihvalcqpre  39176  dihglbcpreN  39241  dihmeetlem5  39249  dihmeetlem7N  39251  dihjatc1  39252  lincreslvec3  45711  isldepslvec2  45714
  Copyright terms: Public domain W3C validator