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

Theorem syl132anc 1494
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 501 . 2 (𝜑 → (𝜂𝜁))
8 syl132anc.7 . 2 ((𝜓 ∧ (𝜒𝜃𝜏) ∧ (𝜂𝜁)) → 𝜎)
91, 2, 3, 4, 7, 8syl131anc 1489 1 (𝜑𝜎)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1071
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 383  df-3an 1073
This theorem is referenced by:  drsdirfi  17139  eengtrkg  26079  eengtrkge  26080  qqhval2lem  30358  qqhghm  30365  qqhrhm  30366  btwncomim  32450  btwnswapid  32454  btwnintr  32456  btwnexch3  32457  btwnxfr  32493  linecgrand  32519  btwnconn1lem13  32536  seglecgr12im  32547  segletr  32551  linethru  32590  lshpkrlem5  34916  omlmod1i2N  35062  omlspjN  35063  atcmp  35113  atexchcvrN  35241  atbtwn  35247  1cvratlt  35275  2atjlej  35280  hlatexch3N  35281  hlatexch4  35282  atcvrlln2  35320  atcvrlln  35321  llncmp  35323  llncvrlpln  35359  lplncmp  35363  lplnexllnN  35365  2llnjaN  35367  4atlem11  35410  lplncvrlvol  35417  lvolcmp  35418  dalem1  35460  dalem2  35462  dalem24  35498  dalem25  35499  dalem42  35515  lncvrat  35583  2llnma3r  35589  lhp2lt  35802  4atexlemswapqr  35864  4atexlemtlw  35868  4atexlemntlpq  35869  4atexlemc  35870  4atexlemnclw  35871  4atexlemcnd  35873  4atex2  35878  cdlemd1  36000  cdlemd7  36006  cdleme0e  36019  cdleme7c  36047  cdleme7d  36048  cdleme7e  36049  cdleme7ga  36050  cdleme7  36051  cdleme16aN  36061  cdleme11c  36063  cdleme11e  36065  cdleme11l  36071  cdleme11  36072  cdleme14  36075  cdleme15a  36076  cdleme16b  36081  cdleme16c  36082  cdleme16d  36083  cdleme16e  36084  cdleme16f  36085  cdleme18b  36094  cdleme19d  36108  cdleme20d  36114  cdleme20f  36116  cdleme20h  36118  cdleme20l1  36122  cdleme20l2  36123  cdleme20l  36124  cdleme21a  36127  cdleme21b  36128  cdleme21c  36129  cdleme21ct  36131  cdleme22f2  36149  cdleme22g  36150  cdlemefr32sn2aw  36206  cdleme43fsv1snlem  36222  cdleme32b  36244  cdleme35a  36250  cdleme35f  36256  cdleme36m  36263  cdleme37m  36264  cdleme42k  36286  cdleme43bN  36292  cdleme17d2  36297  cdlemeg46req  36331  cdlemeg46gfv  36332  cdlemeg46gfre  36334  cdleme50trn2a  36352  cdleme50trn2  36353  cdlemg8b  36430  cdlemg10a  36442  cdlemg12d  36448  cdlemg13a  36453  cdlemg15  36458  cdlemg16z  36461  cdlemg18b  36481  cdlemg18c  36482  cdlemg18  36484  cdlemg27b  36498  cdlemg33  36513  cdlemg42  36531  trljco  36542  cdlemj3  36625  tendoid0  36627  cdlemk3  36635  cdlemk22  36695  cdlemk36  36715  cdlemkfid3N  36727  cdlemk47  36751  cdlemk48  36752  cdlemk49  36753  cdlemk50  36754  cdlemk51  36755  cdlemk52  36756  cdlemk53a  36757  cdlemk53b  36758  cdlemk53  36759  cdlemk54  36760  cdlemk55  36763  cdlemk35u  36766  cdlemk39u1  36769  cdleml3N  36780
  Copyright terms: Public domain W3C validator