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  655  mtod  664  pm2.76  809  dcim  842  condcOLD  855  pm5.18dc  884  pm2.54dc  892  pm2.85dc  906  dcor  937  anordc  958  xor3dc  1398  biassdc  1406  syl6ci  1456  hbequid  1524  19.30dc  1638  equsalh  1737  equvini  1769  nfsbxyt  1955  modc  2081  euan  2094  moexexdc  2122  nebidc  2440  rgen2a  2544  ralrimivw  2564  reximdv  2591  rexlimdvw  2611  r19.32r  2636  reuind  2957  rabxmdc  3469  rexn0  3536  exmidn0m  4219  regexmidlem1  4550  finds1  4619  nn0suc  4621  nndceq0  4635  ssrel2  4734  poltletr  5047  fmptco  5703  nnsucsssuc  6517  map1  6838  1domsn  6845  pw2f1odclem  6862  fopwdom  6864  mapxpen  6876  fidifsnen  6898  eldju2ndl  7101  eldju2ndr  7102  difinfsnlem  7128  finomni  7168  fodjuomnilemdc  7172  pr2ne  7221  exmidfodomrlemim  7230  indpi  7371  nnindnn  7922  nnind  8965  nn1m1nn  8967  nn1gt1  8983  nn0n0n1ge2b  9362  nn0le2is012  9365  xrltnsym  9823  xrlttr  9825  xrltso  9826  xltnegi  9865  xsubge0  9911  fzospliti  10206  elfzonlteqm1  10240  qbtwnxr  10288  modfzo0difsn  10426  monoord  10507  seq3coll  10854  rexuz3  11031  rexanuz2  11032  fprodfac  11655  dvdsaddre2b  11880  dvdsle  11882  dvdsabseq  11885  nno  11943  nn0seqcvgd  12073  lcmdvds  12111  divgcdcoprm0  12133  exprmfct  12170  rpexp1i  12186  phibndlem  12248  prm23lt5  12295  pc2dvds  12362  pcz  12364  pcadd  12372  pcmptcl  12374  oddprmdvds  12386  4sqlem11  12433  ennnfoneleminc  12462  dfgrp3me  13044  epttop  14050  xblss2ps  14364  xblss2  14365  blfps  14369  blf  14370  metrest  14466  cncfmptc  14542  zabsle1  14861  lgsne0  14900  2sqlem10  14933  bj-nn0suc0  15163  exmidsbthrlem  15232
  Copyright terms: Public domain W3C validator