ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  syl13anc GIF version

Theorem syl13anc 1174
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
sylXanc.1 (𝜑𝜓)
sylXanc.2 (𝜑𝜒)
sylXanc.3 (𝜑𝜃)
sylXanc.4 (𝜑𝜏)
syl13anc.5 ((𝜓 ∧ (𝜒𝜃𝜏)) → 𝜂)
Assertion
Ref Expression
syl13anc (𝜑𝜂)

Proof of Theorem syl13anc
StepHypRef Expression
1 sylXanc.1 . 2 (𝜑𝜓)
2 sylXanc.2 . . 3 (𝜑𝜒)
3 sylXanc.3 . . 3 (𝜑𝜃)
4 sylXanc.4 . . 3 (𝜑𝜏)
52, 3, 43jca 1121 . 2 (𝜑 → (𝜒𝜃𝜏))
6 syl13anc.5 . 2 ((𝜓 ∧ (𝜒𝜃𝜏)) → 𝜂)
71, 5, 6syl2anc 403 1 (𝜑𝜂)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  w3a 922
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115  df-3an 924
This theorem is referenced by:  syl23anc  1179  syl33anc  1187  caovassd  5761  caovcand  5764  caovordid  5768  caovordd  5770  caovdid  5777  caovdird  5780  swoer  6272  swoord1  6273  swoord2  6274  fimax2gtrilemstep  6568  suplub2ti  6640  prarloclem3  7000  fzosubel3  9535  iseqsplit  9813  iseqcaopr  9817  zisum  10665  divalglemex  10804
  Copyright terms: Public domain W3C validator