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

Theorem syl23anc 1330
 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 554 . 2 (𝜑 → (𝜓𝜒))
4 syl12anc.3 . 2 (𝜑𝜃)
5 syl22anc.4 . 2 (𝜑𝜏)
6 syl23anc.5 . 2 (𝜑𝜂)
7 syl23anc.6 . 2 (((𝜓𝜒) ∧ (𝜃𝜏𝜂)) → 𝜁)
83, 4, 5, 6, 7syl13anc 1325 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:  suppofss1d  7284  suppofss2d  7285  cnfcomlem  8547  ackbij1lem16  9008  div2subd  10802  symg2bas  17746  evl1expd  19637  psgndiflemA  19875  oftpos  20186  restopn2  20900  tsmsxp  21877  blcld  22229  metustexhalf  22280  cnllycmp  22674  dvlipcn  23674  tanregt0  24202  ostthlem1  25229  ax5seglem6  25727  axcontlem4  25760  axcontlem7  25763  wwlksnextwrd  26674  pnfneige0  29797  qqhval2  29826  esumcocn  29941  carsgmon  30175  bnj1125  30795  heiborlem8  33276  2atjm  34238  1cvrat  34269  lvolnlelln  34377  lvolnlelpln  34378  4atlem3  34389  lplncvrlvol  34409  dalem39  34504  cdleme4a  35033  cdleme15  35072  cdleme16c  35074  cdleme19b  35099  cdleme19e  35102  cdleme20d  35107  cdleme20g  35110  cdleme20j  35113  cdleme20k  35114  cdleme20l2  35116  cdleme20l  35117  cdleme20m  35118  cdleme22e  35139  cdleme22eALTN  35140  cdleme22f  35141  cdleme27cl  35161  cdlemefr27cl  35198  mpaaeu  37228
 Copyright terms: Public domain W3C validator