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

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

Proof of Theorem syl132anc
StepHypRef Expression
1 syl12anc.1 . 2 (𝜑𝜓)
2 syl12anc.2 . 2 (𝜑𝜒)
3 syl12anc.3 . 2 (𝜑𝜃)
4 syl22anc.4 . 2 (𝜑𝜏)
5 syl23anc.5 . . 3 (𝜑𝜂)
6 syl33anc.6 . . 3 (𝜑𝜁)
75, 6jca 554 . 2 (𝜑 → (𝜂𝜁))
8 syl132anc.7 . 2 ((𝜓 ∧ (𝜒𝜃𝜏) ∧ (𝜂𝜁)) → 𝜎)
91, 2, 3, 4, 7, 8syl131anc 1336 1 (𝜑𝜎)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
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 386  df-3an 1038
This theorem is referenced by:  drsdirfi  16866  eengtrkg  25778  eengtrkge  25779  qqhval2lem  29825  qqhghm  29832  qqhrhm  29833  btwncomim  31789  btwnswapid  31793  btwnintr  31795  btwnexch3  31796  btwnxfr  31832  linecgrand  31858  btwnconn1lem13  31875  seglecgr12im  31886  segletr  31890  linethru  31929  lshpkrlem5  33908  omlmod1i2N  34054  omlspjN  34055  atcmp  34105  atexchcvrN  34233  atbtwn  34239  1cvratlt  34267  2atjlej  34272  hlatexch3N  34273  hlatexch4  34274  atcvrlln2  34312  atcvrlln  34313  llncmp  34315  llncvrlpln  34351  lplncmp  34355  lplnexllnN  34357  2llnjaN  34359  4atlem11  34402  lplncvrlvol  34409  lvolcmp  34410  dalem1  34452  dalem2  34454  dalem24  34490  dalem25  34491  dalem42  34507  lncvrat  34575  2llnma3r  34581  lhp2lt  34794  4atexlemswapqr  34856  4atexlemtlw  34860  4atexlemntlpq  34861  4atexlemc  34862  4atexlemnclw  34863  4atexlemcnd  34865  4atex2  34870  cdlemd1  34992  cdlemd7  34998  cdleme0e  35011  cdleme7c  35039  cdleme7d  35040  cdleme7e  35041  cdleme7ga  35042  cdleme7  35043  cdleme16aN  35053  cdleme11c  35055  cdleme11e  35057  cdleme11l  35063  cdleme11  35064  cdleme14  35067  cdleme15a  35068  cdleme16b  35073  cdleme16c  35074  cdleme16d  35075  cdleme16e  35076  cdleme16f  35077  cdleme18b  35086  cdleme19d  35101  cdleme20d  35107  cdleme20f  35109  cdleme20h  35111  cdleme20l1  35115  cdleme20l2  35116  cdleme20l  35117  cdleme21a  35120  cdleme21b  35121  cdleme21c  35122  cdleme21ct  35124  cdleme22f2  35142  cdleme22g  35143  cdlemefr32sn2aw  35199  cdleme43fsv1snlem  35215  cdleme32b  35237  cdleme35a  35243  cdleme35f  35249  cdleme36m  35256  cdleme37m  35257  cdleme42k  35279  cdleme43bN  35285  cdleme17d2  35290  cdlemeg46req  35324  cdlemeg46gfv  35325  cdlemeg46gfre  35327  cdleme50trn2a  35345  cdleme50trn2  35346  cdlemg8b  35423  cdlemg10a  35435  cdlemg12d  35441  cdlemg13a  35446  cdlemg15  35451  cdlemg16z  35454  cdlemg18b  35474  cdlemg18c  35475  cdlemg18  35477  cdlemg27b  35491  cdlemg33  35506  cdlemg42  35524  trljco  35535  cdlemj3  35618  tendoid0  35620  cdlemk3  35628  cdlemk22  35688  cdlemk36  35708  cdlemkfid3N  35720  cdlemk47  35744  cdlemk48  35745  cdlemk49  35746  cdlemk50  35747  cdlemk51  35748  cdlemk52  35749  cdlemk53a  35750  cdlemk53b  35751  cdlemk53  35752  cdlemk54  35753  cdlemk55  35756  cdlemk35u  35759  cdlemk39u1  35762  cdleml3N  35773
  Copyright terms: Public domain W3C validator