ILE Home 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  1396  disjiun  4000  tfrlem1  6311  tfrcl  6367  mkvprop  7158  ccfunen  7265  caucvgprprlemval  7689  suplocsrlem  7809  peano5uzti  9363  zfz1iso  10823  lcmneg  12076  prmind2  12122  pcfac  12350  cnmpt12  13826  cnmpt22  13833  limccnp2lem  14184  2sqlem6  14506  2sqlem8  14509  sbthom  14813
  Copyright terms: Public domain W3C validator