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

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

Proof of Theorem syl132anc
StepHypRef Expression
1 syl3anc.1 . 2 (𝜑𝜓)
2 syl3anc.2 . 2 (𝜑𝜒)
3 syl3anc.3 . 2 (𝜑𝜃)
4 syl3Xanc.4 . 2 (𝜑𝜏)
5 syl23anc.5 . . 3 (𝜑𝜂)
6 syl33anc.6 . . 3 (𝜑𝜁)
75, 6jca 503 . 2 (𝜑 → (𝜂𝜁))
8 syl132anc.7 . 2 ((𝜓 ∧ (𝜒𝜃𝜏) ∧ (𝜂𝜁)) → 𝜎)
91, 2, 3, 4, 7, 8syl131anc 1495 1 (𝜑𝜎)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  drsdirfi  17143  eengtrkg  26079  eengtrkge  26080  qqhval2lem  30350  qqhghm  30357  qqhrhm  30358  btwncomim  32441  btwnswapid  32445  btwnintr  32447  btwnexch3  32448  btwnxfr  32484  linecgrand  32510  btwnconn1lem13  32527  seglecgr12im  32538  segletr  32542  linethru  32581  lshpkrlem5  34894  omlmod1i2N  35040  omlspjN  35041  atcmp  35091  atexchcvrN  35220  atbtwn  35226  1cvratlt  35254  2atjlej  35259  hlatexch3N  35260  hlatexch4  35261  atcvrlln2  35299  atcvrlln  35300  llncmp  35302  llncvrlpln  35338  lplncmp  35342  lplnexllnN  35344  2llnjaN  35346  4atlem11  35389  lplncvrlvol  35396  lvolcmp  35397  dalem1  35439  dalem2  35441  dalem24  35477  dalem25  35478  dalem42  35494  lncvrat  35562  2llnma3r  35568  lhp2lt  35781  4atexlemswapqr  35843  4atexlemtlw  35847  4atexlemntlpq  35848  4atexlemc  35849  4atexlemnclw  35850  4atexlemcnd  35852  4atex2  35857  cdlemd1  35979  cdlemd7  35985  cdleme0e  35998  cdleme7c  36026  cdleme7d  36027  cdleme7e  36028  cdleme7ga  36029  cdleme7  36030  cdleme16aN  36040  cdleme11c  36042  cdleme11e  36044  cdleme11l  36050  cdleme11  36051  cdleme14  36054  cdleme15a  36055  cdleme16b  36060  cdleme16c  36061  cdleme16d  36062  cdleme16e  36063  cdleme16f  36064  cdleme18b  36073  cdleme19d  36087  cdleme20d  36093  cdleme20f  36095  cdleme20h  36097  cdleme20l1  36101  cdleme20l2  36102  cdleme20l  36103  cdleme21a  36106  cdleme21b  36107  cdleme21c  36108  cdleme21ct  36110  cdleme22f2  36128  cdleme22g  36129  cdlemefr32sn2aw  36185  cdleme43fsv1snlem  36201  cdleme32b  36223  cdleme35a  36229  cdleme35f  36235  cdleme36m  36242  cdleme37m  36243  cdleme42k  36265  cdleme43bN  36271  cdleme17d2  36276  cdlemeg46req  36310  cdlemeg46gfv  36311  cdlemeg46gfre  36313  cdleme50trn2a  36331  cdleme50trn2  36332  cdlemg8b  36409  cdlemg10a  36421  cdlemg12d  36427  cdlemg13a  36432  cdlemg15  36437  cdlemg16z  36440  cdlemg18b  36460  cdlemg18c  36461  cdlemg18  36463  cdlemg27b  36477  cdlemg33  36492  cdlemg42  36510  trljco  36521  cdlemj3  36604  tendoid0  36606  cdlemk3  36614  cdlemk22  36674  cdlemk36  36694  cdlemkfid3N  36706  cdlemk47  36730  cdlemk48  36731  cdlemk49  36732  cdlemk50  36733  cdlemk51  36734  cdlemk52  36735  cdlemk53a  36736  cdlemk53b  36737  cdlemk53  36738  cdlemk54  36739  cdlemk55  36742  cdlemk35u  36745  cdlemk39u1  36748  cdleml3N  36759
  Copyright terms: Public domain W3C validator