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

Theorem syl3anbrc 1128
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 1124 . 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 925
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 927
This theorem is referenced by:  smores2  6073  smoiso  6081  iserd  6332  xpiderm  6377  erinxp  6380  resixp  6504  prarloc  7116  eluzuzle  9081  uztrn  9089  nn0pzuz  9129  nn0ge2m1nnALT  9157  ige2m1fz  9578  0elfz  9586  uzsubfz0  9594  elfzmlbm  9596  difelfzle  9599  difelfznle  9600  elfzolt2b  9623  elfzolt3b  9624  elfzouz2  9626  fzossrbm1  9638  elfzo0  9647  eluzgtdifelfzo  9662  elfzodifsumelfzo  9666  fzonn0p1  9676  fzonn0p1p1  9678  elfzom1p1elfzo  9679  fzo0sn0fzo1  9686  ssfzo12bi  9690  ubmelm1fzo  9691  elfzonelfzo  9695  fzosplitprm1  9699  fzostep1  9702  fvinim0ffz  9706  flqword2  9750  modfzo0difsn  9856  modsumfzodifsn  9857  seq3split  9961  iseqf1olemkle  9967  iseqf1olemklt  9968  iseqf1olemqk  9977  seq3f1olemqsumkj  9981  seq3f1olemqsumk  9982  seq3f1olemqsum  9983  ibcval5  10225  1elfz0hash  10268  iseqcoll  10301  seq3shft  10326  resqrexlemoverl  10508  fsum3cvg3  10843  fisumrev2  10894  isumshft  10938  cvgratnnlemseq  10974  cvgratnnlemabsle  10975  cvgratnnlemsumlt  10976  cvgratz  10980  sinbnd2  11099  cosbnd2  11100  nn0o  11239  dvdsnprmd  11439  hashgcdlem  11535  strleund  11636
  Copyright terms: Public domain W3C validator