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

Theorem sylanbrc 413
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 304 . 2  |-  ( ph  ->  ( ps  /\  ch ) )
4 sylanbrc.3 . 2  |-  ( th  <->  ( ps  /\  ch )
)
53, 4sylibr 133 1  |-  ( ph  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  sb2  1725  sbequ1  1726  sbidm  1807  eqeu  2827  euind  2844  reuind  2862  eldifd  3051  eqssd  3084  ssrabdv  3146  elind  3231  dcun  3443  opm  4126  issod  4211  ordsucim  4386  onintonm  4403  ordtri2or2exmidlem  4411  en2lp  4439  ordwe  4460  sosng  4582  sotri2  4906  sotri3  4907  relssdmrn  5029  funun  5137  fnsng  5140  fnprg  5148  fntpg  5149  fntp  5150  fununi  5161  imain  5175  fnco  5201  f00  5284  f1ss  5304  f1ssr  5305  f1ssres  5307  f1f1orn  5346  foimacnv  5353  foun  5354  fun11iun  5356  sefvex  5410  dff3im  5533  fmpt  5538  ffnfv  5546  fmpt2d  5550  ffvresb  5551  fprg  5571  foco2  5623  fcof1  5652  fcofo  5653  fcof1o  5658  fliftf  5668  isoini2  5688  f1oiso  5695  moriotass  5726  fnoprabg  5840  f1ocnvd  5940  suppssfv  5946  suppssov1  5947  1stcof  6029  2ndcof  6030  1stconst  6086  2ndconst  6087  fo2ndf  6092  f1o2ndf1  6093  f1od2  6100  smores2  6159  tfrlem5  6179  tfrlemibfn  6193  tfr1onlembfn  6209  tfri1dALT  6216  tfrcllembfn  6222  nntri2  6358  eroveu  6488  elixpsn  6597  dom2lem  6634  xpf1o  6706  fidifsnen  6732  finexdc  6764  unfidisj  6778  f1finf1o  6803  fidcenumlemrks  6809  sbthlemi9  6821  supeuti  6849  infeuti  6884  casef1  6943  caseinl  6944  caseinr  6945  difinfsnlem  6952  ctmlemr  6961  ctm  6962  ctssdclemn0  6963  ctssdccl  6964  ctssdc  6966  enumctlemm  6967  nnnninf  6991  en2other2  7020  exmidfodomrlemim  7025  addclpi  7103  mulclpi  7104  nnppipi  7119  recmulnqg  7167  enq0ref  7209  nqnq0pi  7214  genipv  7285  addclpr  7313  nqprxx  7322  prmuloc  7342  mulclpr  7348  distrlem1prl  7358  distrlem1pru  7359  ltexprlempr  7384  ltexprlemrl  7386  ltexprlemru  7388  lteupri  7393  recexprlempr  7408  cauappcvgprlemm  7421  cauappcvgprlemopl  7422  cauappcvgprlemlol  7423  cauappcvgprlemopu  7424  cauappcvgprlemupu  7425  cauappcvgprlemloc  7428  cauappcvgprlemcl  7429  cauappcvgprlemladdfu  7430  cauappcvgprlemladdfl  7431  cauappcvgprlem2  7436  caucvgprlemm  7444  caucvgprlemopl  7445  caucvgprlemlol  7446  caucvgprlemopu  7447  caucvgprlemupu  7448  caucvgprlemloc  7451  caucvgprlemcl  7452  caucvgprlemladdfu  7453  caucvgprlem2  7456  caucvgprprlemml  7470  caucvgprprlemmu  7471  caucvgprprlemopl  7473  caucvgprprlemlol  7474  caucvgprprlemopu  7475  caucvgprprlemupu  7476  caucvgprprlemloc  7479  caucvgprprlemcl  7480  caucvgprprlem2  7486  suplocexprlemex  7498  suplocsrlem  7584  elrealeu  7605  rereceu  7665  axpre-suploclemres  7677  negf1o  8112  receuap  8397  divvalap  8401  cju  8683  nn0ge2m1nn  8995  nnnegz  9015  elnnz  9022  elnn0z  9025  peano2z  9048  nn0n0n1ge2  9079  msqznn  9109  eluzaddi  9308  eluzsubi  9309  uzind4  9339  supinfneg  9346  infsupneg  9347  elnn1uz2  9357  uz2mulcl  9358  divfnzn  9369  nnrp  9406  rpaddcl  9420  rpmulcl  9421  rpdivcl  9422  rpgecl  9425  ge0p1rp  9428  elrpd  9436  ge0addcl  9719  ge0mulcl  9720  ge0xaddcl  9721  icoshftf1o  9729  peano2fzr  9772  uzsubsubfz  9782  fzsplit2  9785  elfznn  9789  fzss1  9798  fzss2  9799  fzp1elp1  9810  elfz1b  9825  elfz0fzfz0  9858  fz0fzelfz0  9859  difelfznle  9867  elfzofz  9894  fzosplitsnm1  9941  ubmelm1fzo  9958  fzofzp1b  9960  fzosplitsn  9965  exbtwnz  9983  flqge0nn0  10021  flqge1nn  10022  zmodcl  10072  modqmuladdnn0  10096  modsumfzodifsn  10124  frec2uzf1od  10134  frec2uzisod  10135  frecuzrdgrrn  10136  frec2uzrdg  10137  frecuzrdgrcl  10138  frecuzrdgtcl  10140  frecuzrdgsuc  10142  frecuzrdgrclt  10143  frecuzrdgfunlem  10147  frecuzrdgtclt  10149  frecuzrdgsuctlem  10151  uzennn  10164  seq3fveq2  10197  monoord  10204  iseqf1olemqcl  10214  iseqf1olemnab  10216  iseqf1olemab  10217  iseqf1olemqf1o  10221  seq3f1olemqsumkj  10226  seq3f1olemqsumk  10227  seq3id2  10237  exp3val  10250  expcl2lemap  10260  expclzaplem  10272  expge0  10284  expge1  10285  zsqcl2  10325  bcval4  10453  bcn1  10459  bccl2  10469  hashennnuni  10480  hashunlem  10505  hashdifpr  10521  zfz1isolem1  10538  seq3coll  10540  shftfn  10551  shftf  10557  recvguniq  10722  resqrexlemdecn  10739  rersqreu  10755  nn0abscl  10812  nnabscl  10827  abs2dif  10833  climuni  11017  2clim  11025  climcn2  11033  summodclem2a  11105  fsum3  11111  fsum3cvg3  11120  fsumcl2lem  11122  fsumadd  11130  fisum0diag2  11171  fsummulc2  11172  fsumge0  11183  geolim2  11236  cvgratnnlemabsle  11251  cvgratz  11256  mertenslemi1  11259  eff2  11300  tanvalap  11329  zdvdsdc  11426  fzo0dvdseq  11467  oexpneg  11486  oddge22np1  11490  evennn02n  11491  evennn2n  11492  nno  11515  divalglemeunn  11530  divalglemex  11531  divalglemeuneg  11532  divalg  11533  zsupcllemstep  11550  zsupcl  11552  divgcdz  11572  bezoutlemmain  11598  bezoutlemmo  11606  bezoutlemeu  11607  bezoutlemle  11608  sqgcd  11629  eucalgval2  11646  eucalglt  11650  lcmcllem  11660  lcmledvds  11663  lcmneg  11667  lcmgcdlem  11670  ncoprmgcdne1b  11682  prmind2  11713  sqnprm  11728  isprm6  11737  sqrt2irrlem  11751  pw2dvdseu  11757  sqpweven  11764  2sqpwodd  11765  sqrt2irrap  11769  qgt0numnn  11788  phicl2  11801  hashdvds  11808  crth  11811  phimullem  11812  hashgcdlem  11814  oddennn  11816  evenennn  11817  ennnfoneleminc  11835  ennnfonelemf1  11842  ennnfonelemen  11845  exmidunben  11850  ctinf  11854  ctiunctlemfo  11863  tgtopon  12146  distopon  12167  epttop  12170  resttopon  12251  resttopon2  12258  cnco  12301  lmss  12326  txtopon  12342  uptx  12354  txdis1cn  12358  hmeocnv  12387  hmeof1o2  12388  hmeores  12395  hmeoco  12396  idhmeo  12397  txhmeo  12399  txswaphmeo  12401  psmetxrge0  12412  isxmet2d  12428  metres2  12461  xmetresbl  12520  comet  12579  bdxmet  12581  bdmet  12582  tgioo  12626  mulc1cncf  12656  mulcncflem  12670  cnrehmeocntop  12673  cnopnap  12674  dedekindeu  12681  dedekindicclemicc  12690  ivthinclemlm  12692  ivthinclemum  12693  ivthinclemlopn  12694  ivthinclemlr  12695  ivthinclemuopn  12696  ivthinclemur  12697  ivthinclemloc  12699  ivthinc  12701  dvfgg  12737  dvcjbr  12752  dvcj  12753  dvfre  12754  bj-nnord  13052  bj-inf2vnlem1  13064  pwf1oexmid  13090  nnsf  13095  nninfall  13100  nninfself  13105  exmidsbthrlem  13113  qdencn  13118
  Copyright terms: Public domain W3C validator