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

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

Proof of Theorem syl23anc
StepHypRef Expression
1 syl12anc.1 . . 3 (𝜑𝜓)
2 syl12anc.2 . . 3 (𝜑𝜒)
31, 2jca 553 . 2 (𝜑 → (𝜓𝜒))
4 syl12anc.3 . 2 (𝜑𝜃)
5 syl22anc.4 . 2 (𝜑𝜏)
6 syl23anc.5 . 2 (𝜑𝜂)
7 syl23anc.6 . 2 (((𝜓𝜒) ∧ (𝜃𝜏𝜂)) → 𝜁)
83, 4, 5, 6, 7syl13anc 1320 1 (𝜑𝜁)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031 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 196  df-an 385  df-3an 1033 This theorem is referenced by:  suppofss1d  7219  suppofss2d  7220  cnfcomlem  8479  ackbij1lem16  8940  div2subd  10730  symg2bas  17641  evl1expd  19530  psgndiflemA  19766  oftpos  20077  restopn2  20791  tsmsxp  21768  blcld  22120  metustexhalf  22171  cnllycmp  22563  dvlipcn  23561  tanregt0  24089  ostthlem1  25116  ax5seglem6  25614  axcontlem4  25647  axcontlem7  25650  wwlkextwrd  26256  pnfneige0  29325  qqhval2  29354  esumcocn  29469  carsgmon  29703  bnj1125  30314  heiborlem8  32787  2atjm  33749  1cvrat  33780  lvolnlelln  33888  lvolnlelpln  33889  4atlem3  33900  lplncvrlvol  33920  dalem39  34015  cdleme4a  34544  cdleme15  34583  cdleme16c  34585  cdleme19b  34610  cdleme19e  34613  cdleme20d  34618  cdleme20g  34621  cdleme20j  34624  cdleme20k  34625  cdleme20l2  34627  cdleme20l  34628  cdleme20m  34629  cdleme22e  34650  cdleme22eALTN  34651  cdleme22f  34652  cdleme27cl  34672  cdlemefr27cl  34709  mpaaeu  36739  wwlksnextwrd  41103
 Copyright terms: Public domain W3C validator