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

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

Proof of Theorem syl23anc
StepHypRef Expression
1 syl3anc.1 . . 3 (𝜑𝜓)
2 syl3anc.2 . . 3 (𝜑𝜒)
31, 2jca 511 . 2 (𝜑 → (𝜓𝜒))
4 syl3anc.3 . 2 (𝜑𝜃)
5 syl3Xanc.4 . 2 (𝜑𝜏)
6 syl23anc.5 . 2 (𝜑𝜂)
7 syl23anc.6 . 2 (((𝜓𝜒) ∧ (𝜃𝜏𝜂)) → 𝜁)
83, 4, 5, 6, 7syl13anc 1374 1 (𝜑𝜁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1087
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 207  df-an 396  df-3an 1089
This theorem is referenced by:  suppofss1d  8229  suppofss2d  8230  cnfcomlem  9739  ackbij1lem16  10274  div2subd  12093  symg2bas  19410  psgndiflemA  21619  evl1expd  22349  evls1maplmhm  22381  oftpos  22458  restopn2  23185  tsmsxp  24163  blcld  24518  cnllycmp  24988  dvlipcn  26033  tanregt0  26581  ostthlem1  27671  nosupbnd1lem1  27753  nosupbnd2  27761  noinfbnd1lem1  27768  noinfbnd2  27776  ax5seglem6  28949  axcontlem4  28982  axcontlem7  28985  wwlksnextwrd  29917  drngidlhash  33462  rhmpreimaprmidl  33479  qsdrngilem  33522  rsprprmprmidlb  33551  rprmirredb  33560  dfufd2lem  33577  lindsunlem  33675  lactlmhm  33685  pnfneige0  33950  qqhval2  33983  esumcocn  34081  carsgmon  34316  bnj1125  35006  heiborlem8  37825  2atjm  39447  1cvrat  39478  lvolnlelln  39586  lvolnlelpln  39587  4atlem3  39598  lplncvrlvol  39618  dalem39  39713  cdleme4a  40241  cdleme15  40280  cdleme16c  40282  cdleme19b  40306  cdleme19e  40309  cdleme20d  40314  cdleme20g  40317  cdleme20j  40320  cdleme20k  40321  cdleme20l2  40323  cdleme20l  40324  cdleme20m  40325  cdleme22e  40346  cdleme22eALTN  40347  cdleme22f  40348  cdleme27cl  40368  cdlemefr27cl  40405  mpaaeu  43162
  Copyright terms: Public domain W3C validator