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:  2a1i  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  581  mtod  589  pm2.76  721  condc  749  pm5.18dc  777  dcim  784  pm2.54dc  790  pm2.85dc  811  dcor  843  anordc  863  xor3dc  1278  biassdc  1286  syl6ci  1334  hbequid  1406  19.30dc  1518  equsalh  1614  equvini  1641  nfsbxyt  1819  modc  1943  euan  1956  moexexdc  1984  nebidc  2285  rgen2a  2375  ralrimivw  2393  reximdv  2420  rexlimdvw  2436  r19.32r  2457  reuind  2744  rabxmdc  3249  rexn0  3319  regexmidlem1  4258  finds1  4325  nn0suc  4327  nndceq0  4339  ssrel2  4430  poltletr  4725  fmptco  5330  nnsucsssuc  6071  fopwdom  6310  fidifsnen  6331  indpi  6440  nnindnn  6967  nnind  7930  nn1m1nn  7932  nn1gt1  7947  nn0n0n1ge2b  8320  xrltnsym  8714  xrlttr  8716  xrltso  8717  xltnegi  8748  fzospliti  9032  elfzonlteqm1  9066  iseqfveq2  9228  iseqshft2  9232  monoord  9235  iseqsplit  9238  rexuz3  9588  rexanuz2  9589  nn0seqcvgd  9880  bj-nn0suc0  10075