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

Theorem syl3c 63
 Description: A syllogism inference combined with contraction. (Contributed by Alan Sare, 7-Jul-2011.)
Hypotheses
Ref Expression
syl3c.1 (𝜑𝜓)
syl3c.2 (𝜑𝜒)
syl3c.3 (𝜑𝜃)
syl3c.4 (𝜓 → (𝜒 → (𝜃𝜏)))
Assertion
Ref Expression
syl3c (𝜑𝜏)

Proof of Theorem syl3c
StepHypRef Expression
1 syl3c.3 . 2 (𝜑𝜃)
2 syl3c.1 . . 3 (𝜑𝜓)
3 syl3c.2 . . 3 (𝜑𝜒)
4 syl3c.4 . . 3 (𝜓 → (𝜒 → (𝜃𝜏)))
52, 3, 4sylc 62 . 2 (𝜑 → (𝜃𝜏))
61, 5mpd 13 1 (𝜑𝜏)
 Colors of variables: wff set class Syntax hints:   → wi 4 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7 This theorem is referenced by:  bilukdc  1375  disjiun  3934  tfrlem1  6217  tfrcl  6273  mkvprop  7051  ccfunen  7125  caucvgprprlemval  7549  suplocsrlem  7669  peano5uzti  9212  zfz1iso  10645  lcmneg  11827  prmind2  11873  cnmpt12  12531  cnmpt22  12538  limccnp2lem  12889  sbthom  13440
 Copyright terms: Public domain W3C validator