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 102) 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 5. We usually show the theorem form without a suffix on its label (e.g. pm2.43 52 versus pm2.43i 48 versus pm2.43d 49). (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 5 . 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-1 5  ax-2 6  ax-mp 7
This theorem is referenced by:  2a1d  23  a1i13  24  2a1i  27  syl5com  29  mpid  41  syld  44  imim2d  53  syl5d  67  syl6d  69  impbid21d  126  imbi2d  228  adantr  270  jctild  309  jctird  310  pm3.4  326  anbi2d  452  anbi1d  453  pm2.51  616  mtod  624  pm2.76  757  condc  787  pm5.18dc  815  dcim  822  pm2.54dc  828  pm2.85dc  849  dcor  881  anordc  902  xor3dc  1323  biassdc  1331  syl6ci  1379  hbequid  1451  19.30dc  1563  equsalh  1661  equvini  1688  nfsbxyt  1867  modc  1991  euan  2004  moexexdc  2032  nebidc  2335  rgen2a  2429  ralrimivw  2447  reximdv  2474  rexlimdvw  2492  r19.32r  2514  reuind  2818  rabxmdc  3312  rexn0  3376  regexmidlem1  4339  finds1  4407  nn0suc  4409  nndceq0  4421  ssrel2  4516  poltletr  4819  fmptco  5448  nnsucsssuc  6235  map1  6509  1domsn  6515  fopwdom  6532  mapxpen  6544  fidifsnen  6566  eldju2ndl  6742  eldju2ndr  6743  finomni  6775  fodjuomnilemdc  6778  pr2ne  6799  exmidfodomrlemim  6806  indpi  6880  nnindnn  7407  nnind  8410  nn1m1nn  8412  nn1gt1  8427  nn0n0n1ge2b  8796  xrltnsym  9232  xrlttr  9234  xrltso  9235  xltnegi  9266  fzospliti  9552  elfzonlteqm1  9586  qbtwnxr  9634  modfzo0difsn  9767  monoord  9869  iseqcoll  10211  rexuz3  10387  rexanuz2  10388  dvdsle  10925  dvdsabseq  10928  nno  10986  nn0seqcvgd  11103  lcmdvds  11141  divgcdcoprm0  11163  exprmfct  11199  rpexp1i  11213  phibndlem  11272  bj-nn0suc0  11489  exmidsbthrlem  11556
  Copyright terms: Public domain W3C validator