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

Theorem syl23anc 1374
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 510 . 2 (𝜑 → (𝜓𝜒))
4 syl3anc.3 . 2 (𝜑𝜃)
5 syl3Xanc.4 . 2 (𝜑𝜏)
6 syl23anc.5 . 2 (𝜑𝜂)
7 syl23anc.6 . 2 (((𝜓𝜒) ∧ (𝜃𝜏𝜂)) → 𝜁)
83, 4, 5, 6, 7syl13anc 1369 1 (𝜑𝜁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  w3a 1084
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 206  df-an 395  df-3an 1086
This theorem is referenced by:  suppofss1d  8210  suppofss2d  8211  cnfcomlem  9724  ackbij1lem16  10260  div2subd  12073  symg2bas  19359  psgndiflemA  21550  evl1expd  22289  evls1maplmhm  22321  oftpos  22398  restopn2  23125  tsmsxp  24103  blcld  24458  cnllycmp  24926  dvlipcn  25971  tanregt0  26518  ostthlem1  27605  nosupbnd1lem1  27687  nosupbnd2  27695  noinfbnd1lem1  27702  noinfbnd2  27710  ax5seglem6  28817  axcontlem4  28850  axcontlem7  28853  wwlksnextwrd  29780  drngidlhash  33246  rhmpreimaprmidl  33263  qsdrngilem  33306  rsprprmprmidlb  33335  rprmirredb  33344  dfufd2lem  33364  lindsunlem  33453  pnfneige0  33683  qqhval2  33714  esumcocn  33830  carsgmon  34065  bnj1125  34754  heiborlem8  37422  2atjm  39048  1cvrat  39079  lvolnlelln  39187  lvolnlelpln  39188  4atlem3  39199  lplncvrlvol  39219  dalem39  39314  cdleme4a  39842  cdleme15  39881  cdleme16c  39883  cdleme19b  39907  cdleme19e  39910  cdleme20d  39915  cdleme20g  39918  cdleme20j  39921  cdleme20k  39922  cdleme20l2  39924  cdleme20l  39925  cdleme20m  39926  cdleme22e  39947  cdleme22eALTN  39948  cdleme22f  39949  cdleme27cl  39969  cdlemefr27cl  40006  mpaaeu  42716
  Copyright terms: Public domain W3C validator