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

Theorem sylanbrc 402
Description: Syllogism inference. (Contributed by Jeff Madsen, 2-Sep-2009.)
Hypotheses
Ref Expression
sylanbrc.1  |-  ( ph  ->  ps )
sylanbrc.2  |-  ( ph  ->  ch )
sylanbrc.3  |-  ( th  <->  ( ps  /\  ch )
)
Assertion
Ref Expression
sylanbrc  |-  ( ph  ->  th )

Proof of Theorem sylanbrc
StepHypRef Expression
1 sylanbrc.1 . . 3  |-  ( ph  ->  ps )
2 sylanbrc.2 . . 3  |-  ( ph  ->  ch )
31, 2jca 294 . 2  |-  ( ph  ->  ( ps  /\  ch ) )
4 sylanbrc.3 . 2  |-  ( th  <->  ( ps  /\  ch )
)
53, 4sylibr 141 1  |-  ( ph  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101    <-> wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  sb2  1666  sbequ1  1667  sbidm  1747  eqeu  2733  euind  2750  reuind  2766  eldifd  2955  eqssd  2989  ssrabdv  3046  psstr  3076  sspsstr  3077  psssstr  3078  opm  3998  issod  4083  ordsucim  4253  onintonm  4270  ordtri2or2exmidlem  4278  en2lp  4305  ordwe  4327  sosng  4440  sotri2  4749  sotri3  4750  relssdmrn  4868  funun  4971  fnsng  4974  fnprg  4981  fntpg  4982  fntp  4983  fununi  4994  imain  5008  fnco  5034  f00  5108  f1ss  5124  f1ssr  5125  f1ssres  5126  f1f1orn  5164  foimacnv  5171  foun  5172  fun11iun  5174  sefvex  5223  dff3im  5339  foco2  5345  fmpt  5346  ffnfv  5350  fmpt2d  5354  ffvresb  5355  fprg  5373  fcof1  5450  fcofo  5451  fcof1o  5456  fliftf  5466  isoini2  5485  f1oiso  5492  moriotass  5523  fnoprabg  5629  f1ocnvd  5729  suppssfv  5735  suppssov1  5736  1stcof  5817  2ndcof  5818  1stconst  5869  2ndconst  5870  fo2ndf  5875  f1o2ndf1  5876  f1od2  5883  smores2  5939  tfrlem5  5960  tfrlemibfn  5972  nntri2  6103  eroveu  6227  dom2lem  6282  fidifsnen  6361  supeuti  6399  addclpi  6482  mulclpi  6483  nnppipi  6498  recmulnqg  6546  enq0ref  6588  nqnq0pi  6593  genipv  6664  addclpr  6692  nqprxx  6701  prmuloc  6721  mulclpr  6727  distrlem1prl  6737  distrlem1pru  6738  ltexprlempr  6763  ltexprlemrl  6765  ltexprlemru  6767  lteupri  6772  recexprlempr  6787  cauappcvgprlemm  6800  cauappcvgprlemopl  6801  cauappcvgprlemlol  6802  cauappcvgprlemopu  6803  cauappcvgprlemupu  6804  cauappcvgprlemloc  6807  cauappcvgprlemcl  6808  cauappcvgprlemladdfu  6809  cauappcvgprlemladdfl  6810  cauappcvgprlem2  6815  caucvgprlemm  6823  caucvgprlemopl  6824  caucvgprlemlol  6825  caucvgprlemopu  6826  caucvgprlemupu  6827  caucvgprlemloc  6830  caucvgprlemcl  6831  caucvgprlemladdfu  6832  caucvgprlem2  6835  caucvgprprlemml  6849  caucvgprprlemmu  6850  caucvgprprlemopl  6852  caucvgprprlemlol  6853  caucvgprprlemopu  6854  caucvgprprlemupu  6855  caucvgprprlemloc  6858  caucvgprprlemcl  6859  caucvgprprlem2  6865  elrealeu  6963  rereceu  7020  receuap  7723  divvalap  7726  cju  7988  nn0ge2m1nn  8298  nnnegz  8304  elnnz  8311  elnn0z  8314  peano2z  8337  nn0n0n1ge2  8368  msqznn  8396  eluzaddi  8594  eluzsubi  8595  uzind4  8626  elnn1uz2  8640  uz2mulcl  8641  divfnzn  8652  nnrp  8689  rpaddcl  8703  rpmulcl  8704  rpdivcl  8705  rpgecl  8708  ge0p1rp  8711  elrpd  8717  ge0addcl  8950  ge0mulcl  8951  icoshftf1o  8959  peano2fzr  9002  uzsubsubfz  9012  fzsplit2  9015  elfznn  9019  fzss1  9027  fzss2  9028  fzp1elp1  9038  elfz1b  9053  elfz0fzfz0  9084  fz0fzelfz0  9085  difelfznle  9094  elfzofz  9119  fzosplitsnm1  9166  ubmelm1fzo  9183  fzofzp1b  9185  fzosplitsn  9190  qbtwnz  9207  flqge0nn0  9237  flqge1nn  9238  zmodcl  9288  modqmuladdnn0  9312  modsumfzodifsn  9340  frec2uzf1od  9350  frec2uzisod  9351  frecuzrdgrrn  9352  frec2uzrdg  9353  frecuzrdgrom  9354  frecuzrdgfn  9356  frecuzrdgsuc  9359  iseqf  9382  iseqfveq2  9386  monoord  9393  serige0  9411  expival  9416  expcl2lemap  9426  expclzaplem  9438  expge0  9450  expge1  9451  zsqcl2  9491  bcval4  9613  bcn1  9619  bccl2  9629  shftfn  9646  shftf  9652  recvguniq  9814  resqrexlemdecn  9831  rersqreu  9847  nn0abscl  9904  nnabscl  9919  abs2dif  9925  climuni  10037  2clim  10045  climcn2  10053  fzo0dvdseq  10161  oexpneg  10180  oddge22np1  10185  evennn02n  10186  evennn2n  10187  nno  10210  sqr2irrlem  10222  pw2dvdseu  10228  bj-nnord  10442  bj-inf2vnlem1  10454  qdencn  10483
  Copyright terms: Public domain W3C validator