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

Step	Hyp	Ref	Expression
1		a1d.1	. 2 ⊢ (φ → ψ)
2		ax-1 5	. 2 ⊢ (ψ → (χ → ψ))
3	1, 2	syl 14	1 ⊢ (φ → (χ → ψ))

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  7711  nn1m1nn  7713  nn1gt1  7728  nn0n0n1ge2b  8096  xrltnsym  8484  xrlttr  8486  xrltso  8487  xltnegi  8518  fzospliti  8802  elfzonlteqm1  8836  iseqfveq2  8905  bj-nn0suc0  9410