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 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	⊢ (𝜑 → 𝜓)

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:  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  451  anbi1d  452  pm2.51  613  mtod  621  pm2.76  754  condc  782  pm5.18dc  810  dcim  817  pm2.54dc  823  pm2.85dc  844  dcor  876  anordc  897  xor3dc  1318  biassdc  1326  syl6ci  1374  hbequid  1446  19.30dc  1558  equsalh  1654  equvini  1681  nfsbxyt  1860  modc  1984  euan  1997  moexexdc  2025  nebidc  2325  rgen2a  2417  ralrimivw  2435  reximdv  2462  rexlimdvw  2480  r19.32r  2501  reuind  2795  rabxmdc  3276  rexn0  3339  regexmidlem1  4276  finds1  4343  nn0suc  4345  nndceq0  4357  ssrel2  4448  poltletr  4745  fmptco  5351  nnsucsssuc  6094  fopwdom  6333  fidifsnen  6355  pr2ne  6461  indpi  6532  nnindnn  7059  nnind  8055  nn1m1nn  8057  nn1gt1  8072  nn0n0n1ge2b  8427  xrltnsym  8868  xrlttr  8870  xrltso  8871  xltnegi  8902  fzospliti  9185  elfzonlteqm1  9219  qbtwnxr  9266  modfzo0difsn  9397  iseqfveq2  9448  iseqshft2  9452  monoord  9455  iseqsplit  9458  rexuz3  9876  rexanuz2  9877  dvdsle  10244  dvdsabseq  10247  nno  10306  nn0seqcvgd  10423  lcmdvds  10461  divgcdcoprm0  10483  exprmfct  10519  rpexp1i  10533  bj-nn0suc0  10745