Theorem a1d 12

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 (df-an 225) 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 8. Finally, a "theorem" would be the form with no hypotheses; in this case the "theorem" form would be the original axiom ax-1 4. In propositional calculus we usually prove the theorem form first without a suffix on its label (e.g. pm2.43 63 vs. pm2.43i 64 vs. pm2.43d 65), but (much) later we often suffix the theorem form's label with "t" as in negnegt 5405 vs. negneg 5402, especially when our "weak deduction theorem" dedth 2387 is used to prove the theorem form from its inference form. When an inference is converted to a theorem by eliminating an "is a set" hypothesis, we sometimes suffix the theorem form with "g" (for somewhat overstated "generalized") as in uniex 2876 vs. uniexg 2877.

Hypothesis

Ref	Expression
a1d.1	|- (ph -> ps)

Assertion

Ref	Expression
a1d	|- (ph -> (ch -> ps))

Proof of Theorem a1d

Step	Hyp	Ref	Expression
1		a1d.1	. 2 |- (ph -> ps)
2		ax-1 4	. 2 |- (ps -> (ch -> ps))
3	1, 2	syl 10	1 |- (ph -> (ch -> ps))

Syntax hints:   -> wi 3

This theorem is referenced by:  imim2d 25  mpid 47  syl5com 52  syl5d 55  syl6d 56  pm2.21d 78  pm2.51 101  pm2.52 102  pm2.24d 105  pm2.61iii 132  pm3.4 331  adantr 391  adantld 392  adantllr 399  adantlrl 400  adantrll 402  adantrrr 405  pm2.74 575  pm2.75 576  pm2.8 578  ibib 592  jctild 603  jctird 604  imbi2d 614  orbidi 745  prlem1 772  3ecase 925  dvelimfALT 1155  equvini 1170  ax11 1221  hbsb4 1250  ax11v 1267  sbal1 1348  dvelimALT 1355  ax11eq 1365  ax11el 1366  ax11indalem 1370  ax11inda2ALT 1371  ax11inda2 1372  a12lem1 1378  mo 1395  moexex 1441  2mo 1450  r19.22sdv 1741  r19.12 1743  hbsbc1gd 1986  hbsbcgd 1987  hbcsb1gd 2030  hbcsbgd 2031  rexn0 2360  dtruALT 2754  onfr 2992  trsuc 3061  ordsucelsuc 3079  limomss 3143  findsg 3163  finds1 3165  tfinds 3167  tfindsg 3168  dmxp 3338  xpexr 3485  tz6.12-2 3745  ndmfv 3751  fveqres 3755  fvopabn 3792  eqfnfv 3803  elunirnALT 3875  rdgsucopabn 3953  abianfplem 3967  ndmord 4056  oaordi 4186  oawordeulem 4194  odi 4216  breng 4381  brdomg 4382  f1oen2g 4400  f1domg 4402  fodomr 4489  onomeneq 4525  pssnn 4544  supmaxlem 4597  suppr 4599  supsnALT 4601  inf3lemd 4621  infensuc 4648  r1ord 4665  rankr1 4684  r1pw 4696  r1pwcl 4697  rankxplim3 4724  scottex 4726  aceq5lem4 4748  ondomon 4867  alephon 4876  alephcard 4878  alephnbtwn 4879  alephordi 4885  alephsucdom 4891  alephfplem3 4909  alephval2 4913  axextnd 4955  axrepnd 4958  axpownd 4965  axregnd 4968  addnidpi 5040  ltexprlem7 5160  prlem936 5167  supexpr 5175  mulgt0sr 5226  suppsr3 5236  negeu 5367  xrltnsymt 5562  xrlttrit 5564  xrlttrt 5565  receu 5713  nnind 5939  nn1suc 5941  nnleltp1t 5956  nnsub 5958  lbinfm 6050  xrsupsslem 6078  xrinfmsslem 6079  xrub 6082  supxrre 6085  supxrpnf 6090  uzindOLD 6210  qbtwnxr 6280  ioojoint 6417  fzaddelt 6501  expge1t 6594  exple1t 6608  sqrlem6 6679  replimt 6762  recant 6905  faclbnd4lem4 6951  bccl2t 6971  clmi1 7086  climaddlem3 7116  climmullem8 7127  climmulc2 7129  clim2serzt 7134  climcmplem 7137  caucvg3lem 7166  caucvg3t 7168  cvgcmp3cetlem1 7188  infcvglem3 7223  expcnvlem6 7232  mulc1cncf 7279  ruclem24 7534  bastop 7641  neif 7712  cnpco 7766  cncnplem4 7774  cnconst 7777  blrn 7838  bl2in 7840  blf 7841  tgioolem 7911  dscmet 7915  lmconst 7931  lmnn 7932  bcthlem21 8016  sm1cnilem 8343  ip2eqi 8513  hial2eqt 8967  hlim0 9100  occont 9155  chocuni 9167  occllem7 9174  hsupss 9304  spanss 9313  idcnop 9900  cnlnssadj 10008  pjnmop 10070  ssmd1 10233  ssmd2 10234  chrelat2 10287  atexcht 10303  mdsymlem4 10328  sumdmdlem 10340  findreccl 10412  fiv 10470  hmeogrp 10524  homcard 10525  hmeobc 10528  top2usne 10535  homindlem3 10537  efilcp 10556  efilcp2 10561  rcfpfillem6 10568  cmpassoh 10700

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7

Copyright terms: Public domain