ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  a1d Unicode 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  ph 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  |-  ( ph  ->  ps )
Assertion
Ref Expression
a1d  |-  ( ph  ->  ( ch  ->  ps ) )

Proof of Theorem a1d
StepHypRef Expression
1 a1d.1 . 2  |-  ( ph  ->  ps )
2 ax-1 6 . 2  |-  ( ps 
->  ( ch  ->  ps ) )
31, 2syl 14 1  |-  ( ph  ->  ( ch  ->  ps ) )
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  643  mtod  652  pm2.76  797  dcim  826  condcOLD  839  pm5.18dc  868  pm2.54dc  876  pm2.85dc  890  dcor  919  anordc  940  xor3dc  1365  biassdc  1373  syl6ci  1421  hbequid  1493  19.30dc  1606  equsalh  1704  equvini  1731  nfsbxyt  1916  modc  2042  euan  2055  moexexdc  2083  nebidc  2388  rgen2a  2486  ralrimivw  2506  reximdv  2533  rexlimdvw  2553  r19.32r  2578  reuind  2889  rabxmdc  3394  rexn0  3461  exmidn0m  4124  regexmidlem1  4448  finds1  4516  nn0suc  4518  nndceq0  4531  ssrel2  4629  poltletr  4939  fmptco  5586  nnsucsssuc  6388  map1  6706  1domsn  6713  fopwdom  6730  mapxpen  6742  fidifsnen  6764  eldju2ndl  6957  eldju2ndr  6958  difinfsnlem  6984  finomni  7012  fodjuomnilemdc  7016  pr2ne  7053  exmidfodomrlemim  7062  indpi  7162  nnindnn  7713  nnind  8748  nn1m1nn  8750  nn1gt1  8766  nn0n0n1ge2b  9142  nn0le2is012  9145  xrltnsym  9591  xrlttr  9593  xrltso  9594  xltnegi  9630  xsubge0  9676  fzospliti  9965  elfzonlteqm1  9999  qbtwnxr  10047  modfzo0difsn  10180  monoord  10261  seq3coll  10597  rexuz3  10774  rexanuz2  10775  dvdsle  11553  dvdsabseq  11556  nno  11614  nn0seqcvgd  11733  lcmdvds  11771  divgcdcoprm0  11793  exprmfct  11829  rpexp1i  11843  phibndlem  11903  ennnfoneleminc  11935  epttop  12273  xblss2ps  12587  xblss2  12588  blfps  12592  blf  12593  metrest  12689  cncfmptc  12765  bj-nn0suc0  13207  exmidsbthrlem  13278
  Copyright terms: Public domain W3C validator