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 103) 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 6. We usually show the theorem form without a suffix on its label (e.g. pm2.43 53 versus pm2.43i 49 versus pm2.43d 50). (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 6 . 2 (𝜓 → (𝜒𝜓))
31, 2syl 14 1 (𝜑 → (𝜒𝜓))
 Colors of variables: wff set class Syntax hints:   → wi 4 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7 This theorem is referenced by:  2a1d  23  a1i13  24  2a1i  27  syl5com  29  mpid  42  syld  45  imim2d  54  syl5d  68  syl6d  70  impbid21d  127  imbi2d  229  adantr  274  jctild  314  jctird  315  pm3.4  331  anbi2d  460  anbi1d  461  conax1k  644  mtod  653  pm2.76  798  dcim  827  condcOLD  840  pm5.18dc  869  pm2.54dc  877  pm2.85dc  891  dcor  920  anordc  941  xor3dc  1366  biassdc  1374  syl6ci  1422  hbequid  1494  19.30dc  1607  equsalh  1706  equvini  1733  nfsbxyt  1918  modc  2044  euan  2057  moexexdc  2085  nebidc  2390  rgen2a  2491  ralrimivw  2511  reximdv  2538  rexlimdvw  2558  r19.32r  2583  reuind  2895  rabxmdc  3401  rexn0  3468  exmidn0m  4135  regexmidlem1  4459  finds1  4527  nn0suc  4529  nndceq0  4543  ssrel2  4641  poltletr  4951  fmptco  5598  nnsucsssuc  6400  map1  6718  1domsn  6725  fopwdom  6742  mapxpen  6754  fidifsnen  6776  eldju2ndl  6974  eldju2ndr  6975  difinfsnlem  7001  finomni  7033  fodjuomnilemdc  7037  pr2ne  7077  exmidfodomrlemim  7086  indpi  7203  nnindnn  7754  nnind  8789  nn1m1nn  8791  nn1gt1  8807  nn0n0n1ge2b  9183  nn0le2is012  9186  xrltnsym  9638  xrlttr  9640  xrltso  9641  xltnegi  9677  xsubge0  9723  fzospliti  10013  elfzonlteqm1  10047  qbtwnxr  10095  modfzo0difsn  10228  monoord  10309  seq3coll  10646  rexuz3  10823  rexanuz2  10824  dvdsle  11614  dvdsabseq  11617  nno  11675  nn0seqcvgd  11794  lcmdvds  11832  divgcdcoprm0  11854  exprmfct  11890  rpexp1i  11904  phibndlem  11964  ennnfoneleminc  11996  epttop  12334  xblss2ps  12648  xblss2  12649  blfps  12653  blf  12654  metrest  12750  cncfmptc  12826  bj-nn0suc0  13364  exmidsbthrlem  13436
 Copyright terms: Public domain W3C validator