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 223) 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 65). 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 3093 vs. uniexg 3094.

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 100  pm2.52 101  pm2.24d 104  pm2.61iii 130  pm3.4 329  adantr 389  adantld 390  adantllr 397  adantlrl 398  adantrll 400  adantrrr 403  pm2.74 576  pm2.75 577  pm2.8 579  ibib 593  jctild 604  jctird 605  imbi2d 615  orbidi 748  prlem1 775  dn1 779  3ecase 930  dvelimfALT 1190  equvini 1205  ax11 1256  hbsb4 1286  ax11v 1303  sbal1 1385  dvelimALT 1392  ax11eq 1402  ax11el 1403  ax11indalem 1407  ax11inda2ALT 1408  ax11inda2 1409  a12lem1 1415  mo 1432  moexex 1478  2mo 1487  r19.22sdv 1784  r19.12 1786  hbsbc1gd 2031  hbsbcgd 2032  hbcsb1gd 2078  hbcsbgd 2079  rexn0 2410  dtru 2831  onfr 3014  trsuc 3056  ordsucelsuc 3178  tfinds 3212  tfindsg 3213  limomss 3224  findsg 3245  finds1 3247  dmxp 3419  xpexr 3564  tz6.12-2 3850  ndmfv 3856  fveqres 3860  fvopabn 3897  eqfnfv 3909  eqfnfv2 3911  elunirnALT 3983  ndmord 4111  rdgsucopabn 4248  abianfplem 4262  oaordi 4316  oawordeulem 4324  odi 4346  breng 4516  brdomg 4517  f1oen2g 4535  f1domg 4537  ac6sfi 4591  fodomr 4628  onomeneq 4665  pssnn 4681  supmaxlem 4731  suppr 4733  supsnALT 4735  inf3lemd 4757  infensuc 4784  r1ord 4801  rankr1 4820  r1pw 4832  r1pwcl 4833  rankxplim3 4860  scottex 4862  aceq5lem4 4884  ondomon 5006  alephon 5015  alephcard 5017  alephnbtwn 5018  alephordi 5024  alephsucdom 5030  alephfplem3 5048  alephval2 5052  axextnd 5097  axrepnd 5100  axpownd 5107  axregnd 5110  addnidpi 5182  ltexprlem7 5302  prlem936 5309  supexpr 5317  mulgt0sr 5368  suppsr3 5378  negeui 5509  xrltnsym 5704  xrlttri 5706  xrlttr 5707  receui 5853  nnind 6082  nn1suc 6084  nnleltp1 6100  nnsubi 6102  lbinfm 6216  xrsupsslem 6244  xrinfmsslem 6245  xrub 6248  supxrre 6251  supxrpnf 6256  uzindOLD 6379  qbtwnxr 6419  ioojoin 6543  fzaddel 6630  expge1 6787  exple1 6804  sqrlem6 6879  replim 6962  recan 7108  faclbnd4lem4 7154  bccl2 7174  clmi1i 7289  climaddlem3 7319  climmullem8 7330  climmulc2 7332  clim2serz 7337  climcmplem 7340  caucvg3lem 7369  caucvg3 7371  cvgcmp3cetlem1 7392  infcvglem3 7427  expcnvlem6 7436  mulc1cncf 7484  ruclem24 7745  bastop1 7854  neif 7925  cnpco 7979  cncnplem4 7987  cnconst 7990  blrn 8051  bl2in 8053  blf 8054  metequiv 8091  tgioolem 8125  dscmet 8129  lmconst 8145  lmnn 8146  bcthlem21 8230  grprlidrid 8270  sm1cnilem 8601  ip2eqi 8773  hial2eq 9248  hlim0 9381  occon 9436  chocunii 9448  occllem7 9455  hsupss 9585  spanss 9594  idcnop 10184  cnlnssadj 10292  pjnmopi 10355  ssmd1 10519  ssmd2 10520  chrelat2i 10573  atexch 10590  mdsymlem4 10615  sumdmdlem 10627  findreccl 10702  twsymr 10808  prj1 10809  prjcp1 10813  unpde2eg22 10826  fiv 10849  tostos 10883  isexid2 10901  multinvb 10960  on1el4 10963  hmeogrp 11044  homcard 11045  hmeobc 11048  top2usne 11051  homindlem3 11053  efilcp 11083  efilcp2 11087  rcfpfillem6 11094  cmpassoh 11256  issubcat 11299  a1i13 11333  a1i24 11336  onsdom 11437  elomsubsd 11446  omsublim 11448  opnnei 11469  compsublem 11487  hscptsscld 11491  compfipin0lem 11492  compfipin0 11493  cncomp 11494  alexsublem4 11499  alexsub 11500  connsub 11502  reconnlem5 11511  topbasfne 11560  finptfin 11568  locfincomp 11575  comppfsc 11578  neibastop1 11579  neibastop2lem1 11580  neibastop2lem2 11581  neibastop2lem3 11582  neibastop2lem4 11583  fbssint 11626  fbunfip 11631  fbfgss 11640  filssufillem 11655  cnpfillim 11686  elfilmap 11690  fmf 11693  fmbas 11694  filmapss 11696  rnelfm 11699  fmfnfm 11704  sfcls 11716  flimfnfcls 11727  fcluscnplem 11729  tailmap 11759  filnetlem1 11763  filnet 11768  dif1card 11835  fimax 11837  fixp 11840  frinfm 11850  uzm1 11862  sdclem2 11876  sdc 11877  caushft 11916  sstotbnd 11992  totbndss 11993  heiborlem18 12028  heiborlem35 12045  bfp 12065  rrntotbnd 12078

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

Copyright terms: Public domain