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 104) 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  128  imbi2d  230  adantr  276  jctild  316  jctird  317  pm3.4  333  anbi2d  464  anbi1d  465  conax1k  654  mtod  663  pm2.76  808  dcim  841  condcOLD  854  pm5.18dc  883  pm2.54dc  891  pm2.85dc  905  dcor  935  anordc  956  xor3dc  1387  biassdc  1395  syl6ci  1445  hbequid  1513  19.30dc  1627  equsalh  1726  equvini  1758  nfsbxyt  1943  modc  2069  euan  2082  moexexdc  2110  nebidc  2427  rgen2a  2531  ralrimivw  2551  reximdv  2578  rexlimdvw  2598  r19.32r  2623  reuind  2942  rabxmdc  3454  rexn0  3521  exmidn0m  4198  regexmidlem1  4529  finds1  4598  nn0suc  4600  nndceq0  4614  ssrel2  4713  poltletr  5025  fmptco  5678  nnsucsssuc  6487  map1  6806  1domsn  6813  fopwdom  6830  mapxpen  6842  fidifsnen  6864  eldju2ndl  7065  eldju2ndr  7066  difinfsnlem  7092  finomni  7132  fodjuomnilemdc  7136  pr2ne  7185  exmidfodomrlemim  7194  indpi  7329  nnindnn  7880  nnind  8921  nn1m1nn  8923  nn1gt1  8939  nn0n0n1ge2b  9318  nn0le2is012  9321  xrltnsym  9777  xrlttr  9779  xrltso  9780  xltnegi  9819  xsubge0  9865  fzospliti  10159  elfzonlteqm1  10193  qbtwnxr  10241  modfzo0difsn  10378  monoord  10459  seq3coll  10803  rexuz3  10980  rexanuz2  10981  fprodfac  11604  dvdsle  11830  dvdsabseq  11833  nno  11891  nn0seqcvgd  12021  lcmdvds  12059  divgcdcoprm0  12081  exprmfct  12118  rpexp1i  12134  phibndlem  12196  prm23lt5  12243  pc2dvds  12309  pcz  12311  pcadd  12319  pcmptcl  12320  oddprmdvds  12332  ennnfoneleminc  12392  dfgrp3me  12856  epttop  13250  xblss2ps  13564  xblss2  13565  blfps  13569  blf  13570  metrest  13666  cncfmptc  13742  zabsle1  14060  lgsne0  14099  2sqlem10  14121  bj-nn0suc0  14351  exmidsbthrlem  14419
  Copyright terms: Public domain W3C validator