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

Theorem syl3anbrc 1099
Description: Syllogism inference. (Contributed by Mario Carneiro, 11-May-2014.)
Hypotheses
Ref Expression
syl3anbrc.1  |-  ( ph  ->  ps )
syl3anbrc.2  |-  ( ph  ->  ch )
syl3anbrc.3  |-  ( ph  ->  th )
syl3anbrc.4  |-  ( ta  <->  ( ps  /\  ch  /\  th ) )
Assertion
Ref Expression
syl3anbrc  |-  ( ph  ->  ta )

Proof of Theorem syl3anbrc
StepHypRef Expression
1 syl3anbrc.1 . . 3  |-  ( ph  ->  ps )
2 syl3anbrc.2 . . 3  |-  ( ph  ->  ch )
3 syl3anbrc.3 . . 3  |-  ( ph  ->  th )
41, 2, 33jca 1095 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
5 syl3anbrc.4 . 2  |-  ( ta  <->  ( ps  /\  ch  /\  th ) )
64, 5sylibr 141 1  |-  ( ph  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 102    /\ w3a 896
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114  df-3an 898
This theorem is referenced by:  smores2  5940  smoiso  5948  iserd  6163  xpiderm  6208  erinxp  6211  prarloc  6659  eluzuzle  8577  uztrn  8585  nn0pzuz  8626  nn0ge2m1nnALT  8650  ige2m1fz  9074  0elfz  9079  elfz0addOLD  9082  uzsubfz0  9088  elfzmlbm  9090  difelfzle  9094  difelfznle  9095  elfzolt2b  9116  elfzolt3b  9117  elfzouz2  9119  fzossrbm1  9131  elfzo0  9140  eluzgtdifelfzo  9155  elfzodifsumelfzo  9159  fzonn0p1  9169  fzonn0p1p1  9171  elfzom1p1elfzo  9172  fzo0sn0fzo1  9179  ssfzo12bi  9183  ubmelm1fzo  9184  elfzonelfzo  9188  fzosplitprm1  9192  fzostep1  9195  fvinim0ffz  9198  flqword2  9239  modfzo0difsn  9345  modsumfzodifsn  9346  ibcval5  9631  resqrexlemoverl  9848  nn0o  10219
  Copyright terms: Public domain W3C validator