ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  a1d GIF version

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 101) 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 51 vs. pm2.43i 47 vs. pm2.43d 48). (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
StepHypRef Expression
1 a1d.1 . 2 (𝜑𝜓)
2 ax-1 5 . 2 (𝜓 → (𝜒𝜓))
31, 2syl 14 1 (𝜑 → (𝜒𝜓))
Colors of variables: wff set class
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  52  syl5d  66  syl6d  68  impbid21d  123  imbi2d  223  adantr  265  jctild  303  jctird  304  pm3.4  320  anbi2d  445  anbi1d  446  pm2.51  591  mtod  599  pm2.76  732  condc  760  pm5.18dc  788  dcim  795  pm2.54dc  801  pm2.85dc  822  dcor  854  anordc  874  xor3dc  1294  biassdc  1302  syl6ci  1350  hbequid  1422  19.30dc  1534  equsalh  1630  equvini  1657  nfsbxyt  1835  modc  1959  euan  1972  moexexdc  2000  nebidc  2300  rgen2a  2392  ralrimivw  2410  reximdv  2437  rexlimdvw  2453  r19.32r  2474  reuind  2767  rabxmdc  3277  rexn0  3347  regexmidlem1  4286  finds1  4353  nn0suc  4355  nndceq0  4367  ssrel2  4458  poltletr  4753  fmptco  5358  nnsucsssuc  6102  fopwdom  6341  fidifsnen  6362  indpi  6498  nnindnn  7025  nnind  8006  nn1m1nn  8008  nn1gt1  8023  nn0n0n1ge2b  8378  xrltnsym  8815  xrlttr  8817  xrltso  8818  xltnegi  8849  fzospliti  9134  elfzonlteqm1  9168  qbtwnxr  9214  modfzo0difsn  9345  iseqfveq2  9392  iseqshft2  9396  monoord  9399  iseqsplit  9402  rexuz3  9817  rexanuz2  9818  dvdsle  10156  dvdsabseq  10159  nno  10218  nn0seqcvgd  10263  bj-nn0suc0  10462
  Copyright terms: Public domain W3C validator