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

Theorem 3syl 17
Description: Inference chaining two syllogisms. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
3syl.1 (𝜑𝜓)
3syl.2 (𝜓𝜒)
3syl.3 (𝜒𝜃)
Assertion
Ref Expression
3syl (𝜑𝜃)

Proof of Theorem 3syl
StepHypRef Expression
1 3syl.1 . . 3 (𝜑𝜓)
2 3syl.2 . . 3 (𝜓𝜒)
31, 2syl 14 . 2 (𝜑𝜒)
4 3syl.3 . 2 (𝜒𝜃)
53, 4syl 14 1 (𝜑𝜃)
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  2690  sbcco3g  2930  snelpwi  3975  opth1  4000  frind  4116  onin  4150  reusv1  4217  xpexg  4479  dmexg  4623  rnexg  4624  relfld  4873  funimaexglem  5009  funimaexg  5010  fabexg  5104  nfvres  5233  funimass4  5251  funconstss  5312  f1oresrab  5356  resfunexg  5409  f1eqcocnv  5458  isores1  5481  isoini  5484  isose  5487  isopolem  5488  isosolem  5490  eusvobj2  5525  acexmidlemcase  5534  oprabid  5564  offval  5746  resfunexgALT  5764  offval3  5788  1stvalg  5796  2ndvalg  5797  1stcof  5817  2ndcof  5818  cnvf1o  5873  tposf12  5914  smores3  5938  smoiso  5947  tfr0  5967  tfrlemibxssdm  5971  tfrlemi14d  5977  tfrexlem  5978  rdgss  6000  frecsuclemdm  6018  nnsucsssuc  6101  swoord1  6165  swoord2  6166  iinerm  6208  eroveu  6227  en1uniel  6314  fopwdom  6340  ac6sfi  6382  supubti  6404  suplubti  6405  isotilem  6409  supisolem  6411  supisoex  6412  supisoti  6413  ordiso2  6414  addclnq  6530  mulclnq  6531  1qec  6543  prarloclemarch2  6574  enq0tr  6589  addclnq0  6606  mulclnq0  6607  nq0m0r  6611  prarloclemlo  6649  prarloc  6658  genpml  6672  genpmu  6673  addnqprl  6684  addnqpru  6685  recnnpr  6703  prmuloc2  6722  1idpru  6746  ltexprlemm  6755  ltexprlemloc  6762  recexprlemm  6779  recexprlem1ssl  6788  caucvgprlemnkj  6821  caucvgprlemnbj  6822  caucvgprlemm  6823  caucvgprlemopl  6824  caucvgprlemlol  6825  caucvgprlemladdfu  6832  caucvgprlemladdrl  6833  caucvgprprlemk  6838  caucvgprprlemloccalc  6839  caucvgprprlemnkltj  6844  caucvgprprlemnjltk  6846  caucvgprprlemml  6849  caucvgprprlemmu  6850  caucvgprprlemlol  6853  caucvgprprlemexb  6862  caucvgprprlem1  6864  addclsr  6895  mulclsr  6896  prsrcl  6925  caucvgsrlemoffcau  6939  peano5nnnn  7023  mulap0r  7679  nn1suc  8008  prime  8395  zindd  8414  xrlttri3  8818  fzopth  9025  fzsuc  9032  fzpred  9033  fzp1ss  9036  fztp  9041  fseq1p1m1  9057  1fv  9097  elfzom1elp1fzo  9159  ssfzo12  9181  fzosplitsn  9190  divfl0  9245  modqid  9298  modqmuladdim  9316  frecuzrdgcl  9362  frecuzrdgsuc  9364  frecfzennn  9366  frecfzen2  9367  iseqsplit  9401  iseqid3s  9409  faclbnd  9608  faclbnd3  9610  bcm1k  9627  cjcj  9710  caucvgre  9807  r19.2uz  9819  resqrexlemgt0  9846  ltabs  9913  nn0o  10218  bj-inex  10400  bj-sucexg  10415  bj-peano4  10453  setindis  10465  bdsetindis  10467  bj-inf2vnlem1  10468
  Copyright terms: Public domain W3C validator