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 232) 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. We usually show the theorem form without a suffix on its label (e.g. pm2.43 63 vs. pm2.43i 64 vs. pm2.43d 66). When an inference is converted to a theorem by eliminating an "is a set" hypothesis, we sometimes suffix the theorem form with "g" (for "more general") as in uniex 2926 vs. uniexg 2927.

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 81  pm2.51 107  pm2.52 108  pm2.24d 111  pm2.61iii 138  pm3.4 338  adantr 398  adantld 399  adantllr 406  adantlrl 407  adantrll 409  adantrrr 412  pm2.74 584  pm2.75 585  pm2.8 587  ibib 601  jctild 612  jctird 613  imbi2d 623  orbidi 755  prlem1 782  3ecase 935  dvelimfALT 1195  equvini 1210  ax11 1261  hbsb4 1290  ax11v 1307  sbal1 1388  dvelimALT 1395  ax11eq 1405  ax11el 1406  ax11indalem 1410  ax11inda2ALT 1411  ax11inda2 1412  a12lem1 1418  mo 1435  moexex 1481  2mo 1490  r19.22sdv 1785  r19.12 1787  hbsbc1gd 2033  hbsbcgd 2034  hbcsb1gd 2078  hbcsbgd 2079  rexn0 2408  dtruALT 2804  onfr 3043  trsuc 3112  ordsucelsuc 3130  limomss 3194  findsg 3214  finds1 3216  tfinds 3218  tfindsg 3219  dmxp 3389  xpexr 3536  tz6.12-2 3796  ndmfv 3802  fveqres 3806  fvopabn 3843  eqfnfv 3854  elunirnALT 3926  rdgsucopabn 4005  abianfplem 4019  ndmord 4108  oaordi 4238  oawordeulem 4246  odi 4268  breng 4436  brdomg 4437  f1oen2g 4455  f1domg 4457  fodomr 4546  onomeneq 4583  pssnn 4599  supmaxlem 4648  suppr 4650  supsnALT 4652  inf3lemd 4674  infensuc 4700  r1ord 4717  rankr1 4736  r1pw 4748  r1pwcl 4749  rankxplim3 4776  scottex 4778  aceq5lem4 4800  ondomon 4921  alephon 4930  alephcard 4932  alephnbtwn 4933  alephordi 4939  alephsucdom 4945  alephfplem3 4963  alephval2 4967  axextnd 5008  axrepnd 5011  axpownd 5018  axregnd 5021  addnidpi 5093  ltexprlem7 5213  prlem936 5220  supexpr 5228  mulgt0sr 5279  suppsr3 5289  negeui 5420  xrltnsym 5615  xrlttri 5617  xrlttr 5618  receui 5766  nnind 5997  nn1suc 5999  nnleltp1 6015  nnsubi 6017  lbinfm 6130  xrsupsslem 6158  xrinfmsslem 6159  xrub 6162  supxrre 6165  supxrpnf 6170  uzindOLD 6293  qbtwnxr 6332  ioojoin 6442  fzaddel 6526  expge1 6682  exple1 6696  sqrlem6 6768  replim 6851  recan 6995  faclbnd4lem4 7041  bccl2 7061  clmi1i 7176  climaddlem3 7206  climmullem8 7217  climmulc2 7219  clim2serz 7224  climcmplem 7227  caucvg3lem 7256  caucvg3 7258  cvgcmp3cetlem1 7278  infcvglem3 7313  expcnvlem6 7322  mulc1cncf 7369  ruclem24 7625  bastop1 7731  neif 7800  cnpco 7854  cncnplem4 7862  cnconst 7865  blrn 7926  bl2in 7928  blf 7929  tgioolem 7999  dscmet 8003  lmconst 8019  lmnn 8020  bcthlem21 8104  sm1cnilem 8431  ip2eqi 8601  hial2eq 9055  hlim0 9188  occon 9243  chocunii 9255  occllem7 9262  hsupss 9392  spanss 9401  idcnop 9988  cnlnssadj 10096  pjnmopi 10158  ssmd1 10322  ssmd2 10323  chrelat2i 10376  atexch 10392  mdsymlem4 10417  sumdmdlem 10429  findreccl 10504  fiv 10571  hmeogrp 10632  homcard 10633  hmeobc 10636  top2usne 10643  homindlem3 10645  efilcp 10664  efilcp2 10669  rcfpfillem6 10676  cmpassoh 10811

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

Copyright terms: Public domain