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  1694  sbequ1  1695  sbidm  1776  eqeu  2776  euind  2793  reuind  2809  eldifd  2998  eqssd  3031  ssrabdv  3089  elind  3174  opm  4035  issod  4120  ordsucim  4290  onintonm  4307  ordtri2or2exmidlem  4315  en2lp  4343  ordwe  4364  sosng  4479  sotri2  4796  sotri3  4797  relssdmrn  4917  funun  5023  fnsng  5026  fnprg  5034  fntpg  5035  fntp  5036  fununi  5047  imain  5061  fnco  5087  f00  5165  f1ss  5185  f1ssr  5186  f1ssres  5188  f1f1orn  5227  foimacnv  5234  foun  5235  fun11iun  5237  sefvex  5289  dff3im  5407  fmpt  5412  ffnfv  5419  fmpt2d  5423  ffvresb  5424  fprg  5443  foco2  5494  fcof1  5523  fcofo  5524  fcof1o  5529  fliftf  5539  isoini2  5559  f1oiso  5566  moriotass  5597  fnoprabg  5703  f1ocnvd  5803  suppssfv  5809  suppssov1  5810  1stcof  5891  2ndcof  5892  1stconst  5943  2ndconst  5944  fo2ndf  5949  f1o2ndf1  5950  f1od2  5957  smores2  6013  tfrlem5  6033  tfrlemibfn  6047  tfr1onlembfn  6063  tfri1dALT  6070  tfrcllembfn  6076  nntri2  6209  eroveu  6335  dom2lem  6441  xpf1o  6512  fidifsnen  6538  finexdc  6570  unfidisj  6584  f1finf1o  6605  sbthlemi9  6618  supeuti  6633  infeuti  6668  casef1  6725  nnnninf  6750  en2other2  6766  exmidfodomrlemim  6771  addclpi  6830  mulclpi  6831  nnppipi  6846  recmulnqg  6894  enq0ref  6936  nqnq0pi  6941  genipv  7012  addclpr  7040  nqprxx  7049  prmuloc  7069  mulclpr  7075  distrlem1prl  7085  distrlem1pru  7086  ltexprlempr  7111  ltexprlemrl  7113  ltexprlemru  7115  lteupri  7120  recexprlempr  7135  cauappcvgprlemm  7148  cauappcvgprlemopl  7149  cauappcvgprlemlol  7150  cauappcvgprlemopu  7151  cauappcvgprlemupu  7152  cauappcvgprlemloc  7155  cauappcvgprlemcl  7156  cauappcvgprlemladdfu  7157  cauappcvgprlemladdfl  7158  cauappcvgprlem2  7163  caucvgprlemm  7171  caucvgprlemopl  7172  caucvgprlemlol  7173  caucvgprlemopu  7174  caucvgprlemupu  7175  caucvgprlemloc  7178  caucvgprlemcl  7179  caucvgprlemladdfu  7180  caucvgprlem2  7183  caucvgprprlemml  7197  caucvgprprlemmu  7198  caucvgprprlemopl  7200  caucvgprprlemlol  7201  caucvgprprlemopu  7202  caucvgprprlemupu  7203  caucvgprprlemloc  7206  caucvgprprlemcl  7207  caucvgprprlem2  7213  elrealeu  7311  rereceu  7368  negf1o  7804  receuap  8077  divvalap  8080  cju  8356  nn0ge2m1nn  8666  nnnegz  8686  elnnz  8693  elnn0z  8696  peano2z  8719  nn0n0n1ge2  8750  msqznn  8779  eluzaddi  8977  eluzsubi  8978  uzind4  9008  supinfneg  9015  infsupneg  9016  elnn1uz2  9026  uz2mulcl  9027  divfnzn  9038  nnrp  9075  rpaddcl  9089  rpmulcl  9090  rpdivcl  9091  rpgecl  9094  ge0p1rp  9097  elrpd  9103  ge0addcl  9331  ge0mulcl  9332  icoshftf1o  9340  peano2fzr  9383  uzsubsubfz  9393  fzsplit2  9396  elfznn  9400  fzss1  9408  fzss2  9409  fzp1elp1  9419  elfz1b  9434  elfz0fzfz0  9465  fz0fzelfz0  9466  difelfznle  9474  elfzofz  9501  fzosplitsnm1  9548  ubmelm1fzo  9565  fzofzp1b  9567  fzosplitsn  9572  exbtwnz  9590  flqge0nn0  9628  flqge1nn  9629  zmodcl  9679  modqmuladdnn0  9703  modsumfzodifsn  9731  frec2uzf1od  9741  frec2uzisod  9742  frecuzrdgrrn  9743  frec2uzrdg  9744  frecuzrdgrcl  9745  frecuzrdgtcl  9747  frecuzrdgsuc  9749  frecuzrdgrclt  9750  frecuzrdgfunlem  9754  frecuzrdgtclt  9756  frecuzrdgsuctlem  9758  iseqfveq2  9802  monoord  9809  iseqf1olemqcl  9819  iseqf1olemnab  9821  iseqf1olemab  9822  iseqf1olemqf1o  9826  iseqf1olemqsumkj  9831  iseqf1olemqsumk  9832  iseqid2  9843  serige0  9850  expival  9855  expcl2lemap  9865  expclzaplem  9877  expge0  9889  expge1  9890  zsqcl2  9930  bcval4  10056  bcn1  10062  bccl2  10072  hashennnuni  10083  hashunlem  10108  hashdifpr  10124  zfz1isolem1  10141  iseqcoll  10143  shftfn  10154  shftf  10160  recvguniq  10323  resqrexlemdecn  10340  rersqreu  10356  nn0abscl  10413  nnabscl  10428  abs2dif  10434  climuni  10574  2clim  10582  climcn2  10590  isummolem2a  10660  fisum  10665  zdvdsdc  10692  fzo0dvdseq  10733  oexpneg  10752  oddge22np1  10756  evennn02n  10757  evennn2n  10758  nno  10781  divalglemeunn  10796  divalglemex  10797  divalglemeuneg  10798  divalg  10799  zsupcllemstep  10816  zsupcl  10818  divgcdz  10838  bezoutlemmain  10862  bezoutlemmo  10870  bezoutlemeu  10871  bezoutlemle  10872  sqgcd  10893  eucalgval2  10910  eucalglt  10914  lcmcllem  10924  lcmledvds  10927  lcmneg  10931  lcmgcdlem  10934  ncoprmgcdne1b  10946  prmind2  10977  sqnprm  10992  isprm6  11001  sqrt2irrlem  11015  pw2dvdseu  11021  sqpweven  11028  2sqpwodd  11029  sqrt2irrap  11033  qgt0numnn  11052  phicl2  11065  hashdvds  11072  crth  11075  phimullem  11076  hashgcdlem  11078  oddennn  11080  evenennn  11081  bj-nnord  11291  bj-inf2vnlem1  11303  nnsf  11333  nninfall  11338  nninfself  11343  exmidsbthrlem  11350  qdencn  11353
  Copyright terms: Public domain W3C validator