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  1740  sbequ1  1741  sbidm  1823  eqeu  2854  euind  2871  reuind  2889  eldifd  3081  eqssd  3114  ssrabdv  3176  elind  3261  dcun  3473  opm  4156  issod  4241  ordsucim  4416  onintonm  4433  ordtri2or2exmidlem  4441  en2lp  4469  ordwe  4490  sosng  4612  sotri2  4936  sotri3  4937  relssdmrn  5059  funun  5167  fnsng  5170  fnprg  5178  fntpg  5179  fntp  5180  fununi  5191  imain  5205  fnco  5231  f00  5314  f1ss  5334  f1ssr  5335  f1ssres  5337  f1f1orn  5378  foimacnv  5385  foun  5386  fun11iun  5388  sefvex  5442  dff3im  5565  fmpt  5570  ffnfv  5578  fmpt2d  5582  ffvresb  5583  fprg  5603  foco2  5655  fcof1  5684  fcofo  5685  fcof1o  5690  fliftf  5700  isoini2  5720  f1oiso  5727  moriotass  5758  fnoprabg  5872  f1ocnvd  5972  suppssfv  5978  suppssov1  5979  1stcof  6061  2ndcof  6062  1stconst  6118  2ndconst  6119  fo2ndf  6124  f1o2ndf1  6125  f1od2  6132  smores2  6191  tfrlem5  6211  tfrlemibfn  6225  tfr1onlembfn  6241  tfri1dALT  6248  tfrcllembfn  6254  nntri2  6390  eroveu  6520  elixpsn  6629  dom2lem  6666  xpf1o  6738  fidifsnen  6764  finexdc  6796  unfidisj  6810  f1finf1o  6835  fidcenumlemrks  6841  sbthlemi9  6853  supeuti  6881  infeuti  6916  casef1  6975  caseinl  6976  caseinr  6977  difinfsnlem  6984  ctmlemr  6993  ctm  6994  ctssdclemn0  6995  ctssdccl  6996  ctssdc  6998  enumctlemm  6999  nnnninf  7023  en2other2  7052  exmidfodomrlemim  7057  cc2lem  7081  cc4f  7084  addclpi  7142  mulclpi  7143  nnppipi  7158  recmulnqg  7206  enq0ref  7248  nqnq0pi  7253  genipv  7324  addclpr  7352  nqprxx  7361  prmuloc  7381  mulclpr  7387  distrlem1prl  7397  distrlem1pru  7398  ltexprlempr  7423  ltexprlemrl  7425  ltexprlemru  7427  lteupri  7432  recexprlempr  7447  cauappcvgprlemm  7460  cauappcvgprlemopl  7461  cauappcvgprlemlol  7462  cauappcvgprlemopu  7463  cauappcvgprlemupu  7464  cauappcvgprlemloc  7467  cauappcvgprlemcl  7468  cauappcvgprlemladdfu  7469  cauappcvgprlemladdfl  7470  cauappcvgprlem2  7475  caucvgprlemm  7483  caucvgprlemopl  7484  caucvgprlemlol  7485  caucvgprlemopu  7486  caucvgprlemupu  7487  caucvgprlemloc  7490  caucvgprlemcl  7491  caucvgprlemladdfu  7492  caucvgprlem2  7495  caucvgprprlemml  7509  caucvgprprlemmu  7510  caucvgprprlemopl  7512  caucvgprprlemlol  7513  caucvgprprlemopu  7514  caucvgprprlemupu  7515  caucvgprprlemloc  7518  caucvgprprlemcl  7519  caucvgprprlem2  7525  suplocexprlemex  7537  suplocsrlem  7623  elrealeu  7644  rereceu  7704  axpre-suploclemres  7716  negf1o  8151  receuap  8437  divvalap  8441  cju  8726  nn0ge2m1nn  9044  nnnegz  9064  elnnz  9071  elnn0z  9074  peano2z  9097  nn0n0n1ge2  9128  msqznn  9158  eluzaddi  9359  eluzsubi  9360  uzind4  9390  supinfneg  9397  infsupneg  9398  elnn1uz2  9408  uz2mulcl  9409  divfnzn  9420  nnrp  9458  rpaddcl  9472  rpmulcl  9473  rpdivcl  9474  rpgecl  9477  ge0p1rp  9480  elrpd  9488  ge0addcl  9771  ge0mulcl  9772  ge0xaddcl  9773  icoshftf1o  9781  peano2fzr  9824  uzsubsubfz  9834  fzsplit2  9837  elfznn  9841  fzss1  9850  fzss2  9851  fzp1elp1  9862  elfz1b  9877  elfz0fzfz0  9910  fz0fzelfz0  9911  difelfznle  9919  elfzofz  9946  fzosplitsnm1  9993  ubmelm1fzo  10010  fzofzp1b  10012  fzosplitsn  10017  exbtwnz  10035  flqge0nn0  10073  flqge1nn  10074  zmodcl  10124  modqmuladdnn0  10148  modsumfzodifsn  10176  frec2uzf1od  10186  frec2uzisod  10187  frecuzrdgrrn  10188  frec2uzrdg  10189  frecuzrdgrcl  10190  frecuzrdgtcl  10192  frecuzrdgsuc  10194  frecuzrdgrclt  10195  frecuzrdgfunlem  10199  frecuzrdgtclt  10201  frecuzrdgsuctlem  10203  uzennn  10216  seq3fveq2  10249  monoord  10256  iseqf1olemqcl  10266  iseqf1olemnab  10268  iseqf1olemab  10269  iseqf1olemqf1o  10273  seq3f1olemqsumkj  10278  seq3f1olemqsumk  10279  seq3id2  10289  exp3val  10302  expcl2lemap  10312  expclzaplem  10324  expge0  10336  expge1  10337  zsqcl2  10377  bcval4  10505  bcn1  10511  bccl2  10521  hashennnuni  10532  hashunlem  10557  hashdifpr  10573  zfz1isolem1  10590  seq3coll  10592  shftfn  10603  shftf  10609  recvguniq  10774  resqrexlemdecn  10791  rersqreu  10807  nn0abscl  10864  nnabscl  10879  abs2dif  10885  climuni  11069  2clim  11077  climcn2  11085  summodclem2a  11157  fsum3  11163  fsum3cvg3  11172  fsumcl2lem  11174  fsumadd  11182  fisum0diag2  11223  fsummulc2  11224  fsumge0  11235  geolim2  11288  cvgratnnlemabsle  11303  cvgratz  11308  mertenslemi1  11311  prodmodclem3  11351  prodmodclem2a  11352  eff2  11393  tanvalap  11422  zdvdsdc  11521  fzo0dvdseq  11562  oexpneg  11581  oddge22np1  11585  evennn02n  11586  evennn2n  11587  nno  11610  divalglemeunn  11625  divalglemex  11626  divalglemeuneg  11627  divalg  11628  zsupcllemstep  11645  zsupcl  11647  divgcdz  11667  bezoutlemmain  11693  bezoutlemmo  11701  bezoutlemeu  11702  bezoutlemle  11703  sqgcd  11724  eucalgval2  11741  eucalglt  11745  lcmcllem  11755  lcmledvds  11758  lcmneg  11762  lcmgcdlem  11765  ncoprmgcdne1b  11777  prmind2  11808  sqnprm  11823  isprm6  11832  sqrt2irrlem  11846  pw2dvdseu  11853  sqpweven  11860  2sqpwodd  11861  sqrt2irrap  11865  qgt0numnn  11884  phicl2  11897  hashdvds  11904  crth  11907  phimullem  11908  hashgcdlem  11910  oddennn  11912  evenennn  11913  ennnfoneleminc  11931  ennnfonelemf1  11938  ennnfonelemen  11941  exmidunben  11946  ctinf  11950  ctiunctlemfo  11959  tgtopon  12245  distopon  12266  epttop  12269  resttopon  12350  resttopon2  12357  cnco  12400  lmss  12425  txtopon  12441  uptx  12453  txdis1cn  12457  hmeocnv  12486  hmeof1o2  12487  hmeores  12494  hmeoco  12495  idhmeo  12496  txhmeo  12498  txswaphmeo  12500  psmetxrge0  12511  isxmet2d  12527  metres2  12560  xmetresbl  12619  comet  12678  bdxmet  12680  bdmet  12681  tgioo  12725  mulc1cncf  12755  mulcncflem  12769  cnrehmeocntop  12772  cnopnap  12773  dedekindeu  12780  dedekindicclemicc  12789  ivthinclemlm  12791  ivthinclemum  12792  ivthinclemlopn  12793  ivthinclemlr  12794  ivthinclemuopn  12795  ivthinclemur  12796  ivthinclemloc  12798  ivthinc  12800  dvfgg  12836  dvcjbr  12851  dvcj  12852  dvfre  12853  bj-nnord  13186  bj-inf2vnlem1  13198  pwf1oexmid  13224  nnsf  13229  nninfall  13234  nninfself  13239  exmidsbthrlem  13247  qdencn  13252
  Copyright terms: Public domain W3C validator