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  378  hbim  1480  19.9hd  1595  equsexd  1661  sbcof2  1735  aev  1737  sbequi  1764  nfsbd  1896  mo2n  1973  eupickb  2026  r19.29af2  2504  spc2gv  2702  spc3gv  2704  eqvincg  2732  sbcco3g  2974  snelpwi  4013  opth1  4037  frind  4153  onin  4187  reusv1  4254  xpexg  4520  dmexg  4665  rnexg  4666  relfld  4925  funimaexglem  5062  funimaexg  5063  fabexg  5161  nfvres  5300  funimass4  5318  funconstss  5380  f1oresrab  5426  resfunexg  5479  f1eqcocnv  5531  isores1  5554  isoini  5558  isose  5561  isopolem  5562  isosolem  5564  eusvobj2  5599  acexmidlemcase  5608  oprabid  5638  offval  5820  resfunexgALT  5838  offval3  5862  1stvalg  5870  2ndvalg  5871  1stcof  5891  2ndcof  5892  cnvf1o  5947  tposf12  5988  smores3  6012  smoiso  6021  tfr0dm  6041  tfrlemibxssdm  6046  tfrlemi14d  6052  tfrexlem  6053  tfr1onlemssrecs  6058  tfr1onlemsucfn  6059  tfr1onlemsucaccv  6060  tfr1onlembxssdm  6062  tfr1onlemres  6068  tfri1dALT  6070  tfrcllemssrecs  6071  tfrcllemsucfn  6072  tfrcllemsucaccv  6073  tfrcllembxssdm  6075  tfrcllemres  6081  rdgss  6102  nnsucsssuc  6207  swoord1  6273  swoord2  6274  iinerm  6316  eroveu  6335  pmresg  6385  en1uniel  6473  fopwdom  6504  xpen  6513  ssenen  6519  isinfinf  6565  ac6sfi  6566  preimaf1ofi  6609  sbthlem1  6610  supubti  6638  suplubti  6639  isotilem  6645  supisolem  6647  supisoex  6648  supisoti  6649  ordiso2  6672  djur  6701  eldju1st  6706  eldju2ndl  6707  updjud  6717  djudom  6731  en2other2  6766  addclnq  6878  mulclnq  6879  1qec  6891  prarloclemarch2  6922  enq0tr  6937  addclnq0  6954  mulclnq0  6955  nq0m0r  6959  prarloclemlo  6997  prarloc  7006  genpml  7020  genpmu  7021  addnqprl  7032  addnqpru  7033  recnnpr  7051  prmuloc2  7070  1idpru  7094  ltexprlemm  7103  ltexprlemloc  7110  recexprlemm  7127  recexprlem1ssl  7136  caucvgprlemnkj  7169  caucvgprlemnbj  7170  caucvgprlemm  7171  caucvgprlemopl  7172  caucvgprlemlol  7173  caucvgprlemladdfu  7180  caucvgprlemladdrl  7181  caucvgprprlemk  7186  caucvgprprlemloccalc  7187  caucvgprprlemnkltj  7192  caucvgprprlemnjltk  7194  caucvgprprlemml  7197  caucvgprprlemmu  7198  caucvgprprlemlol  7201  caucvgprprlemexb  7210  caucvgprprlem1  7212  addclsr  7243  mulclsr  7244  prsrcl  7273  caucvgsrlemoffcau  7287  peano5nnnn  7371  mulap0r  8033  nn1suc  8376  prime  8778  zindd  8797  xrlttri3  9199  fzopth  9406  fzsuc  9413  fzpred  9414  fzp1ss  9417  fztp  9422  fseq1p1m1  9438  1fv  9478  elfzom1elp1fzo  9541  ssfzo12  9563  fzosplitsn  9572  divfl0  9631  modqid  9684  modqmuladdim  9702  frecuzrdgtcl  9747  frecuzrdgfunlem  9754  frecfzennn  9761  frecfzen2  9762  iseqvalt  9790  iseqsplit  9812  iseqf1olemqcl  9819  iseqf1olemnab  9821  iseqf1olemmo  9825  iseqf1olemqk  9827  iseqf1olemstep  9834  iseqid3s  9841  faclbnd  10045  faclbnd3  10047  bcm1k  10064  hashfz1  10087  focdmex  10091  hashfz  10125  hashfzp1  10128  hashfacen  10137  leisorel  10138  cjcj  10212  caucvgre  10309  r19.2uz  10321  resqrexlemgt0  10348  ltabs  10415  isummolemnm  10658  isummolem2a  10660  fsumf1o  10668  nn0o  10782  zsupcllemstep  10816  zsupcllemex  10817  infssuzledc  10821  gcdmultiplez  10885  dvdssq  10895  eucialg  10916  lcmgcdnn  10939  dvdsnprmd  10982  prm2orodd  10983  qnumdenbi  11045  nn0gcdsq  11053  phibnd  11068  hashdvds  11072  phimullem  11076  hashgcdlem  11078  unennn  11085  bj-inex  11236  bj-sucexg  11251  bj-peano4  11288  setindis  11300  bdsetindis  11302  bj-inf2vnlem1  11303  nnsf  11333  nninfalllemn  11336  nninfall  11338  nninfsellemeq  11344
  Copyright terms: Public domain W3C validator