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  6357  addclnq  6473  mulclnq  6474  1qec  6486  prarloclemarch2  6517  enq0tr  6532  addclnq0  6549  mulclnq0  6550  nq0m0r  6554  prarloclemlo  6592  prarloc  6601  genpml  6615  genpmu  6616  addnqprl  6627  addnqpru  6628  recnnpr  6646  prmuloc2  6665  1idpru  6689  ltexprlemm  6698  ltexprlemloc  6705  recexprlemm  6722  recexprlem1ssl  6731  caucvgprlemnkj  6764  caucvgprlemnbj  6765  caucvgprlemm  6766  caucvgprlemopl  6767  caucvgprlemlol  6768  caucvgprlemladdfu  6775  caucvgprlemladdrl  6776  caucvgprprlemk  6781  caucvgprprlemloccalc  6782  caucvgprprlemnkltj  6787  caucvgprprlemnjltk  6789  caucvgprprlemml  6792  caucvgprprlemmu  6793  caucvgprprlemlol  6796  caucvgprprlemexb  6805  caucvgprprlem1  6807  addclsr  6838  mulclsr  6839  prsrcl  6868  caucvgsrlemoffcau  6882  peano5nnnn  6966  mulap0r  7606  nn1suc  7933  prime  8337  zindd  8356  xrlttri3  8718  fzopth  8924  fzsuc  8931  fzpred  8932  fzp1ss  8935  fztp  8940  fseq1p1m1  8956  1fv  8996  elfzom1elp1fzo  9058  ssfzo12  9080  fzosplitsn  9089  divfl0  9138  frecuzrdgcl  9199  frecuzrdgsuc  9201  frecfzennn  9203  frecfzen2  9204  iseqsplit  9238  iseqid3s  9246  cjcj  9483  caucvgre  9580  r19.2uz  9591  resqrexlemgt0  9618  ltabs  9683  bj-inex  10027  bj-sucexg  10042  bj-peano4  10080  setindis  10092  bdsetindis  10094  bj-inf2vnlem1  10095
  Copyright terms: Public domain W3C validator