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

Theorem syl3anbrc 1127
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 1123 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
5 syl3anbrc.4 . 2  |-  ( ta  <->  ( ps  /\  ch  /\  th ) )
64, 5sylibr 132 1  |-  ( ph  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103    /\ w3a 924
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115  df-3an 926
This theorem is referenced by:  smores2  6059  smoiso  6067  iserd  6318  xpiderm  6363  erinxp  6366  prarloc  7062  eluzuzle  9027  uztrn  9035  nn0pzuz  9075  nn0ge2m1nnALT  9103  ige2m1fz  9524  0elfz  9532  uzsubfz0  9540  elfzmlbm  9542  difelfzle  9545  difelfznle  9546  elfzolt2b  9569  elfzolt3b  9570  elfzouz2  9572  fzossrbm1  9584  elfzo0  9593  eluzgtdifelfzo  9608  elfzodifsumelfzo  9612  fzonn0p1  9622  fzonn0p1p1  9624  elfzom1p1elfzo  9625  fzo0sn0fzo1  9632  ssfzo12bi  9636  ubmelm1fzo  9637  elfzonelfzo  9641  fzosplitprm1  9645  fzostep1  9648  fvinim0ffz  9652  flqword2  9696  modfzo0difsn  9802  modsumfzodifsn  9803  seq3split  9907  iseqf1olemkle  9913  iseqf1olemklt  9914  iseqf1olemqk  9923  seq3f1olemqsumkj  9927  seq3f1olemqsumk  9928  seq3f1olemqsum  9929  ibcval5  10171  1elfz0hash  10214  iseqcoll  10247  seq3shft  10272  resqrexlemoverl  10454  fsum3cvg3  10789  fisumrev2  10840  isumshft  10884  cvgratnnlemseq  10920  cvgratnnlemabsle  10921  cvgratnnlemsumlt  10922  cvgratz  10926  sinbnd2  11045  cosbnd2  11046  nn0o  11185  dvdsnprmd  11385  hashgcdlem  11481  strleund  11581
  Copyright terms: Public domain W3C validator