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

Theorem syl132anc 1495
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 555 . 2 (𝜑 → (𝜂𝜁))
8 syl132anc.7 . 2 ((𝜓 ∧ (𝜒𝜃𝜏) ∧ (𝜂𝜁)) → 𝜎)
91, 2, 3, 4, 7, 8syl131anc 1490 1 (𝜑𝜎)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072
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 385  df-3an 1074
This theorem is referenced by:  drsdirfi  17139  eengtrkg  26064  eengtrkge  26065  qqhval2lem  30334  qqhghm  30341  qqhrhm  30342  btwncomim  32426  btwnswapid  32430  btwnintr  32432  btwnexch3  32433  btwnxfr  32469  linecgrand  32495  btwnconn1lem13  32512  seglecgr12im  32523  segletr  32527  linethru  32566  lshpkrlem5  34904  omlmod1i2N  35050  omlspjN  35051  atcmp  35101  atexchcvrN  35229  atbtwn  35235  1cvratlt  35263  2atjlej  35268  hlatexch3N  35269  hlatexch4  35270  atcvrlln2  35308  atcvrlln  35309  llncmp  35311  llncvrlpln  35347  lplncmp  35351  lplnexllnN  35353  2llnjaN  35355  4atlem11  35398  lplncvrlvol  35405  lvolcmp  35406  dalem1  35448  dalem2  35450  dalem24  35486  dalem25  35487  dalem42  35503  lncvrat  35571  2llnma3r  35577  lhp2lt  35790  4atexlemswapqr  35852  4atexlemtlw  35856  4atexlemntlpq  35857  4atexlemc  35858  4atexlemnclw  35859  4atexlemcnd  35861  4atex2  35866  cdlemd1  35988  cdlemd7  35994  cdleme0e  36007  cdleme7c  36035  cdleme7d  36036  cdleme7e  36037  cdleme7ga  36038  cdleme7  36039  cdleme16aN  36049  cdleme11c  36051  cdleme11e  36053  cdleme11l  36059  cdleme11  36060  cdleme14  36063  cdleme15a  36064  cdleme16b  36069  cdleme16c  36070  cdleme16d  36071  cdleme16e  36072  cdleme16f  36073  cdleme18b  36082  cdleme19d  36096  cdleme20d  36102  cdleme20f  36104  cdleme20h  36106  cdleme20l1  36110  cdleme20l2  36111  cdleme20l  36112  cdleme21a  36115  cdleme21b  36116  cdleme21c  36117  cdleme21ct  36119  cdleme22f2  36137  cdleme22g  36138  cdlemefr32sn2aw  36194  cdleme43fsv1snlem  36210  cdleme32b  36232  cdleme35a  36238  cdleme35f  36244  cdleme36m  36251  cdleme37m  36252  cdleme42k  36274  cdleme43bN  36280  cdleme17d2  36285  cdlemeg46req  36319  cdlemeg46gfv  36320  cdlemeg46gfre  36322  cdleme50trn2a  36340  cdleme50trn2  36341  cdlemg8b  36418  cdlemg10a  36430  cdlemg12d  36436  cdlemg13a  36441  cdlemg15  36446  cdlemg16z  36449  cdlemg18b  36469  cdlemg18c  36470  cdlemg18  36472  cdlemg27b  36486  cdlemg33  36501  cdlemg42  36519  trljco  36530  cdlemj3  36613  tendoid0  36615  cdlemk3  36623  cdlemk22  36683  cdlemk36  36703  cdlemkfid3N  36715  cdlemk47  36739  cdlemk48  36740  cdlemk49  36741  cdlemk50  36742  cdlemk51  36743  cdlemk52  36744  cdlemk53a  36745  cdlemk53b  36746  cdlemk53  36747  cdlemk54  36748  cdlemk55  36751  cdlemk35u  36754  cdlemk39u1  36757  cdleml3N  36768
  Copyright terms: Public domain W3C validator