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

Theorem syl6an 1411
 Description: A syllogism deduction combined with conjoining antecedents. (Contributed by Alan Sare, 28-Oct-2011.)
Hypotheses
Ref Expression
syl6an.1 (𝜑𝜓)
syl6an.2 (𝜑 → (𝜒𝜃))
syl6an.3 ((𝜓𝜃) → 𝜏)
Assertion
Ref Expression
syl6an (𝜑 → (𝜒𝜏))

Proof of Theorem syl6an
StepHypRef Expression
1 syl6an.2 . . 3 (𝜑 → (𝜒𝜃))
2 syl6an.1 . . 3 (𝜑𝜓)
31, 2jctild 314 . 2 (𝜑 → (𝜒 → (𝜓𝜃)))
4 syl6an.3 . 2 ((𝜓𝜃) → 𝜏)
53, 4syl6 33 1 (𝜑 → (𝜒𝜏))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107 This theorem is referenced by:  mapxpen  6749  prarloclem5  7331  ltsopr  7427  suplocsrlem  7639  nominpos  8980  ublbneg  9431  absle  10892  rexanre  11023  rexico  11024  climshftlemg  11102  serf0  11152  dvds1lem  11538  dvds2lem  11539  lmconst  12422  addcncntoplem  12757  bj-indind  13299
 Copyright terms: Public domain W3C validator