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

Theorem syl3anbrc 1166
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 1162 . 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 963
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 965
This theorem is referenced by:  smores2  6244  smoiso  6252  iserd  6509  erinxp  6557  resixp  6681  prarloc  7426  eluzuzle  9453  uztrn  9461  nn0pzuz  9504  nn0ge2m1nnALT  9534  ige2m1fz  10019  0elfz  10027  uzsubfz0  10038  elfzmlbm  10040  difelfzle  10043  difelfznle  10044  elfzolt2b  10067  elfzolt3b  10068  elfzouz2  10070  fzossrbm1  10082  elfzo0  10091  eluzgtdifelfzo  10106  elfzodifsumelfzo  10110  fzonn0p1  10120  fzonn0p1p1  10122  elfzom1p1elfzo  10123  fzo0sn0fzo1  10130  ssfzo12bi  10134  ubmelm1fzo  10135  elfzonelfzo  10139  fzosplitprm1  10143  fzostep1  10146  fvinim0ffz  10150  flqword2  10198  modfzo0difsn  10304  modsumfzodifsn  10305  uzennn  10345  seq3split  10388  iseqf1olemkle  10393  iseqf1olemklt  10394  iseqf1olemqk  10403  seq3f1olemqsumkj  10407  seq3f1olemqsumk  10408  seq3f1olemqsum  10409  bcval5  10649  1elfz0hash  10692  seq3coll  10725  seq3shft  10750  resqrexlemoverl  10933  fsum3cvg3  11305  fisumrev2  11355  isumshft  11399  cvgratnnlemseq  11435  cvgratnnlemabsle  11436  cvgratnnlemsumlt  11437  cvgratz  11441  sinbnd2  11663  cosbnd2  11664  cos12dec  11676  nn0o  11811  suprzubdc  11852  zsupssdc  11854  dvdsnprmd  12018  eulerthlema  12121  hashgcdlem  12129  prm23lt5  12154  prm23ge5  12155  nninfdclemcl  12275  nninfdclemp1  12277  nninfdclemlt  12278  unbendc  12281  strleund  12374  sin0pilem1  13198  sin0pilem2  13199  cosq14gt0  13249  cosq23lt0  13250  coseq0q4123  13251  coseq00topi  13252  coseq0negpitopi  13253  tangtx  13255  cosordlem  13266  cosq34lt1  13267  cos02pilt1  13268  cos0pilt1  13269  rplogbval  13359  cvgcmp2nlemabs  13700  iooref1o  13702  taupi  13738
  Copyright terms: Public domain W3C validator