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

Theorem syld 45
Description: Syllogism deduction.

Notice that syld 45 has the same form as syl 14 with 𝜑 added in front of each hypothesis and conclusion. When all theorems referenced in a proof are converted in this way, we can replace 𝜑 with a hypothesis of the proof, allowing the hypothesis to be eliminated with id 19 and become an antecedent. The Deduction Theorem for propositional calculus, e.g. Theorem 3 in [Margaris] p. 56, tells us that this procedure is always possible. (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 19-Feb-2008.) (Proof shortened by Wolf Lammen, 3-Aug-2012.)

Hypotheses
Ref Expression
syld.1 (𝜑 → (𝜓𝜒))
syld.2 (𝜑 → (𝜒𝜃))
Assertion
Ref Expression
syld (𝜑 → (𝜓𝜃))

Proof of Theorem syld
StepHypRef Expression
1 syld.1 . 2 (𝜑 → (𝜓𝜒))
2 syld.2 . . 3 (𝜑 → (𝜒𝜃))
32a1d 22 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
41, 3mpdd 41 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  syldc  46  3syld  57  sylsyld  58  sylibd  148  sylbid  149  sylibrd  168  sylbird  169  syland  289  animpimp2impd  531  nsyld  620  pm5.21ndd  677  mtord  755  pm2.521gdc  836  pm5.11dc  877  anordc  923  hbimd  1535  alrimdd  1571  dral1  1691  sbiedh  1743  ax10oe  1751  sbequi  1793  sbcomxyyz  1921  mo2icl  2834  trel3  4002  exmidsssnc  4094  poss  4188  sess2  4228  abnexg  4335  funun  5135  ssimaex  5448  f1imass  5641  isores3  5682  isoselem  5687  f1dmex  5980  f1o2ndf1  6091  smoel  6163  tfrlem9  6182  nntri1  6358  nnaordex  6389  ertr  6410  swoord2  6425  findcard2s  6750  pr2ne  7014  addnidpig  7108  ordpipqqs  7146  enq0tr  7206  prloc  7263  addnqprl  7301  addnqpru  7302  mulnqprl  7340  mulnqpru  7341  recexprlemss1l  7407  recexprlemss1u  7408  cauappcvgprlemdisj  7423  mulcmpblnr  7513  ltsrprg  7519  mulextsr1lem  7552  map2psrprg  7577  apreap  8312  mulext1  8337  mulext  8339  mulge0  8344  recexap  8374  lemul12b  8576  mulgt1  8578  lbreu  8660  nnrecgt0  8715  bndndx  8927  uzind  9113  fzind  9117  fnn0ind  9118  xlesubadd  9606  icoshft  9713  zltaddlt1le  9729  fzen  9763  elfz1b  9810  elfz0fzfz0  9843  elfzmlbp  9849  fzo1fzo0n0  9900  elfzo0z  9901  fzofzim  9905  elfzodifsumelfzo  9918  modqadd1  10074  modqmul1  10090  frecuzrdgtcl  10125  frecuzrdgfunlem  10132  monoord  10189  seq3coll  10525  caucvgrelemcau  10692  caucvgre  10693  absext  10775  absle  10801  cau3lem  10826  icodiamlt  10892  climuni  11002  mulcn2  11021  cvgratnnlemnexp  11233  cvgratnnlemmn  11234  dvds2lem  11401  dvdsabseq  11441  dfgcd2  11598  algcvga  11628  coprmgcdb  11665  coprmdvds2  11670  isprm3  11695  prmdvdsfz  11715  coprm  11718  rpexp12i  11729  sqrt2irr  11736  dfphi2  11791  strsetsid  11887  cncnp  12294  cncnp2m  12295  cnptopresti  12302  lmtopcnp  12314  txcnp  12335  txlm  12343  cnmptcom  12362  bldisj  12465  blssps  12491  blss  12492  metcnp3  12575  rescncf  12632  dedekindeulemloc  12661  bj-sbimedh  12780  decidin  12806  bj-nnelirr  12953
  Copyright terms: Public domain W3C validator