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 5393 vs. negneg 5390, especially when our "weak deduction theorem" dedth 2383 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 2870 vs. uniexg 2871.

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 389  adantld 390  adantllr 397  adantlrl 398  adantrll 400  adantrrr 403  pm2.74 573  pm2.75 574  pm2.8 576  ibib 590  jctild 601  jctird 602  imbi2d 612  orbidi 743  prlem1 770  3ecase 923  dvelimfALT 1153  equvini 1168  ax11 1219  hbsb4 1248  ax11v 1265  sbal1 1346  dvelimALT 1353  ax11eq 1363  ax11el 1364  ax11indalem 1368  ax11inda2ALT 1369  ax11inda2 1370  a12lem1 1376  mo 1393  moexex 1438  2mo 1447  r19.22sdv 1738  r19.12 1740  hbsbc1gd 1983  hbsbcgd 1984  hbcsb1gd 2027  hbcsbgd 2028  rexn0 2356  dtruALT 2748  onfr 2986  trsuc 3055  ordsucelsuc 3073  limomss 3137  findsg 3157  finds1 3159  tfinds 3161  tfindsg 3162  dmxp 3332  xpexr 3479  tz6.12-2 3739  ndmfv 3745  fveqres 3749  fvopabn 3786  eqfnfv 3797  elunirnALT 3869  rdgsucopabn 3947  abianfplem 3961  ndmord 4050  oaordi 4180  oawordeulem 4188  odi 4210  breng 4375  brdomg 4376  f1oen2g 4394  f1domg 4396  fodomr 4483  onomeneq 4519  pssnn 4534  supmaxlem 4588  suppr 4590  supsnALT 4592  inf3lemd 4612  infensuc 4638  r1ord 4655  rankr1 4674  r1pw 4686  r1pwcl 4687  rankxplim3 4714  scottex 4716  aceq5lem4 4738  ondomon 4856  alephon 4865  alephcard 4867  alephnbtwn 4868  alephordi 4874  alephsucdom 4880  alephfplem3 4898  alephval2 4902  axextnd 4943  axrepnd 4946  axpownd 4953  axregnd 4956  addnidpi 5028  ltexprlem7 5148  prlem936 5155  supexpr 5163  mulgt0sr 5214  suppsr3 5224  negeu 5355  xrltnsymt 5550  xrlttrit 5552  xrlttrt 5553  receu 5701  nnind 5937  nn1suc 5939  nnleltp1t 5954  nnsub 5956  lbinfm 6048  xrsupsslem 6076  xrinfmsslem 6077  xrub 6080  supxrre 6083  supxrpnf 6088  uzindOLD 6208  qbtwnxr 6279  ioojoint 6416  fzaddelt 6500  expge1t 6593  exple1t 6607  sqrlem6 6678  replimt 6761  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 7533  bastop 7642  neif 7715  cnpco 7769  cncnplem4 7777  cnconst 7780  blrn 7841  bl2in 7843  blf 7844  tgioolem 7914  dscmet 7918  lmconst 7934  lmnn 7935  bcthlem21 8019  sm1cnilem 8347  ip2eqi 8517  spwpr3OLD 8662  hial2eqt 8972  hlim0 9105  occont 9160  chocuni 9172  occllem7 9179  hsupss 9309  spanss 9318  idcnop 9905  cnlnssadj 10013  pjnmop 10075  ssmd1 10238  ssmd2 10239  chrelat2 10292  atexcht 10308  mdsymlem4 10333  sumdmdlem 10345  findreccl 10417  fiv 10482  fivOLD 10483  hmeogrp 10538  homcard 10539  hmeobc 10542  top2usne 10549  homindlem3 10551  efilcp 10572  efilcpOLD 10573  efilcp2 10581  efilcp2OLD 10582  rcfpfillem6 10595  rcfpfillem6OLD 10596  cmpassoh 10729

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

Copyright terms: Public domain