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 5. 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 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  42  syld  45  imim2d  54  syl5d  68  syl6d  70  impbid21d  127  imbi2d  229  adantr  272  jctild  312  jctird  313  pm3.4  329  anbi2d  455  anbi1d  456  pm2.51  622  mtod  630  pm2.76  763  condc  793  pm5.18dc  821  dcim  828  pm2.54dc  834  pm2.85dc  855  dcor  887  anordc  908  xor3dc  1333  biassdc  1341  syl6ci  1389  hbequid  1461  19.30dc  1574  equsalh  1672  equvini  1699  nfsbxyt  1879  modc  2003  euan  2016  moexexdc  2044  nebidc  2347  rgen2a  2445  ralrimivw  2465  reximdv  2492  rexlimdvw  2512  r19.32r  2536  reuind  2842  rabxmdc  3341  rexn0  3408  exmidn0m  4062  regexmidlem1  4386  finds1  4454  nn0suc  4456  nndceq0  4469  ssrel2  4567  poltletr  4875  fmptco  5518  nnsucsssuc  6318  map1  6636  1domsn  6642  fopwdom  6659  mapxpen  6671  fidifsnen  6693  eldju2ndl  6872  eldju2ndr  6873  difinfsnlem  6899  finomni  6924  fodjuomnilemdc  6928  pr2ne  6959  exmidfodomrlemim  6966  indpi  7051  nnindnn  7578  nnind  8594  nn1m1nn  8596  nn1gt1  8612  nn0n0n1ge2b  8982  nn0le2is012  8985  xrltnsym  9420  xrlttr  9422  xrltso  9423  xltnegi  9459  xsubge0  9505  fzospliti  9794  elfzonlteqm1  9828  qbtwnxr  9876  modfzo0difsn  10009  monoord  10090  seq3coll  10426  rexuz3  10602  rexanuz2  10603  dvdsle  11337  dvdsabseq  11340  nno  11398  nn0seqcvgd  11515  lcmdvds  11553  divgcdcoprm0  11575  exprmfct  11611  rpexp1i  11625  phibndlem  11684  ennnfoneleminc  11716  epttop  12041  xblss2ps  12332  xblss2  12333  blfps  12337  blf  12338  metrest  12434  cncfmptc  12495  bj-nn0suc0  12733  exmidsbthrlem  12801
  Copyright terms: Public domain W3C validator