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  440  anbi1d  441  pm2.51  568  mtod  576  pm2.76  708  condc  740  pm5.18dc  770  dcim  777  pm2.54dc  783  pm2.85dc  804  dcor  831  anordc  851  xor3dc  1261  biassdc  1269  ee21  1313  hbequid  1387  19.30dc  1500  equsalh  1596  equvini  1623  nfsbxyt  1801  modc  1925  euan  1938  moexexdc  1966  nebidc  2263  rgen2a  2353  ralrimivw  2371  reximdv  2398  rexlimdvw  2414  r19.32r  2435  reuind  2721  rabxmdc  3226  rexn0  3298  regexmidlem1  4202  finds1  4252  nn0suc  4254  nndceq0  4266  ssrel2  4357  poltletr  4652  fmptco  5255  nnsucsssuc  5986  bj-nn0suc0  7172