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

Theorem syl132anc 1382
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 512 . 2 (𝜑 → (𝜂𝜁))
8 syl132anc.7 . 2 ((𝜓 ∧ (𝜒𝜃𝜏) ∧ (𝜂𝜁)) → 𝜎)
91, 2, 3, 4, 7, 8syl131anc 1377 1 (𝜑𝜎)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1081
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 208  df-an 397  df-3an 1083
This theorem is referenced by:  drsdirfi  17538  eengtrkg  26686  eengtrkge  26687  linds2eq  30855  qqhval2lem  31108  qqhghm  31115  qqhrhm  31116  btwncomim  33358  btwnswapid  33362  btwnintr  33364  btwnexch3  33365  btwnxfr  33401  linecgrand  33427  btwnconn1lem13  33444  seglecgr12im  33455  segletr  33459  linethru  33498  lshpkrlem5  36117  omlmod1i2N  36263  omlspjN  36264  atcmp  36314  atexchcvrN  36443  atbtwn  36449  1cvratlt  36477  2atjlej  36482  hlatexch3N  36483  hlatexch4  36484  atcvrlln2  36522  atcvrlln  36523  llncmp  36525  llncvrlpln  36561  lplncmp  36565  lplnexllnN  36567  2llnjaN  36569  4atlem11  36612  lplncvrlvol  36619  lvolcmp  36620  dalem1  36662  dalem2  36664  dalem24  36700  dalem25  36701  dalem42  36717  lncvrat  36785  2llnma3r  36791  lhp2lt  37004  4atexlemswapqr  37066  4atexlemtlw  37070  4atexlemntlpq  37071  4atexlemc  37072  4atexlemnclw  37073  4atexlemcnd  37075  4atex2  37080  cdlemd1  37201  cdlemd7  37207  cdleme0e  37220  cdleme7c  37248  cdleme7d  37249  cdleme7e  37250  cdleme7ga  37251  cdleme7  37252  cdleme16aN  37262  cdleme11c  37264  cdleme11e  37266  cdleme11l  37272  cdleme11  37273  cdleme14  37276  cdleme15a  37277  cdleme16b  37282  cdleme16c  37283  cdleme16d  37284  cdleme16e  37285  cdleme16f  37286  cdleme18b  37295  cdleme19d  37309  cdleme20d  37315  cdleme20f  37317  cdleme20h  37319  cdleme20l1  37323  cdleme20l2  37324  cdleme20l  37325  cdleme21a  37328  cdleme21b  37329  cdleme21c  37330  cdleme21ct  37332  cdleme22f2  37350  cdleme22g  37351  cdlemefr32sn2aw  37407  cdleme43fsv1snlem  37423  cdleme32b  37445  cdleme35a  37451  cdleme35f  37457  cdleme36m  37464  cdleme37m  37465  cdleme42k  37487  cdleme43bN  37493  cdleme17d2  37498  cdlemeg46req  37532  cdlemeg46gfv  37533  cdlemeg46gfre  37535  cdleme50trn2a  37553  cdleme50trn2  37554  cdlemg8b  37631  cdlemg10a  37643  cdlemg12d  37649  cdlemg13a  37654  cdlemg15  37659  cdlemg16z  37662  cdlemg18b  37682  cdlemg18c  37683  cdlemg18  37685  cdlemg27b  37699  cdlemg33  37714  cdlemg42  37732  trljco  37743  cdlemj3  37826  tendoid0  37828  cdlemk3  37836  cdlemk22  37896  cdlemk36  37916  cdlemkfid3N  37928  cdlemk47  37952  cdlemk48  37953  cdlemk49  37954  cdlemk50  37955  cdlemk51  37956  cdlemk52  37957  cdlemk53a  37958  cdlemk53b  37959  cdlemk53  37960  cdlemk54  37961  cdlemk55  37964  cdlemk35u  37967  cdlemk39u1  37970  cdleml3N  37981
  Copyright terms: Public domain W3C validator