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

Theorem syl3anbrc 1148
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 1144 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
5 syl3anbrc.4 . 2  |-  ( ta  <->  ( ps  /\  ch  /\  th ) )
64, 5sylibr 133 1  |-  ( ph  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104    /\ w3a 945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 947
This theorem is referenced by:  smores2  6157  smoiso  6165  iserd  6421  erinxp  6469  resixp  6593  prarloc  7275  eluzuzle  9283  uztrn  9291  nn0pzuz  9331  nn0ge2m1nnALT  9359  ige2m1fz  9830  0elfz  9838  uzsubfz0  9846  elfzmlbm  9848  difelfzle  9851  difelfznle  9852  elfzolt2b  9875  elfzolt3b  9876  elfzouz2  9878  fzossrbm1  9890  elfzo0  9899  eluzgtdifelfzo  9914  elfzodifsumelfzo  9918  fzonn0p1  9928  fzonn0p1p1  9930  elfzom1p1elfzo  9931  fzo0sn0fzo1  9938  ssfzo12bi  9942  ubmelm1fzo  9943  elfzonelfzo  9947  fzosplitprm1  9951  fzostep1  9954  fvinim0ffz  9958  flqword2  10002  modfzo0difsn  10108  modsumfzodifsn  10109  uzennn  10149  seq3split  10192  iseqf1olemkle  10197  iseqf1olemklt  10198  iseqf1olemqk  10207  seq3f1olemqsumkj  10211  seq3f1olemqsumk  10212  seq3f1olemqsum  10213  bcval5  10449  1elfz0hash  10492  seq3coll  10525  seq3shft  10550  resqrexlemoverl  10733  fsum3cvg3  11105  fisumrev2  11155  isumshft  11199  cvgratnnlemseq  11235  cvgratnnlemabsle  11236  cvgratnnlemsumlt  11237  cvgratz  11241  sinbnd2  11360  cosbnd2  11361  nn0o  11500  dvdsnprmd  11702  hashgcdlem  11798  strleund  11942  cvgcmp2nlemabs  13029
  Copyright terms: Public domain W3C validator