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-1 5  ax-2 6  ax-mp 7
This theorem is referenced by:  4syl  18  simpl2im  372  hbim  1453  19.9hd  1568  equsexd  1633  sbcof2  1707  aev  1709  sbequi  1736  nfsbd  1867  mo2n  1944  eupickb  1997  r19.29af2  2469  spc2gv  2660  spc3gv  2662  eqvincg  2691  sbcco3g  2931  snelpwi  3976  opth1  4001  frind  4117  onin  4151  reusv1  4218  xpexg  4480  dmexg  4624  rnexg  4625  relfld  4874  funimaexglem  5010  funimaexg  5011  fabexg  5105  nfvres  5234  funimass4  5252  funconstss  5313  f1oresrab  5357  resfunexg  5410  f1eqcocnv  5459  isores1  5482  isoini  5485  isose  5488  isopolem  5489  isosolem  5491  eusvobj2  5526  acexmidlemcase  5535  oprabid  5565  offval  5747  resfunexgALT  5765  offval3  5789  1stvalg  5797  2ndvalg  5798  1stcof  5818  2ndcof  5819  cnvf1o  5874  tposf12  5915  smores3  5939  smoiso  5948  tfr0  5968  tfrlemibxssdm  5972  tfrlemi14d  5978  tfrexlem  5979  rdgss  6001  frecsuclemdm  6019  nnsucsssuc  6102  swoord1  6166  swoord2  6167  iinerm  6209  eroveu  6228  en1uniel  6315  fopwdom  6341  ac6sfi  6383  supubti  6405  suplubti  6406  isotilem  6410  supisolem  6412  supisoex  6413  supisoti  6414  ordiso2  6415  addclnq  6531  mulclnq  6532  1qec  6544  prarloclemarch2  6575  enq0tr  6590  addclnq0  6607  mulclnq0  6608  nq0m0r  6612  prarloclemlo  6650  prarloc  6659  genpml  6673  genpmu  6674  addnqprl  6685  addnqpru  6686  recnnpr  6704  prmuloc2  6723  1idpru  6747  ltexprlemm  6756  ltexprlemloc  6763  recexprlemm  6780  recexprlem1ssl  6789  caucvgprlemnkj  6822  caucvgprlemnbj  6823  caucvgprlemm  6824  caucvgprlemopl  6825  caucvgprlemlol  6826  caucvgprlemladdfu  6833  caucvgprlemladdrl  6834  caucvgprprlemk  6839  caucvgprprlemloccalc  6840  caucvgprprlemnkltj  6845  caucvgprprlemnjltk  6847  caucvgprprlemml  6850  caucvgprprlemmu  6851  caucvgprprlemlol  6854  caucvgprprlemexb  6863  caucvgprprlem1  6865  addclsr  6896  mulclsr  6897  prsrcl  6926  caucvgsrlemoffcau  6940  peano5nnnn  7024  mulap0r  7680  nn1suc  8009  prime  8396  zindd  8415  xrlttri3  8819  fzopth  9026  fzsuc  9033  fzpred  9034  fzp1ss  9037  fztp  9042  fseq1p1m1  9058  1fv  9098  elfzom1elp1fzo  9160  ssfzo12  9182  fzosplitsn  9191  divfl0  9246  modqid  9299  modqmuladdim  9317  frecuzrdgcl  9363  frecuzrdgsuc  9365  frecfzennn  9367  frecfzen2  9368  iseqsplit  9402  iseqid3s  9410  faclbnd  9609  faclbnd3  9611  bcm1k  9628  cjcj  9711  caucvgre  9808  r19.2uz  9820  resqrexlemgt0  9847  ltabs  9914  nn0o  10219  bj-inex  10414  bj-sucexg  10429  bj-peano4  10467  setindis  10479  bdsetindis  10481  bj-inf2vnlem1  10482
  Copyright terms: Public domain W3C validator