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  291  animpimp2impd  549  nsyld  638  pm5.21ndd  695  mtord  773  pm2.521gdc  854  pm5.11dc  895  anordc  941  hbimd  1553  alrimdd  1589  dral1  1709  sbiedh  1761  ax10oe  1770  sbequi  1812  sbcomxyyz  1946  mo2icl  2868  trel3  4043  exmidsssnc  4136  poss  4230  sess2  4270  abnexg  4377  funun  5178  ssimaex  5493  f1imass  5686  isores3  5727  isoselem  5732  f1dmex  6025  f1o2ndf1  6136  smoel  6208  tfrlem9  6227  nntri1  6403  nnaordex  6434  ertr  6455  swoord2  6470  findcard2s  6795  pr2ne  7075  addnidpig  7195  ordpipqqs  7233  enq0tr  7293  prloc  7350  addnqprl  7388  addnqpru  7389  mulnqprl  7427  mulnqpru  7428  recexprlemss1l  7494  recexprlemss1u  7495  cauappcvgprlemdisj  7510  mulcmpblnr  7600  ltsrprg  7606  mulextsr1lem  7639  map2psrprg  7664  apreap  8400  mulext1  8425  mulext  8427  mulge0  8432  recexap  8465  lemul12b  8670  mulgt1  8672  lbreu  8754  nnrecgt0  8809  bndndx  9027  uzind  9213  fzind  9217  fnn0ind  9218  xlesubadd  9723  icoshft  9830  zltaddlt1le  9847  fzen  9881  elfz1b  9928  elfz0fzfz0  9961  elfzmlbp  9967  fzo1fzo0n0  10018  elfzo0z  10019  fzofzim  10023  elfzodifsumelfzo  10036  modqadd1  10192  modqmul1  10208  frecuzrdgtcl  10243  frecuzrdgfunlem  10250  monoord  10307  seq3coll  10644  caucvgrelemcau  10811  caucvgre  10812  absext  10894  absle  10920  cau3lem  10945  icodiamlt  11011  climuni  11121  mulcn2  11140  cvgratnnlemnexp  11352  cvgratnnlemmn  11353  fprodssdc  11418  dvds2lem  11575  dvdsabseq  11615  dfgcd2  11772  algcvga  11802  coprmgcdb  11839  coprmdvds2  11844  isprm3  11869  prmdvdsfz  11889  coprm  11892  rpexp12i  11903  sqrt2irr  11910  dfphi2  11966  strsetsid  12065  cncnp  12472  cncnp2m  12473  cnptopresti  12480  lmtopcnp  12492  txcnp  12513  txlm  12521  cnmptcom  12540  bldisj  12643  blssps  12669  blss  12670  metcnp3  12753  rescncf  12810  dedekindeulemloc  12839  dedekindicclemloc  12848  sincosq1lem  12988  sinq12gt0  12993  logbgcd1irr  13126  bj-sbimedh  13187  decidin  13213  bj-charfunbi  13224  bj-nnelirr  13366
 Copyright terms: Public domain W3C validator