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

Theorem a1d 22
Description: Deduction introducing an embedded antecedent. (The proof was revised by Stefan Allan, 20-Mar-2006.)

Naming convention: We often call a theorem a "deduction" and suffix its label with "d" whenever the hypotheses and conclusion are each prefixed with the same antecedent. This allows us to use the theorem in places where (in traditional textbook formalizations) the standard Deduction Theorem would be used; here  ph would be replaced with a conjunction (wa 102) of the hypotheses of the would-be deduction. By contrast, we tend to call the simpler version with no common antecedent an "inference" and suffix its label with "i"; compare theorem a1i 9. Finally, a "theorem" would be the form with no hypotheses; in this case the "theorem" form would be the original axiom ax-1 5. We usually show the theorem form without a suffix on its label (e.g. pm2.43 52 vs. pm2.43i 48 vs. pm2.43d 49). (Contributed by NM, 5-Aug-1993.) (Revised by NM, 20-Mar-2006.)

Hypothesis
Ref Expression
a1d.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
a1d  |-  ( ph  ->  ( ch  ->  ps ) )

Proof of Theorem a1d
StepHypRef Expression
1 a1d.1 . 2  |-  ( ph  ->  ps )
2 ax-1 5 . 2  |-  ( ps 
->  ( ch  ->  ps ) )
31, 2syl 14 1  |-  ( ph  ->  ( ch  ->  ps ) )
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:  2a1d  23  a1i13  24  2a1i  27  syl5com  29  mpid  41  syld  44  imim2d  53  syl5d  67  syl6d  69  impbid21d  126  imbi2d  228  adantr  270  jctild  309  jctird  310  pm3.4  326  anbi2d  452  anbi1d  453  pm2.51  614  mtod  622  pm2.76  755  condc  783  pm5.18dc  811  dcim  818  pm2.54dc  824  pm2.85dc  845  dcor  877  anordc  898  xor3dc  1319  biassdc  1327  syl6ci  1375  hbequid  1447  19.30dc  1559  equsalh  1655  equvini  1682  nfsbxyt  1861  modc  1985  euan  1998  moexexdc  2026  nebidc  2326  rgen2a  2418  ralrimivw  2436  reximdv  2463  rexlimdvw  2481  r19.32r  2502  reuind  2796  rabxmdc  3283  rexn0  3347  regexmidlem1  4284  finds1  4351  nn0suc  4353  nndceq0  4365  ssrel2  4456  poltletr  4755  fmptco  5362  nnsucsssuc  6136  1domsn  6363  fopwdom  6380  fidifsnen  6405  pr2ne  6520  indpi  6594  nnindnn  7121  nnind  8122  nn1m1nn  8124  nn1gt1  8139  nn0n0n1ge2b  8508  xrltnsym  8944  xrlttr  8946  xrltso  8947  xltnegi  8978  fzospliti  9262  elfzonlteqm1  9296  qbtwnxr  9344  modfzo0difsn  9477  monoord  9551  rexuz3  10014  rexanuz2  10015  dvdsle  10389  dvdsabseq  10392  nno  10450  nn0seqcvgd  10567  lcmdvds  10605  divgcdcoprm0  10627  exprmfct  10663  rpexp1i  10677  bj-nn0suc0  10903
  Copyright terms: Public domain W3C validator