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
4syl.2
4syl.3
4syl.4
Assertion
Ref Expression
4syl

Proof of Theorem 4syl
StepHypRef Expression
1 4syl.1 . . 3
2 4syl.2 . . 3
3 4syl.3 . . 3
41, 2, 33syl 17 . 2
5 4syl.4 . 2
64, 5syl 14 1
 Colors of variables: wff set class Syntax hints:   wi 4 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7 This theorem is referenced by:  f1ocnvfvrneq  5422  fcof1o  5429  isoselem  5459  isose  5460  tposss  5861  smoiso  5917  fzssp1  8930  fzosplitsnm1  9065  fzofzp1  9083  fzostep1  9093  climuni  9814  serif0  9871
 Copyright terms: Public domain W3C validator