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  452  anbi1d  453  pm2.51  614  mtod  622  pm2.76  755  condc  783  pm5.18dc  811  dcim  818  pm2.54dc  824  pm2.85dc  845  dcor  877  anordc  898  xor3dc  1319  biassdc  1327  syl6ci  1375  hbequid  1447  19.30dc  1559  equsalh  1656  equvini  1683  nfsbxyt  1862  modc  1986  euan  1999  moexexdc  2027  nebidc  2329  rgen2a  2423  ralrimivw  2441  reximdv  2468  rexlimdvw  2486  r19.32r  2507  reuind  2806  rabxmdc  3297  rexn0  3361  regexmidlem1  4311  finds1  4379  nn0suc  4381  nndceq0  4393  ssrel2  4485  poltletr  4786  fmptco  5405  nnsucsssuc  6184  map1  6458  1domsn  6464  fopwdom  6481  mapxpen  6493  fidifsnen  6515  eldju2ndl  6669  eldju2ndr  6670  finomni  6700  fodjuomnilemdc  6703  pr2ne  6722  exmidfodomrlemim  6729  indpi  6803  nnindnn  7330  nnind  8331  nn1m1nn  8333  nn1gt1  8348  nn0n0n1ge2b  8721  xrltnsym  9157  xrlttr  9159  xrltso  9160  xltnegi  9191  fzospliti  9475  elfzonlteqm1  9509  qbtwnxr  9557  modfzo0difsn  9690  monoord  9769  rexuz3  10249  rexanuz2  10250  dvdsle  10624  dvdsabseq  10627  nno  10685  nn0seqcvgd  10802  lcmdvds  10840  divgcdcoprm0  10862  exprmfct  10898  rpexp1i  10912  phibndlem  10971  bj-nn0suc0  11187