New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  a1d GIF version

Theorem a1d 22
 Description: Deduction introducing an embedded antecedent. 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 (df-an 360) 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 10. 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). When an inference is converted to a theorem by eliminating an "is a set" hypothesis, we sometimes suffix the theorem form with "g" (for "more general") as in uniex 4317 vs. uniexg 4316. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Stefan Allan, 20-Mar-2006.)
Hypothesis
Ref Expression
a1d.1 (φψ)
Assertion
Ref Expression
a1d (φ → (χψ))

Proof of Theorem a1d
StepHypRef Expression
1 a1d.1 . 2 (φψ)
2 ax-1 5 . 2 (ψ → (χψ))
31, 2syl 15 1 (φ → (χψ))
 Colors of variables: wff setvar class Syntax hints:   → wi 4 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8 This theorem is referenced by:  2a1i  24  syl5com  26  mpid  37  syld  40  imim2d  48  syl5d  62  syl6d  64  pm2.21d  98  pm2.24d  135  pm2.51  145  pm2.521  146  pm2.61iii  159  mtod  168  impbid21d  182  imbi2d  307  adantr  451  jctild  527  jctird  528  pm3.4  544  anbi2d  684  anbi1d  685  3ecase  1286  ee21  1375  meredith  1404  equsalhwOLD  1839  dvelimv  1939  equsal  1960  dvelimh  1964  equvini  1987  equveli  1988  ax11v  2096  sbal1  2126  dvelimALT  2133  ax11  2155  hbequid  2160  dvelimf-o  2180  ax11eq  2193  ax11el  2194  ax11indalem  2197  ax11inda2ALT  2198  ax11inda2  2199  euan  2261  moexex  2273  rgen2a  2680  ralrimivw  2698  reximdv  2725  rexlimdvw  2741  reuind  3039  rexn0  3652  nnc0suc  4412  prepeano4  4451  tfinltfin  4501  spfininduct  4540  xpexr  5109  fveqres  5355  fconst5  5455  ndmovord  5620  ce0addcnnul  6179  nmembers1lem3  6270  nchoicelem12  6300
 Copyright terms: Public domain W3C validator