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 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  459  anbi1d  460  conax1k  628  mtod  637  pm2.76  782  dcim  811  condcOLD  824  pm5.18dc  853  pm2.54dc  861  pm2.85dc  875  dcor  904  anordc  925  xor3dc  1350  biassdc  1358  syl6ci  1406  hbequid  1478  19.30dc  1591  equsalh  1689  equvini  1716  nfsbxyt  1896  modc  2020  euan  2033  moexexdc  2061  nebidc  2365  rgen2a  2463  ralrimivw  2483  reximdv  2510  rexlimdvw  2530  r19.32r  2555  reuind  2862  rabxmdc  3364  rexn0  3431  exmidn0m  4094  regexmidlem1  4418  finds1  4486  nn0suc  4488  nndceq0  4501  ssrel2  4599  poltletr  4909  fmptco  5554  nnsucsssuc  6356  map1  6674  1domsn  6681  fopwdom  6698  mapxpen  6710  fidifsnen  6732  eldju2ndl  6925  eldju2ndr  6926  difinfsnlem  6952  finomni  6980  fodjuomnilemdc  6984  pr2ne  7016  exmidfodomrlemim  7025  indpi  7118  nnindnn  7669  nnind  8704  nn1m1nn  8706  nn1gt1  8722  nn0n0n1ge2b  9098  nn0le2is012  9101  xrltnsym  9547  xrlttr  9549  xrltso  9550  xltnegi  9586  xsubge0  9632  fzospliti  9921  elfzonlteqm1  9955  qbtwnxr  10003  modfzo0difsn  10136  monoord  10217  seq3coll  10553  rexuz3  10730  rexanuz2  10731  dvdsle  11469  dvdsabseq  11472  nno  11530  nn0seqcvgd  11649  lcmdvds  11687  divgcdcoprm0  11709  exprmfct  11745  rpexp1i  11759  phibndlem  11819  ennnfoneleminc  11851  epttop  12186  xblss2ps  12500  xblss2  12501  blfps  12505  blf  12506  metrest  12602  cncfmptc  12678  bj-nn0suc0  13075  exmidsbthrlem  13144
  Copyright terms: Public domain W3C validator