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

Theorem syl3anbrc 1088
 Description: Syllogism inference. (Contributed by Mario Carneiro, 11-May-2014.)
Hypotheses
Ref Expression
syl3anbrc.1
syl3anbrc.2
syl3anbrc.3
syl3anbrc.4
Assertion
Ref Expression
syl3anbrc

Proof of Theorem syl3anbrc
StepHypRef Expression
1 syl3anbrc.1 . . 3
2 syl3anbrc.2 . . 3
3 syl3anbrc.3 . . 3
41, 2, 33jca 1084 . 2
5 syl3anbrc.4 . 2
64, 5sylibr 137 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 98   w3a 885 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101 This theorem depends on definitions:  df-bi 110  df-3an 887 This theorem is referenced by:  smores2  5909  smoiso  5917  iserd  6132  xpiderm  6177  erinxp  6180  prarloc  6601  eluzuzle  8481  uztrn  8489  nn0pzuz  8530  nn0ge2m1nnALT  8553  ige2m1fz  8972  0elfz  8977  elfz0addOLD  8980  uzsubfz0  8986  elfzmlbm  8988  difelfzle  8992  difelfznle  8993  elfzolt2b  9014  elfzolt3b  9015  elfzouz2  9017  fzossrbm1  9029  elfzo0  9038  eluzgtdifelfzo  9053  elfzodifsumelfzo  9057  fzonn0p1  9067  fzonn0p1p1  9069  elfzom1p1elfzo  9070  fzo0sn0fzo1  9077  ssfzo12bi  9081  ubmelm1fzo  9082  elfzonelfzo  9086  fzosplitprm1  9090  fzostep1  9093  fvinim0ffz  9096  flqword2  9131  resqrexlemoverl  9619
 Copyright terms: Public domain W3C validator