Theorem dedth 2383

Description: Weak deduction theorem that eliminates a hypothesis ph, making it become an antecedent. We assume that a proof exists for ph when the class variable A is replaced with a specific class B. The hypothesis ch should be assigned to the inference, and the inference's hypothesis eliminated with elimhyp 2390. If the inference has other hypotheses with class variable A, these can be kept by assigning keephyp 2396 to them. For more information, see the Deduction Theorem http://us.metamath.org/mpegif/mmdeduction.html.

Hypotheses

Ref	Expression
dedth.1	|- (A = if(ph, A, B) -> (ps <-> ch))
dedth.2	|- ch

Assertion

Ref	Expression
dedth	|- (ph -> ps)

Proof of Theorem dedth

Step	Hyp	Ref	Expression
1		dedth.2	. 2 |- ch
2		iftrue 2366	. . . 4 |- (ph -> if(ph, A, B) = A)
3	2	eqcomd 1480	. . 3 |- (ph -> A = if(ph, A, B))
4		dedth.1	. . 3 |- (A = if(ph, A, B) -> (ps <-> ch))
5	3, 4	syl 10	. 2 |- (ph -> (ps <-> ch))
6	1, 5	mpbiri 194	1 |- (ph -> ps)

Syntax hints:   -> wi 3   <-> wb 146   = wceq 956  ifcif 2361

This theorem is referenced by:  dedth2h 2387  dedth3h 2388  orduninsuc 3114  rdgsuct 3945  rdglimt 3948  limensuc 4507  supsr 5231  negnegt 5393  subidt 5395  subid1t 5396  renegclt 5437  mul01t 5443  msqgt0t 5615  msqge0t 5616  gt0ne0t 5618  mulcant 5690  mulcantOLD 5691  divmulz 5706  divclz 5711  divcan1z 5718  divcan2z 5719  recne0z 5731  recne0t 5732  recidt 5735  divrecz 5738  divdirz 5749  divcan3z 5754  div1t 5773  recrect 5776  redivcl 5798  redivclz 5799  eqnegt 5805  prodgt0 5819  ltmul1 5822  ltdiv1 5824  2timest 6004  halfpost 6036  nneot 6198  peano5uzt 6204  sqge0t 6633  discrlem2 6657  sqrlem6 6678  sqrlem12 6684  sqrlem20 6692  sqrlem21 6693  sqrlem22 6694  sqrth 6699  sqrcl 6700  sqrgt0 6701  sqrclt 6710  sqrgt0t 6711  sqrge0t 6712  sqr00t 6714  sqrsqt 6722  sqsqrt 6723  cjrebt 6800  cjmulrclt 6801  cjmulvalt 6802  cjmulge0t 6803  renegt 6804  imnegt 6807  cjcjt 6811  cjnegt 6814  addcjt 6815  absval2t 6852  abs00t 6853  absge0t 6854  absidt 6862  absgt0t 6893  abslem2 6909  clm4at 7090  clmi2at 7091  climconst3 7096  iserzshft2 7107  serzclim0 7109  climub 7154  caucvg3t 7168  cvgcmp3cetlem1 7188  cvgcmp3cetlem2 7189  cvgcmp3cet 7190  expcnvlem3 7229  geolim 7237  geolim1 7239  cvgratlem2ALT 7248  efseq1ex 7306  reefclt 7318  efcjt 7337  efaddlem24 7361  eftlext 7378  ef4pt 7400  efgt0t 7405  eflegeot 7416  efm1legeot 7418  reeff1olem2 7425  ruclem25 7534  ruclem29 7538  ruclem32 7541  ruclem33 7542  ruclem35 7544  ruclem37 7546  ruclem39 7548  methaus 7882  bcth 8032  imsmet 8324  nmcn 8339  nmlno0i 8454  nmblolbi 8460  blocn 8467  ipdir 8502  ipass 8505  siilem2 8512  ubthi 8544  efifolem1 8722  normlem6 8981  normlem7tALT 8985  normsqt 9001  hlimcaui 9106  hlimcau 9107  hhssablt 9133  hhssnvt 9135  hhsssh 9139  occlt 9182  projlem1 9186  projlem16 9201  projlem17 9202  projlem28 9213  projlem29 9214  pjthlem8 9226  pjthlem9 9227  pjthlem14 9232  pjth 9233  pjtheut 9236  ococt 9248  shintclt 9294  chintclt 9296  chm0t 9414  chne0t 9417  chocint 9418  chj0t 9420  chjot 9438  h1de2ct 9479  spansnt 9482  elspansnt 9489  pjch1t 9615  pjinormt 9632  pjige0t 9636  hoaddid1t 9717  hodidt 9718  hmopbdoptHIL 9913  nmlnop0t 9923  lnopunilem2 9936  elunop2t 9938  lnophmt 9944  nmbdoplbt 9950  nmcopext 9959  nmcoplbt 9960  lnopcont 9964  lnfn0t 9976  lnfnmult 9977  nmbdfnlbt 9979  nmcfnext 9988  nmcfnlbt 9989  lnfncont 9991  riesz4t 9997  riesz1t 9998  cnlnadjeut 10011  pjhmopt 10077  hmopidmcht 10081  hmopidmpjt 10082  pjss2co 10092  pjssmt 10093  pjssge0t 10094  pjdifnormt 10095  pjidmcot 10109  mdslmd1lem3 10254  mdslmd1lem4 10255  csmdsym 10261  hatomict 10287  atordt 10315  atcvat2t 10316  irredt 10322  cayleythlem 10413  erdisj2 10442  moec 10461  homindlem3 10551  limfillem2OLD 10608  ishomd 10718

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-if 2362

Copyright terms: Public domain