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 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 (𝜑𝜓)
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  127  imbi2d  229  adantr  272  jctild  312  jctird  313  pm3.4  329  anbi2d  457  anbi1d  458  conax1k  626  mtod  635  pm2.76  780  dcim  809  condcOLD  822  pm5.18dc  851  pm2.54dc  859  pm2.85dc  873  dcor  902  anordc  923  xor3dc  1348  biassdc  1356  syl6ci  1404  hbequid  1476  19.30dc  1589  equsalh  1687  equvini  1714  nfsbxyt  1894  modc  2018  euan  2031  moexexdc  2059  nebidc  2363  rgen2a  2461  ralrimivw  2481  reximdv  2508  rexlimdvw  2528  r19.32r  2553  reuind  2860  rabxmdc  3362  rexn0  3429  exmidn0m  4092  regexmidlem1  4416  finds1  4484  nn0suc  4486  nndceq0  4499  ssrel2  4597  poltletr  4907  fmptco  5552  nnsucsssuc  6354  map1  6672  1domsn  6679  fopwdom  6696  mapxpen  6708  fidifsnen  6730  eldju2ndl  6923  eldju2ndr  6924  difinfsnlem  6950  finomni  6978  fodjuomnilemdc  6982  pr2ne  7014  exmidfodomrlemim  7021  indpi  7114  nnindnn  7665  nnind  8696  nn1m1nn  8698  nn1gt1  8714  nn0n0n1ge2b  9084  nn0le2is012  9087  xrltnsym  9530  xrlttr  9532  xrltso  9533  xltnegi  9569  xsubge0  9615  fzospliti  9904  elfzonlteqm1  9938  qbtwnxr  9986  modfzo0difsn  10119  monoord  10200  seq3coll  10536  rexuz3  10713  rexanuz2  10714  dvdsle  11449  dvdsabseq  11452  nno  11510  nn0seqcvgd  11629  lcmdvds  11667  divgcdcoprm0  11689  exprmfct  11725  rpexp1i  11739  phibndlem  11798  ennnfoneleminc  11830  epttop  12165  xblss2ps  12479  xblss2  12480  blfps  12484  blf  12485  metrest  12581  cncfmptc  12657  bj-nn0suc0  12982  exmidsbthrlem  13051
  Copyright terms: Public domain W3C validator