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

Theorem syl3anbrc 1150
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 1146 . 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 947
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 949
This theorem is referenced by:  smores2  6159  smoiso  6167  iserd  6423  erinxp  6471  resixp  6595  prarloc  7279  eluzuzle  9302  uztrn  9310  nn0pzuz  9350  nn0ge2m1nnALT  9378  ige2m1fz  9858  0elfz  9866  uzsubfz0  9874  elfzmlbm  9876  difelfzle  9879  difelfznle  9880  elfzolt2b  9903  elfzolt3b  9904  elfzouz2  9906  fzossrbm1  9918  elfzo0  9927  eluzgtdifelfzo  9942  elfzodifsumelfzo  9946  fzonn0p1  9956  fzonn0p1p1  9958  elfzom1p1elfzo  9959  fzo0sn0fzo1  9966  ssfzo12bi  9970  ubmelm1fzo  9971  elfzonelfzo  9975  fzosplitprm1  9979  fzostep1  9982  fvinim0ffz  9986  flqword2  10030  modfzo0difsn  10136  modsumfzodifsn  10137  uzennn  10177  seq3split  10220  iseqf1olemkle  10225  iseqf1olemklt  10226  iseqf1olemqk  10235  seq3f1olemqsumkj  10239  seq3f1olemqsumk  10240  seq3f1olemqsum  10241  bcval5  10477  1elfz0hash  10520  seq3coll  10553  seq3shft  10578  resqrexlemoverl  10761  fsum3cvg3  11133  fisumrev2  11183  isumshft  11227  cvgratnnlemseq  11263  cvgratnnlemabsle  11264  cvgratnnlemsumlt  11265  cvgratz  11269  sinbnd2  11388  cosbnd2  11389  cos12dec  11401  nn0o  11531  dvdsnprmd  11733  hashgcdlem  11830  strleund  11974  sin0pilem1  12789  sin0pilem2  12790  cosq14gt0  12840  cosq23lt0  12841  coseq0q4123  12842  coseq00topi  12843  coseq0negpitopi  12844  tangtx  12846  cosordlem  12857  cosq34lt1  12858  cos02pilt1  12859  cvgcmp2nlemabs  13154  taupi  13166
  Copyright terms: Public domain W3C validator