ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  a1d Structured version   GIF 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 φ would be replaced with a conjunction (wa 97) 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 47 vs. pm2.43i 43 vs. pm2.43d 44). (Contributed by NM, 5-Aug-1993.) (Revised by NM, 20-Mar-2006.)

Hypothesis
Ref Expression
a1d.1 (φψ)
Assertion
Ref Expression
a1d (φ → (χψ))

Proof of Theorem a1d
StepHypRef Expression
1 a1d.1 . 2 (φψ)
2 ax-1 5 . 2 (ψ → (χψ))
31, 2syl 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:  a1ii  24  syl5com  26  mpid  37  syld  40  imim2d  48  syl5d  62  syl6d  64  impbid21d  119  imbi2d  219  adantr  261  jctild  299  jctird  300  pm3.4  316  anbi2d  437  anbi1d  438  pm2.51  580  mtod  588  pm2.76  720  condc  748  pm5.18dc  776  dcim  783  pm2.54dc  789  pm2.85dc  810  dcor  842  anordc  862  xor3dc  1275  biassdc  1283  syl6ci  1331  hbequid  1403  19.30dc  1515  equsalh  1611  equvini  1638  nfsbxyt  1816  modc  1940  euan  1953  moexexdc  1981  nebidc  2279  rgen2a  2369  ralrimivw  2387  reximdv  2414  rexlimdvw  2430  r19.32r  2451  reuind  2738  rabxmdc  3243  rexn0  3313  regexmidlem1  4218  finds1  4268  nn0suc  4270  nndceq0  4282  ssrel2  4373  poltletr  4668  fmptco  5273  nnsucsssuc  6010  fopwdom  6246  indpi  6326  nnind  7671  nn1m1nn  7673  nn1gt1  7688  nn0n0n1ge2b  8056  xrltnsym  8444  xrlttr  8446  xrltso  8447  xltnegi  8478  fzospliti  8762  elfzonlteqm1  8796  iseqfveq2  8865  bj-nn0suc0  9338
  Copyright terms: Public domain W3C validator