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

Theorem 3syl 17
Description: Inference chaining two syllogisms. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
3syl.1  |-  ( ph  ->  ps )
3syl.2  |-  ( ps 
->  ch )
3syl.3  |-  ( ch 
->  th )
Assertion
Ref Expression
3syl  |-  ( ph  ->  th )

Proof of Theorem 3syl
StepHypRef Expression
1 3syl.1 . . 3  |-  ( ph  ->  ps )
2 3syl.2 . . 3  |-  ( ps 
->  ch )
31, 2syl 14 . 2  |-  ( ph  ->  ch )
4 3syl.3 . 2  |-  ( ch 
->  th )
53, 4syl 14 1  |-  ( ph  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  4syl  18  simpl2im  383  hbim  1524  19.9hd  1640  equsexd  1707  sbcof2  1782  aev  1784  sbequi  1811  nfsbd  1950  mo2n  2027  eupickb  2080  r19.29af2  2572  spc2gv  2776  spc3gv  2778  eqvincg  2809  sbcco3g  3057  ssrmof  3160  exmidsssnc  4126  snelpwi  4134  opth1  4158  frind  4274  onin  4308  abnexg  4367  reusv1  4379  xpexg  4653  dmexg  4803  rnexg  4804  relfld  5067  funimaexglem  5206  funimaexg  5207  fabexg  5310  fsnd  5410  nfvres  5454  funimass4  5472  elfvmptrab1  5515  funconstss  5538  f1oresrab  5585  resfunexg  5641  f1eqcocnv  5692  isores1  5715  isoini  5719  isose  5722  isopolem  5723  isosolem  5725  eusvobj2  5760  acexmidlemcase  5769  oprabid  5803  offval  5989  resfunexgALT  6008  offval3  6032  1stvalg  6040  2ndvalg  6041  1stcof  6061  2ndcof  6062  cnvf1o  6122  tposf12  6166  smores3  6190  smoiso  6199  tfr0dm  6219  tfrlemibxssdm  6224  tfrlemi14d  6230  tfrexlem  6231  tfr1onlemssrecs  6236  tfr1onlemsucfn  6237  tfr1onlemsucaccv  6238  tfr1onlembxssdm  6240  tfr1onlemres  6246  tfri1dALT  6248  tfrcllemssrecs  6249  tfrcllemsucfn  6250  tfrcllemsucaccv  6251  tfrcllembxssdm  6253  tfrcllemres  6259  rdgss  6280  nnsucsssuc  6388  nntr2  6399  swoord1  6458  swoord2  6459  iinerm  6501  eroveu  6520  pmresg  6570  en1uniel  6698  fopwdom  6730  xpen  6739  ssenen  6745  isinfinf  6791  ac6sfi  6792  preimaf1ofi  6839  sbthlem1  6845  fi0  6863  fiss  6865  supubti  6886  suplubti  6887  isotilem  6893  supisolem  6895  supisoex  6896  supisoti  6897  ordiso2  6920  eldju1st  6956  eldju2ndl  6957  updjud  6967  djudom  6978  ctmlemr  6993  enumctlemm  6999  ctssexmid  7024  exmidonfinlem  7049  en2other2  7052  exmidaclem  7064  cc2lem  7081  cc3  7083  addclnq  7190  mulclnq  7191  1qec  7203  prarloclemarch2  7234  enq0tr  7249  addclnq0  7266  mulclnq0  7267  nq0m0r  7271  prarloclemlo  7309  prarloc  7318  genpml  7332  genpmu  7333  addnqprl  7344  addnqpru  7345  recnnpr  7363  prmuloc2  7382  1idpru  7406  ltexprlemm  7415  ltexprlemloc  7422  recexprlemm  7439  recexprlem1ssl  7448  caucvgprlemnkj  7481  caucvgprlemnbj  7482  caucvgprlemm  7483  caucvgprlemopl  7484  caucvgprlemlol  7485  caucvgprlemladdfu  7492  caucvgprlemladdrl  7493  caucvgprprlemk  7498  caucvgprprlemloccalc  7499  caucvgprprlemnkltj  7504  caucvgprprlemnjltk  7506  caucvgprprlemml  7509  caucvgprprlemmu  7510  caucvgprprlemlol  7513  caucvgprprlemexb  7522  caucvgprprlem1  7524  suplocexprlemml  7531  suplocexprlemlub  7539  addclsr  7568  mulclsr  7569  prsrcl  7599  caucvgsrlemoffcau  7613  peano5nnnn  7707  mulap0r  8384  nn1suc  8746  prime  9157  zindd  9176  xrlttri3  9590  xnn0xadd0  9657  fzopth  9848  fzsuc  9856  fzpred  9857  fzp1ss  9860  fztp  9865  fseq1p1m1  9881  1fv  9923  elfzom1elp1fzo  9986  ssfzo12  10008  fzosplitsn  10017  divfl0  10076  modqid  10129  modqmuladdim  10147  frecuzrdgtcl  10192  frecuzrdgfunlem  10199  frecfzennn  10206  frecfzen2  10207  seq3val  10238  seqvalcd  10239  iseqf1olemqcl  10266  iseqf1olemnab  10268  iseqf1olemmo  10272  iseqf1olemqk  10274  seq3f1olemstep  10281  seq3id3  10287  faclbnd  10494  faclbnd3  10496  bcm1k  10513  hashfz1  10536  focdmex  10540  hashfz  10574  hashfzp1  10577  hashfacen  10586  leisorel  10587  cjcj  10662  caucvgre  10760  r19.2uz  10772  resqrexlemgt0  10799  ltabs  10866  xrmaxiflemab  11023  xrmaxiflemlub  11024  nnf1o  11152  summodclem2a  11157  fsumf1o  11166  fisum0diag2  11223  modfsummodlemstep  11233  fsumparts  11246  clim2prod  11315  prodfap0  11321  prodmodclem2a  11352  ef0lem  11373  resinval  11429  recosval  11430  demoivreALT  11487  nn0o  11611  zsupcllemstep  11645  zsupcllemex  11646  infssuzledc  11650  gcdmultiplez  11716  dvdssq  11726  eucalg  11747  lcmgcdnn  11770  dvdsnprmd  11813  prm2orodd  11814  qnumdenbi  11877  nn0gcdsq  11885  phibnd  11900  hashdvds  11904  phimullem  11908  hashgcdlem  11910  unennn  11917  ennnfonelemk  11920  ennnfonelemjn  11922  ennnfonelemhf1o  11933  ennnfonelemex  11934  ennnfonelemf1  11938  ennnfonelemrn  11939  qnnen  11951  setsfun0  12005  srngbased  12092  srngplusgd  12093  srngmulrd  12094  srnginvld  12095  lmodbased  12103  lmodplusgd  12104  lmodscad  12105  lmodvscad  12106  ipsbased  12111  ipsaddgd  12112  ipsmulrd  12113  ipsscad  12114  ipsvscad  12115  ipsipd  12116  tgval  12228  cldval  12278  ntrfval  12279  clsfval  12280  neifval  12319  neif  12320  neival  12322  cnclima  12402  cncnpi  12407  cnrest2  12415  cnrest2r  12416  cnptoprest  12418  cnpdis  12421  txvalex  12433  txval  12434  txcnmpt  12452  txdis  12456  cnmpt1t  12464  cnmpt2t  12472  hmeocnv  12486  hmeontr  12492  txhmeo  12498  xmetunirn  12537  xmettpos  12549  metn0  12557  xmetres  12561  metres  12562  blrnps  12590  blrn  12591  blin2  12611  blbas  12612  xmeterval  12614  xmettxlem  12688  xmettx  12689  metcnpi  12694  reldvg  12827  dvaddxx  12846  dvmulxx  12847  dviaddf  12848  dvimulf  12849  dvfre  12853  dveflem  12865  sinq12gt0  12924  bj-inex  13135  bj-sucexg  13150  bj-peano4  13183  setindis  13195  bdsetindis  13197  bj-inf2vnlem1  13198  exmid1stab  13225  nnsf  13229  nninfalllemn  13232  nninfall  13234  nninfsellemeq  13240  sbthom  13251
  Copyright terms: Public domain W3C validator