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  1509  19.9hd  1625  equsexd  1692  sbcof2  1766  aev  1768  sbequi  1795  nfsbd  1928  mo2n  2005  eupickb  2058  r19.29af2  2549  spc2gv  2750  spc3gv  2752  eqvincg  2783  sbcco3g  3027  ssrmof  3130  exmidsssnc  4096  snelpwi  4104  opth1  4128  frind  4244  onin  4278  abnexg  4337  reusv1  4349  xpexg  4623  dmexg  4773  rnexg  4774  relfld  5037  funimaexglem  5176  funimaexg  5177  fabexg  5280  fsnd  5378  nfvres  5422  funimass4  5440  elfvmptrab1  5483  funconstss  5506  f1oresrab  5553  resfunexg  5609  f1eqcocnv  5660  isores1  5683  isoini  5687  isose  5690  isopolem  5691  isosolem  5693  eusvobj2  5728  acexmidlemcase  5737  oprabid  5771  offval  5957  resfunexgALT  5976  offval3  6000  1stvalg  6008  2ndvalg  6009  1stcof  6029  2ndcof  6030  cnvf1o  6090  tposf12  6134  smores3  6158  smoiso  6167  tfr0dm  6187  tfrlemibxssdm  6192  tfrlemi14d  6198  tfrexlem  6199  tfr1onlemssrecs  6204  tfr1onlemsucfn  6205  tfr1onlemsucaccv  6206  tfr1onlembxssdm  6208  tfr1onlemres  6214  tfri1dALT  6216  tfrcllemssrecs  6217  tfrcllemsucfn  6218  tfrcllemsucaccv  6219  tfrcllembxssdm  6221  tfrcllemres  6227  rdgss  6248  nnsucsssuc  6356  nntr2  6367  swoord1  6426  swoord2  6427  iinerm  6469  eroveu  6488  pmresg  6538  en1uniel  6666  fopwdom  6698  xpen  6707  ssenen  6713  isinfinf  6759  ac6sfi  6760  preimaf1ofi  6807  sbthlem1  6813  fi0  6831  fiss  6833  supubti  6854  suplubti  6855  isotilem  6861  supisolem  6863  supisoex  6864  supisoti  6865  ordiso2  6888  eldju1st  6924  eldju2ndl  6925  updjud  6935  djudom  6946  ctmlemr  6961  enumctlemm  6967  ctssexmid  6992  exmidonfinlem  7017  en2other2  7020  exmidaclem  7032  addclnq  7151  mulclnq  7152  1qec  7164  prarloclemarch2  7195  enq0tr  7210  addclnq0  7227  mulclnq0  7228  nq0m0r  7232  prarloclemlo  7270  prarloc  7279  genpml  7293  genpmu  7294  addnqprl  7305  addnqpru  7306  recnnpr  7324  prmuloc2  7343  1idpru  7367  ltexprlemm  7376  ltexprlemloc  7383  recexprlemm  7400  recexprlem1ssl  7409  caucvgprlemnkj  7442  caucvgprlemnbj  7443  caucvgprlemm  7444  caucvgprlemopl  7445  caucvgprlemlol  7446  caucvgprlemladdfu  7453  caucvgprlemladdrl  7454  caucvgprprlemk  7459  caucvgprprlemloccalc  7460  caucvgprprlemnkltj  7465  caucvgprprlemnjltk  7467  caucvgprprlemml  7470  caucvgprprlemmu  7471  caucvgprprlemlol  7474  caucvgprprlemexb  7483  caucvgprprlem1  7485  suplocexprlemml  7492  suplocexprlemlub  7500  addclsr  7529  mulclsr  7530  prsrcl  7560  caucvgsrlemoffcau  7574  peano5nnnn  7668  mulap0r  8344  nn1suc  8703  prime  9108  zindd  9127  xrlttri3  9538  xnn0xadd0  9605  fzopth  9796  fzsuc  9804  fzpred  9805  fzp1ss  9808  fztp  9813  fseq1p1m1  9829  1fv  9871  elfzom1elp1fzo  9934  ssfzo12  9956  fzosplitsn  9965  divfl0  10024  modqid  10077  modqmuladdim  10095  frecuzrdgtcl  10140  frecuzrdgfunlem  10147  frecfzennn  10154  frecfzen2  10155  seq3val  10186  seqvalcd  10187  iseqf1olemqcl  10214  iseqf1olemnab  10216  iseqf1olemmo  10220  iseqf1olemqk  10222  seq3f1olemstep  10229  seq3id3  10235  faclbnd  10442  faclbnd3  10444  bcm1k  10461  hashfz1  10484  focdmex  10488  hashfz  10522  hashfzp1  10525  hashfacen  10534  leisorel  10535  cjcj  10610  caucvgre  10708  r19.2uz  10720  resqrexlemgt0  10747  ltabs  10814  xrmaxiflemab  10971  xrmaxiflemlub  10972  isummolemnm  11103  summodclem2a  11105  fsumf1o  11114  fisum0diag2  11171  modfsummodlemstep  11181  fsumparts  11194  ef0lem  11280  resinval  11336  recosval  11337  demoivreALT  11394  nn0o  11516  zsupcllemstep  11550  zsupcllemex  11551  infssuzledc  11555  gcdmultiplez  11621  dvdssq  11631  eucalg  11652  lcmgcdnn  11675  dvdsnprmd  11718  prm2orodd  11719  qnumdenbi  11781  nn0gcdsq  11789  phibnd  11804  hashdvds  11808  phimullem  11812  hashgcdlem  11814  unennn  11821  ennnfonelemk  11824  ennnfonelemjn  11826  ennnfonelemhf1o  11837  ennnfonelemex  11838  ennnfonelemf1  11842  ennnfonelemrn  11843  qnnen  11855  setsfun0  11906  srngbased  11993  srngplusgd  11994  srngmulrd  11995  srnginvld  11996  lmodbased  12004  lmodplusgd  12005  lmodscad  12006  lmodvscad  12007  ipsbased  12012  ipsaddgd  12013  ipsmulrd  12014  ipsscad  12015  ipsvscad  12016  ipsipd  12017  tgval  12129  cldval  12179  ntrfval  12180  clsfval  12181  neifval  12220  neif  12221  neival  12223  cnclima  12303  cncnpi  12308  cnrest2  12316  cnrest2r  12317  cnptoprest  12319  cnpdis  12322  txvalex  12334  txval  12335  txcnmpt  12353  txdis  12357  cnmpt1t  12365  cnmpt2t  12373  hmeocnv  12387  hmeontr  12393  txhmeo  12399  xmetunirn  12438  xmettpos  12450  metn0  12458  xmetres  12462  metres  12463  blrnps  12491  blrn  12492  blin2  12512  blbas  12513  xmeterval  12515  xmettxlem  12589  xmettx  12590  metcnpi  12595  reldvg  12728  dvaddxx  12747  dvmulxx  12748  dviaddf  12749  dvimulf  12750  dvfre  12754  dveflem  12766  sinq12gt0  12822  bj-inex  13001  bj-sucexg  13016  bj-peano4  13049  setindis  13061  bdsetindis  13063  bj-inf2vnlem1  13064  exmid1stab  13091  nnsf  13095  nninfalllemn  13098  nninfall  13100  nninfsellemeq  13106  sbthom  13117
  Copyright terms: Public domain W3C validator