Theorem a1d 15

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 242) 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 77 vs. pm2.43i 78 vs. pm2.43d 79). 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 3794 vs. uniexg 3795.

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

Syntax hints:   -> wi 3

This theorem is referenced by:  imim2d 28  mpid 58  syl5com 63  syl5d 66  syl6d 67  pm2.21d 94  pm2.51 116  pm2.52 117  pm2.24d 120  pm2.61nii 145  pm2.61iii 147  pm3.4 358  adantr 425  adantld 426  adantllr 433  adantlrl 434  adantrll 436  adantrrr 439  pm2.74OLD 633  pm2.75 634  pm2.8 636  ibib 650  jctild 662  jctird 663  imbi2d 674  orbidi 815  prlem1OLD 849  dn1OLD 856  3ecase 1199  meredith 1200  ee12an 1273  ee121 1277  ee122 1278  hbequid 1313  equsal 1511  dvelimfALT 1514  equvini 1531  equviniOLD 1532  ax11 1589  hbsb4 1620  ax11v 1642  sbal1 1737  dvelimALT 1744  ax11eq 1754  ax11el 1755  ax11indalem 1759  ax11inda2ALT 1760  ax11inda2 1761  a12lem1 1767  mo 1787  euan 1827  moexex 1841  2mo 1851  rgen2a 2160  reximdv 2202  r19.12OLD 2205  reuind 2450  hbsbc1gd 2515  hbsbc1gdOLD 2516  hbsbcgd 2517  hbsbcgdOLD 2518  hbcsb1gd 2570  hbcsbgd 2571  rexn0 2972  dtru 3498  onfr 3702  trsucOLD 3753  ordsssuc2 3758  eufromeq5 3832  eufromeq6 3833  ordsucelsuc 3902  ordsucelsucOLD 3903  tfinds 3942  tfindsOLD 3943  tfindsg 3944  limomss 3956  findsg 3980  finds1 3982  dmxp 4177  dmxpOLD 4178  xpexr 4352  tz6.12-2 4696  ndmfv 4702  fveqres 4708  fvopabn 4749  eqfnfv 4766  elunirnALT 4845  ndmord 4983  rdgsucopabn 5155  abianfplem 5170  oaordi 5227  oawordeulem 5236  odi 5258  breng 5434  brdomg 5435  f1oen2g 5453  f1domg 5455  ac6sfi 5509  fodomr 5547  onomeneq 5612  pssnn 5628  supmaxlem 5678  suppr 5680  supsnALT 5682  onsdom 5694  inf3lemd 5718  infensuc 5745  en3lplem2 5757  r1ord 5766  rankr1 5785  r1pw 5797  r1pwcl 5798  rankxplim3 5825  ra4sbc2 5829  ee21 5840  scottex 5846  alephon 5876  elomsubsd 5885  omsublim 5887  aceq5lem4 5900  ondomon 6008  alephcard 6015  alephnbtwn 6016  alephordi 6022  alephsucdom 6028  alephfplem3 6046  alephval2 6050  axextnd 6095  axrepnd 6098  axpownd 6105  axregnd 6108  addnidpi 6180  ltexprlem7 6300  prlem936 6307  supexpr 6315  mulgt0sr 6366  suppsr3 6376  negeui 6510  xrltnsym 6725  xrlttri 6727  xrlttr 6728  receui 6890  nnind 7120  nn1suc 7122  nnleltp1 7138  nnsubi 7140  lbinfm 7257  xrsupsslem 7285  xrinfmsslem 7286  xrub 7289  supxrre 7292  supxrpnf 7297  uzindOLD 7420  qbtwnxr 7460  ioojoin 7585  fzaddel 7672  expge1 7835  exple1 7852  sqrlem6 7928  replim 8011  recan 8157  faclbnd4lem4 8203  bccl2 8223  clmi1i 8346  climaddlem3 8376  climmullem8 8387  climmulc2 8389  clim2serz 8394  climcmplem 8397  caucvg3lem 8426  caucvg3 8428  cvgcmp3cetlem1 8449  infcvglem3 8484  expcnvlem6 8493  mulc1cncf 8541  ruclem24 8802  bastop1 8912  neif 8991  cnpco 9046  cncnplem4 9054  cnconst 9057  blrn 9118  bl2in 9120  blf 9121  metequiv 9158  tgioolem 9192  dscmet 9196  lmconst 9212  lmnn 9213  bcthlem21 9297  grprlidrid 9337  sm1cnilem 9686  ip2eqi 9858  dif1card 10177  fixp 10180  fiv 10212  hmeobc 10239  fbssint 10279  fbunfip 10282  fbfgss 10288  filmapss 10309  fmf 10310  fmbas 10311  elfilmap 10312  cncomp 10331  isexid2 10372  on1el4 10413  hial2eq 10605  hlim0 10738  occon 10793  chocunii 10805  occllem7 10812  hsupss 10942  spanss 10951  idcnop 11542  cnlnssadj 11650  pjnmopi 11719  ssmd1 11883  ssmd2 11884  chrelat2i 11937  atexch 11953  mdsymlem4 11978  sumdmdlem 11990  bnj32 12398  bnj151 13243  bnj218 13250  bnj594 13300  bnj600 13308  bnj849 13318  suprzcl 13658  nn0seqcvgd 13659  eucalglt 13753  1nprm 13769  isprm3 13776  trcllem1 13933  soxp 13950  poseq 13954  findreccl 14254  twsymr 14394  prj1 14395  prjcp1 14399  unpde2eg22 14407  eqfnung2 14459  npincppr 14501  prl 14512  dupre1 14584  dutos1 14626  tostos 14637  fprod1ib 14686  fincmpzer 14711  multinvb 14772  zerdivemp1 14785  svli2 14826  svs3 14830  hmeogrp 14892  homcard 14893  top2usne 14898  homindlem3 14900  prtoptop 14919  efilcp 14922  efilcp2 14926  rcfpfillem6 14933  limvinlv 14941  conttnf 14944  tpgprop1 14986  dualalg 15131  dualcat2 15133  cmpassoh 15150  issubcat 15193  elincin 15220  cptarc 15242  intartar 15255  vtarsuelt 15272  a1i13 15326  a1i24 15329  onsdomOLD 15385  elomsubsdOLD 15394  omsublimOLD 15396  opnnei 15417  compsublem 15430  hscptsscld 15434  compfipin0lem 15435  compfipin0 15436  alexsublem4 15440  alexsub 15441  connsub 15443  reconnlem5 15450  topbasfne 15499  finptfin 15507  locfincomp 15514  comppfsc 15517  neibastop1 15518  neibastop2lem1 15519  neibastop2lem2 15520  neibastop2lem3 15521  neibastop2lem4 15522  filssufillem 15570  cnpfillim 15589  rnelfm 15593  fmfnfm 15598  sfcls 15604  flimfnfcls 15615  fcluscnplem 15617  tailmap 15636  filnetlem1 15640  filnet 15645  fimax 15746  frinfm 15758  fisup2g 15768  uzm1 15784  sdclem2 15810  sdc 15811  fdc 15812  caushft 15851  sstotbnd 15936  totbndss 15937  heiborlem18 15972  heiborlem35 15989  bfp 16009  rrntotbnd 16022  zerdivemp1x 16108  smprngpr 16200  jca3 16233  prtlem80 16247  prtlem18 16279  vd12 16501  vd13 16502  ee221 16540  ee212 16542  ee112 16545  ee211 16548  ee210 16550  ee201 16552  ee120 16554  ee021 16556  ee012 16558  ee102 16560  ee03 16609  ee31 16620  ee31an 16622  ee123 16631  cvrexchlem 17059  ps2 17079  paddasslem14 17294

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

Copyright terms: Public domain