ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  4syl Unicode version

Theorem 4syl 18
Description: Inference chaining three syllogisms. The use of this theorem is marked "discouraged" because it can cause the "minimize" command to have very long run times. However, feel free to use "minimize 4syl /override" if you wish. (Contributed by BJ, 14-Jul-2018.) (New usage is discouraged.)
Hypotheses
Ref Expression
4syl.1  |-  ( ph  ->  ps )
4syl.2  |-  ( ps 
->  ch )
4syl.3  |-  ( ch 
->  th )
4syl.4  |-  ( th 
->  ta )
Assertion
Ref Expression
4syl  |-  ( ph  ->  ta )

Proof of Theorem 4syl
StepHypRef Expression
1 4syl.1 . . 3  |-  ( ph  ->  ps )
2 4syl.2 . . 3  |-  ( ps 
->  ch )
3 4syl.3 . . 3  |-  ( ch 
->  th )
41, 2, 33syl 17 . 2  |-  ( ph  ->  th )
5 4syl.4 . 2  |-  ( th 
->  ta )
64, 5syl 14 1  |-  ( ph  ->  ta )
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:  f1ocnvfvrneq  5783  fcof1o  5790  isoselem  5821  isose  5822  tposss  6247  smoiso  6303  fzssp1  10067  fzosplitsnm1  10209  fzofzp1  10227  fzostep1  10237  bcm1k  10740  climuni  11301  serf0  11360  fsumparts  11478  hashiun  11486  oddprm  12259  hmeores  13818
  Copyright terms: Public domain W3C validator