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  3993  tfrlem1  6299  tfrcl  6355  mkvprop  7146  ccfunen  7238  caucvgprprlemval  7662  suplocsrlem  7782  peano5uzti  9332  zfz1iso  10788  lcmneg  12040  prmind2  12086  pcfac  12314  cnmpt12  13280  cnmpt22  13287  limccnp2lem  13638  2sqlem6  13949  2sqlem8  13952  sbthom  14257
  Copyright terms: Public domain W3C validator