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

Theorem sylanbrc 408
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 300 . 2  |-  ( ph  ->  ( ps  /\  ch ) )
4 sylanbrc.3 . 2  |-  ( th  <->  ( ps  /\  ch )
)
53, 4sylibr 132 1  |-  ( ph  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    <-> wb 103
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
This theorem is referenced by:  sb2  1692  sbequ1  1693  sbidm  1774  eqeu  2771  euind  2788  reuind  2804  eldifd  2992  eqssd  3025  ssrabdv  3082  elind  3167  opm  4017  issod  4102  ordsucim  4272  onintonm  4289  ordtri2or2exmidlem  4297  en2lp  4325  ordwe  4346  sosng  4459  sotri2  4772  sotri3  4773  relssdmrn  4891  funun  4994  fnsng  4997  fnprg  5005  fntpg  5006  fntp  5007  fununi  5018  imain  5032  fnco  5058  f00  5132  f1ss  5148  f1ssr  5149  f1ssres  5150  f1f1orn  5189  foimacnv  5196  foun  5197  fun11iun  5199  sefvex  5248  dff3im  5365  foco2  5371  fmpt  5372  ffnfv  5376  fmpt2d  5380  ffvresb  5381  fprg  5399  fcof1  5475  fcofo  5476  fcof1o  5481  fliftf  5491  isoini2  5510  f1oiso  5517  moriotass  5548  fnoprabg  5654  f1ocnvd  5754  suppssfv  5760  suppssov1  5761  1stcof  5842  2ndcof  5843  1stconst  5894  2ndconst  5895  fo2ndf  5900  f1o2ndf1  5901  f1od2  5908  smores2  5964  tfrlem5  5984  tfrlemibfn  5998  tfr1onlembfn  6014  tfri1dALT  6021  tfrcllembfn  6027  nntri2  6159  eroveu  6285  dom2lem  6341  xpf1o  6407  fidifsnen  6427  unfidisj  6467  f1finf1o  6487  supeuti  6502  infeuti  6537  en2other2  6592  addclpi  6649  mulclpi  6650  nnppipi  6665  recmulnqg  6713  enq0ref  6755  nqnq0pi  6760  genipv  6831  addclpr  6859  nqprxx  6868  prmuloc  6888  mulclpr  6894  distrlem1prl  6904  distrlem1pru  6905  ltexprlempr  6930  ltexprlemrl  6932  ltexprlemru  6934  lteupri  6939  recexprlempr  6954  cauappcvgprlemm  6967  cauappcvgprlemopl  6968  cauappcvgprlemlol  6969  cauappcvgprlemopu  6970  cauappcvgprlemupu  6971  cauappcvgprlemloc  6974  cauappcvgprlemcl  6975  cauappcvgprlemladdfu  6976  cauappcvgprlemladdfl  6977  cauappcvgprlem2  6982  caucvgprlemm  6990  caucvgprlemopl  6991  caucvgprlemlol  6992  caucvgprlemopu  6993  caucvgprlemupu  6994  caucvgprlemloc  6997  caucvgprlemcl  6998  caucvgprlemladdfu  6999  caucvgprlem2  7002  caucvgprprlemml  7016  caucvgprprlemmu  7017  caucvgprprlemopl  7019  caucvgprprlemlol  7020  caucvgprprlemopu  7021  caucvgprprlemupu  7022  caucvgprprlemloc  7025  caucvgprprlemcl  7026  caucvgprprlem2  7032  elrealeu  7130  rereceu  7187  negf1o  7623  receuap  7896  divvalap  7899  cju  8175  nn0ge2m1nn  8485  nnnegz  8505  elnnz  8512  elnn0z  8515  peano2z  8538  nn0n0n1ge2  8569  msqznn  8598  eluzaddi  8796  eluzsubi  8797  uzind4  8827  supinfneg  8834  infsupneg  8835  elnn1uz2  8845  uz2mulcl  8846  divfnzn  8857  nnrp  8894  rpaddcl  8908  rpmulcl  8909  rpdivcl  8910  rpgecl  8913  ge0p1rp  8916  elrpd  8922  ge0addcl  9150  ge0mulcl  9151  icoshftf1o  9159  peano2fzr  9202  uzsubsubfz  9212  fzsplit2  9215  elfznn  9219  fzss1  9227  fzss2  9228  fzp1elp1  9238  elfz1b  9253  elfz0fzfz0  9284  fz0fzelfz0  9285  difelfznle  9293  elfzofz  9318  fzosplitsnm1  9365  ubmelm1fzo  9382  fzofzp1b  9384  fzosplitsn  9389  exbtwnz  9407  flqge0nn0  9445  flqge1nn  9446  zmodcl  9496  modqmuladdnn0  9520  modsumfzodifsn  9548  frec2uzf1od  9558  frec2uzisod  9559  frecuzrdgrrn  9560  frec2uzrdg  9561  frecuzrdgrcl  9562  frecuzrdgtcl  9564  frecuzrdgsuc  9566  frecuzrdgrclt  9567  frecuzrdgfunlem  9571  frecuzrdgtclt  9573  frecuzrdgsuctlem  9575  iseqfveq2  9614  monoord  9621  iseqid2  9634  serige0  9640  expival  9645  expcl2lemap  9655  expclzaplem  9667  expge0  9679  expge1  9680  zsqcl2  9720  bcval4  9846  bcn1  9852  bccl2  9862  hashennnuni  9873  hashunlem  9898  hashdifpr  9914  shftfn  9931  shftf  9937  recvguniq  10100  resqrexlemdecn  10117  rersqreu  10133  nn0abscl  10190  nnabscl  10205  abs2dif  10211  climuni  10351  2clim  10359  climcn2  10367  zdvdsdc  10442  fzo0dvdseq  10483  oexpneg  10502  oddge22np1  10506  evennn02n  10507  evennn2n  10508  nno  10531  divalglemeunn  10546  divalglemex  10547  divalglemeuneg  10548  divalg  10549  zsupcllemstep  10566  zsupcl  10568  divgcdz  10588  bezoutlemmain  10612  bezoutlemmo  10620  bezoutlemeu  10621  bezoutlemle  10622  sqgcd  10643  eucalgval2  10660  eucalglt  10664  lcmcllem  10674  lcmledvds  10677  lcmneg  10681  lcmgcdlem  10684  ncoprmgcdne1b  10696  prmind2  10727  sqnprm  10742  isprm6  10751  sqrt2irrlem  10765  pw2dvdseu  10771  sqpweven  10778  2sqpwodd  10779  sqrt2irrap  10783  qgt0numnn  10802  phicl2  10815  hashdvds  10822  crth  10825  phimullem  10826  hashgcdlem  10828  oddennn  10830  evenennn  10831  znnen  10836  bj-nnord  11038  bj-inf2vnlem1  11050  qdencn  11070
  Copyright terms: Public domain W3C validator