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 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 vs. pm2.43i 48 vs. pm2.43d 49). (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 5 . 2 (𝜓 → (𝜒𝜓))
31, 2syl 14 1 (𝜑 → (𝜒𝜓))
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  614  mtod  622  pm2.76  755  condc  785  pm5.18dc  813  dcim  820  pm2.54dc  826  pm2.85dc  847  dcor  879  anordc  900  xor3dc  1321  biassdc  1329  syl6ci  1377  hbequid  1449  19.30dc  1561  equsalh  1658  equvini  1685  nfsbxyt  1864  modc  1988  euan  2001  moexexdc  2029  nebidc  2331  rgen2a  2425  ralrimivw  2443  reximdv  2470  rexlimdvw  2488  r19.32r  2510  reuind  2809  rabxmdc  3303  rexn0  3367  regexmidlem1  4322  finds1  4390  nn0suc  4392  nndceq0  4404  ssrel2  4496  poltletr  4799  fmptco  5427  nnsucsssuc  6207  map1  6481  1domsn  6487  fopwdom  6504  mapxpen  6516  fidifsnen  6538  eldju2ndl  6707  eldju2ndr  6708  finomni  6740  fodjuomnilemdc  6743  pr2ne  6764  exmidfodomrlemim  6771  indpi  6845  nnindnn  7372  nnind  8373  nn1m1nn  8375  nn1gt1  8390  nn0n0n1ge2b  8759  xrltnsym  9195  xrlttr  9197  xrltso  9198  xltnegi  9229  fzospliti  9515  elfzonlteqm1  9549  qbtwnxr  9597  modfzo0difsn  9730  monoord  9810  iseqcoll  10144  rexuz3  10319  rexanuz2  10320  dvdsle  10727  dvdsabseq  10730  nno  10788  nn0seqcvgd  10905  lcmdvds  10943  divgcdcoprm0  10965  exprmfct  11001  rpexp1i  11015  phibndlem  11074  bj-nn0suc0  11290  exmidsbthrlem  11357
  Copyright terms: Public domain W3C validator