ILE Home 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