Theorem a1d 18

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 435) 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 111 vs. pm2.43i 112 vs. pm2.43d 113). 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 3965 vs. uniexg 3966.

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 13	1 |- (ph -> (ch -> ps))

Syntax hints:   -> wi 3

This theorem is referenced by:  mpid 21  syl5com 24  syl5comOLD 25  imim2d 28  syld 31  syl5d 46  syl5dOLD 47  syl6d 49  pm2.21d 127  pm2.24d 180  pm2.51 195  pm2.521 196  pm2.52OLD 198  pm2.61niiOLD 208  pm2.61iii 209  impbid21d 249  imbi2d 380  adantr 543  adantldOLD 547  jaoi 549  jctild 603  jctird 604  pm3.4 627  adantllrOLD 843  adantlrlOLD 845  adantrllOLD 849  adantrrrOLD 855  pm2.75OLD 967  pm2.8OLD 970  orbidiOLD 1084  3ecase 1502  meredith 1503  meredithOLD 1504  ee121 1578  ee122 1579  ee21 1608  hbequid 1630  equsal 1821  dvelimfALT 1823  equvini 1840  equveli 1841  ax11 1894  hbsb4 1924  ax11v 1941  sbal1 2030  dvelimALT 2037  ax11eq 2047  ax11el 2048  ax11indalem 2052  ax11inda2ALT 2053  ax11inda2 2054  a12lem1 2060  mo 2082  euan 2118  moexex 2130  2mo 2139  rgen2a 2441  reximdv 2482  reuind 2727  hbsbc1gd 2781  hbsbcgd 2782  hbcsb1gd 2833  hbcsbgd 2834  rexn0 3203  dtru 3694  onfr 3882  ordsssuc2 3932  reusv1lem 3997  reusv6OLD 4009  reusv7OLD 4010  ordsucelsuc 4077  tfinds 4111  tfindsg 4112  limomss 4123  findsg 4145  finds1 4147  dmxp 4332  xpexr 4496  tz6.12-2 4824  ndmfv 4827  fveqres 4832  fvopabn 4874  eqfnfv 4892  elunirnALT 4980  ndmord 5115  soxp 5253  reiota2df 5283  smofvon2 5307  rdgsucopabn 5359  abianfplem 5377  oaordi 5431  oawordeulem 5439  odi 5461  omeulem1 5464  breng 5638  brdomg 5639  f1oen2g 5657  f1domg 5659  ac6sfi 5718  fodomr 5759  tskwe 5766  riotasvd 5802  riotasvdOLD 5803  infensuc 5837  onomeneq 5848  sucdom2 5854  fineqv 5874  pssnn 5878  fimax 5890  xpfi 5911  fisup2g 5952  supmaxlem 5953  suppr 5955  supsnALT 5957  onsdom 5969  inf3lemd 5994  infensucOLD 6025  en3lplem2 6041  r1ord 6052  rankr1c 6078  rankr1 6086  r1pw 6098  r1pwcl 6099  rankxplim3 6126  ra4sbc2 6131  scottex 6150  dif1cardOLD 6209  alephon 6219  alephcard 6221  alephnbtwn 6222  alephordi 6224  elomsubsd 6241  omsublim 6243  aceq5lem4 6257  onssnum 6272  alephfplem3 6295  domtriomlem 6365  domtriomlemOLD 6366  domtriomlemOLDOLD 6369  axdc3lem2 6377  axdc3lem4 6379  axcclem 6383  ondomon 6497  alephcardOLD 6508  alephnbtwnOLD 6509  alephordiOLD 6515  alephsucdomOLD 6518  alephval2 6521  cfpwsdom 6528  axextnd 6538  axrepnd 6541  axpownd 6548  axregnd 6551  addnidpi 6623  ltexprlem7 6743  prlem936 6750  supexpr 6758  mulgt0sr 6809  suppsr3 6819  xrltnsym 7011  xrlttri 7013  xrlttr 7014  negeui 7110  receui 7323  nnind 7555  nn1suc 7557  nnleltp1 7573  nnsubi 7575  lbinfm 7705  xrsupsslem 7737  xrinfmsslem 7738  xrub 7741  supxrre 7744  supxrpnf 7749  uzindOLD 7875  qbtwnxr 7918  ioojoin 8043  uzm1 8066  suprzcl 8111  fzaddel 8149  expge1 8335  exple1 8352  sqrlem6 8428  replim 8511  recan 8658  faclbnd4lem4 8704  bccl2 8724  clmi1i 8858  climaddlem3 8888  climmullem8 8899  climmulc2 8901  clim2serz 8906  climcmplem 8909  caucvg3lem 8938  caucvg3 8940  cvgcmp3cetlem1 8961  infcvglem3OLD 9000  expcnvlem6 9009  mulc1cncf 9057  ruclem24 9332  nn0seqcvgd 9469  eucalglt 9484  1nprm 9502  isprm3 9506  bastop1 9913  neif 10006  opnnei 10025  cnpco 10062  cncnplem4 10070  cnconst 10073  blrn 10134  bl2in 10136  blf 10137  metequiv 10174  tgioolem 10208  dscmet 10212  lmconst 10228  lmnn 10229  bcthlem21 10315  grprlidrid 10358  sm1cnilem 10707  ip2eqi 10881  fiv 11202  hmeobc 11232  fbssint 11275  fbunfip 11278  fbfgss 11284  filmapss 11305  fmf 11306  fmbas 11307  elfilmap 11308  cncomp 11327  isexid2 11368  on1el4 11409  hial2eq 11600  hlim0 11730  occon 11785  chocunii 11797  occllem7 11804  shsvs 11912  hsupss 11934  spanss 11943  idcnop 12532  cnlnssadj 12640  pjnmopi 12708  ssmd1 12872  ssmd2 12873  chrelat2i 12926  atexch 12942  mdsymlem4 12967  sumdmdlem 12979  bnj32 13353  bnj151 14172  bnj218 14179  bnj594 14229  bnj600 14237  bnj849 14247  pinq 14530  trpredlem1 14826  trpredss 14828  soxpOLD 14850  poseq 14854  findreccl 15201  twsymr 15365  prjcp1 15371  prjcp2 15372  unpde2eg22 15380  eqfnung2 15432  npincppr 15501  prl 15512  dupre1 15584  dutos1 15626  tostos 15637  fprod1ib 15686  fincmpzer 15707  multinvb 15786  zerdivemp1 15799  svli2 15840  svs3 15844  hmeogrp 15910  homcard 15911  top2usne 15916  homindlem3 15918  prtoptop 15945  efilcp 15949  efilcp2 15953  rcfpfillem6 15960  limvinlv 15968  conttnf 15971  cmptdst 15978  limptlimpr2lem1 15984  tpgprop1 16025  grphm 16035  dualalg 16186  dualcat2 16188  cmpassoh 16205  issubcat 16248  elincin 16291  cptarc 16313  intartar 16326  vtarsuelt 16343  a1i13 16411  a1i24 16414  onsdomOLD 16470  elomsubsdOLD 16479  omsublimOLD 16481  opnneiOLD 16502  compsublem 16515  hscptsscld 16519  compfipin0lem 16520  compfipin0 16521  alexsublem4 16525  alexsub 16526  connsub 16528  reconnlem5 16535  topbasfne 16584  finptfin 16592  locfincomp 16599  comppfsc 16602  neibastop1 16603  neibastop2lem1 16604  neibastop2lem2 16605  neibastop2lem3 16606  neibastop2lem4 16607  filssufillem 16655  cnpfillim 16674  rnelfm 16678  fmfnfm 16683  sfcls 16689  flimfnfcls 16700  fcluscnplem 16702  tailmap 16721  filnetlem1 16725  filnet 16730  fimaxOLD 16831  frinfm 16843  fisup2gOLD 16853  uzm1OLD 16869  sdclem2 16895  sdc 16896  fdc 16897  caushft 16936  sstotbnd 17021  totbndss 17022  heiborlem18 17057  heiborlem35 17074  bfp 17094  rrntotbnd 17107  zerdivemp1x 17193  smprngpr 17285  jca3 17318  prtlem80 17332  prtlem18 17364  vd12 17592  vd13 17593  ee221 17637  ee212 17639  ee112 17642  ee211 17645  ee210 17647  ee201 17649  ee120 17651  ee021 17653  ee012 17655  ee102 17657  ee03 17704  ee31 17715  ee31an 17717  ee123 17726  cvrexchlem 18079  ps-2 18139  paddasslem14 18537  lhpatleex2 18693  idldil 18748  isltrn2 18754  ltrneq2 18780  cdleme25a 19021  tendo0cl 19453

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

Copyright terms: Public domain