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

Theorem syl2anc2 412
Description: Double syllogism inference combined with contraction. (Contributed by BTernaryTau, 29-Sep-2023.)
Hypotheses
Ref Expression
syl2anc2.1 (𝜑𝜓)
syl2anc2.2 (𝜓𝜒)
syl2anc2.3 ((𝜓𝜒) → 𝜃)
Assertion
Ref Expression
syl2anc2 (𝜑𝜃)

Proof of Theorem syl2anc2
StepHypRef Expression
1 syl2anc2.1 . 2 (𝜑𝜓)
2 syl2anc2.2 . . 3 (𝜓𝜒)
31, 2syl 14 . 2 (𝜑𝜒)
4 syl2anc2.3 . 2 ((𝜓𝜒) → 𝜃)
51, 3, 4syl2anc 411 1 (𝜑𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108
This theorem is referenced by:  0mhm  12750  grpidssd  12822  ringlz  13035  ringrz  13036
  Copyright terms: Public domain W3C validator