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  hbim  1437  19.9hd  1552  equsexd  1617  sbcof2  1691  aev  1693  sbequi  1720  nfsbd  1851  mo2n  1928  eupickb  1981  r19.29af2  2452  spc2gv  2643  spc3gv  2645  eqvincg  2668  sbcco3g  2903  snelpwi  3948  opth1  3973  frind  4089  onin  4123  reusv1  4190  xpexg  4452  dmexg  4596  rnexg  4597  relfld  4846  funimaexglem  4982  funimaexg  4983  fabexg  5077  nfvres  5206  funimass4  5224  funconstss  5285  f1oresrab  5329  resfunexg  5382  f1eqcocnv  5431  isores1  5454  isoini  5457  isose  5460  isopolem  5461  isosolem  5463  eusvobj2  5498  acexmidlemcase  5507  oprabid  5537  offval  5719  resfunexgALT  5737  offval3  5761  1stvalg  5769  2ndvalg  5770  1stcof  5790  2ndcof  5791  cnvf1o  5846  tposf12  5884  smores3  5908  smoiso  5917  tfr0  5937  tfrlemibxssdm  5941  tfrlemi14d  5947  tfrexlem  5948  rdgss  5970  frecsuclemdm  5988  nnsucsssuc  6071  swoord1  6135  swoord2  6136  iinerm  6178  eroveu  6197  en1uniel  6284  fopwdom  6310  ac6sfi  6352  ordiso2  6355  addclnq  6471  mulclnq  6472  1qec  6484  prarloclemarch2  6515  enq0tr  6530  addclnq0  6547  mulclnq0  6548  nq0m0r  6552  prarloclemlo  6590  prarloc  6599  genpml  6613  genpmu  6614  addnqprl  6625  addnqpru  6626  recnnpr  6644  prmuloc2  6663  1idpru  6687  ltexprlemm  6696  ltexprlemloc  6703  recexprlemm  6720  recexprlem1ssl  6729  caucvgprlemnkj  6762  caucvgprlemnbj  6763  caucvgprlemm  6764  caucvgprlemopl  6765  caucvgprlemlol  6766  caucvgprlemladdfu  6773  caucvgprlemladdrl  6774  caucvgprprlemk  6779  caucvgprprlemloccalc  6780  caucvgprprlemnkltj  6785  caucvgprprlemnjltk  6787  caucvgprprlemml  6790  caucvgprprlemmu  6791  caucvgprprlemlol  6794  caucvgprprlemexb  6803  caucvgprprlem1  6805  addclsr  6836  mulclsr  6837  prsrcl  6866  caucvgsrlemoffcau  6880  peano5nnnn  6964  mulap0r  7604  nn1suc  7931  prime  8335  zindd  8354  xrlttri3  8716  fzopth  8922  fzsuc  8929  fzpred  8930  fzp1ss  8933  fztp  8938  fseq1p1m1  8954  1fv  8994  elfzom1elp1fzo  9056  ssfzo12  9078  fzosplitsn  9087  divfl0  9136  frecuzrdgcl  9173  frecuzrdgsuc  9175  frecfzennn  9177  frecfzen2  9178  iseqsplit  9212  iseqid3s  9220  cjcj  9457  caucvgre  9554  r19.2uz  9565  resqrexlemgt0  9592  ltabs  9657  bj-inex  10001  bj-sucexg  10016  bj-peano4  10054  setindis  10066  bdsetindis  10068  bj-inf2vnlem1  10069
  Copyright terms: Public domain W3C validator