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  3997  tfrlem1  6306  tfrcl  6362  mkvprop  7153  ccfunen  7260  caucvgprprlemval  7684  suplocsrlem  7804  peano5uzti  9357  zfz1iso  10814  lcmneg  12066  prmind2  12112  pcfac  12340  cnmpt12  13658  cnmpt22  13665  limccnp2lem  14016  2sqlem6  14327  2sqlem8  14330  sbthom  14634
  Copyright terms: Public domain W3C validator