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

Theorem syl13anc 1137
 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 1084 . 2 (𝜑 → (𝜒𝜃𝜏))
6 syl13anc.5 . 2 ((𝜓 ∧ (𝜒𝜃𝜏)) → 𝜂)
71, 5, 6syl2anc 391 1 (𝜑𝜂)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ∧ w3a 885 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101 This theorem depends on definitions:  df-bi 110  df-3an 887 This theorem is referenced by:  syl23anc  1142  syl33anc  1150  caovassd  5660  caovcand  5663  caovordid  5667  caovordd  5669  caovdid  5676  caovdird  5679  swoer  6134  swoord1  6135  swoord2  6136  prarloclem3  6595  fzosubel3  9052  iseqsplit  9238  iseqcaopr  9242
 Copyright terms: Public domain W3C validator