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 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  |-  ( 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  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  936  anordc  957  xor3dc  1397  biassdc  1405  syl6ci  1455  hbequid  1523  19.30dc  1637  equsalh  1736  equvini  1768  nfsbxyt  1953  modc  2079  euan  2092  moexexdc  2120  nebidc  2437  rgen2a  2541  ralrimivw  2561  reximdv  2588  rexlimdvw  2608  r19.32r  2633  reuind  2954  rabxmdc  3466  rexn0  3533  exmidn0m  4213  regexmidlem1  4544  finds1  4613  nn0suc  4615  nndceq0  4629  ssrel2  4728  poltletr  5041  fmptco  5695  nnsucsssuc  6507  map1  6826  1domsn  6833  fopwdom  6850  mapxpen  6862  fidifsnen  6884  eldju2ndl  7085  eldju2ndr  7086  difinfsnlem  7112  finomni  7152  fodjuomnilemdc  7156  pr2ne  7205  exmidfodomrlemim  7214  indpi  7355  nnindnn  7906  nnind  8949  nn1m1nn  8951  nn1gt1  8967  nn0n0n1ge2b  9346  nn0le2is012  9349  xrltnsym  9807  xrlttr  9809  xrltso  9810  xltnegi  9849  xsubge0  9895  fzospliti  10190  elfzonlteqm1  10224  qbtwnxr  10272  modfzo0difsn  10409  monoord  10490  seq3coll  10836  rexuz3  11013  rexanuz2  11014  fprodfac  11637  dvdsaddre2b  11862  dvdsle  11864  dvdsabseq  11867  nno  11925  nn0seqcvgd  12055  lcmdvds  12093  divgcdcoprm0  12115  exprmfct  12152  rpexp1i  12168  phibndlem  12230  prm23lt5  12277  pc2dvds  12343  pcz  12345  pcadd  12353  pcmptcl  12354  oddprmdvds  12366  ennnfoneleminc  12426  dfgrp3me  12997  epttop  13886  xblss2ps  14200  xblss2  14201  blfps  14205  blf  14206  metrest  14302  cncfmptc  14378  zabsle1  14696  lgsne0  14735  2sqlem10  14768  bj-nn0suc0  14998  exmidsbthrlem  15067
  Copyright terms: Public domain W3C validator