Theorem dedth 2373

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 2380. If the inference has other hypotheses with class variable A, these can be kept by assigning keephyp 2386 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 2356	. . . 4 |- (ph -> if(ph, A, B) = A)
3	2	eqcomd 1472	. . 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 953  ifcif 2351

This theorem is referenced by:  dedth2h 2377  dedth3h 2378  orduninsuc 3104  rdgsuct 3930  rdglimt 3933  limensuc 4487  supsr 5203  negnegt 5365  subidt 5367  subid1t 5368  renegclt 5409  mul01t 5415  msqgt0t 5589  msqge0t 5590  gt0ne0t 5592  mulcant 5661  divmulz 5675  divclz 5680  divcan1z 5687  divcan2z 5688  recne0z 5694  recne0t 5695  recidt 5698  divrecz 5701  divdirz 5712  divcan3z 5716  div1t 5729  recrect 5732  redivcl 5754  redivclz 5755  eqnegt 5761  prodgt0 5775  ltmul1 5778  ltdiv1 5780  2timest 5951  halfpost 5983  nneot 6145  peano5uzt 6152  sq0t 6550  sqge0t 6564  discrlem2 6587  sqrlem6 6608  sqrlem12 6614  sqrlem20 6622  sqrlem21 6623  sqrlem22 6624  sqrth 6629  sqrcl 6630  sqrgt0 6631  sqrclt 6640  sqrgt0t 6641  sqrge0t 6642  sqr00t 6644  sqrsqt 6652  sqsqrt 6653  cjrebt 6735  cjmulrclt 6736  cjmulvalt 6737  cjmulge0t 6738  renegt 6739  imnegt 6742  cjcjt 6746  cjnegt 6749  addcjt 6750  absval2t 6787  abs00t 6788  absge0t 6789  absidt 6797  absgt0t 6831  abslem2 6846  clm4at 7028  clmi2at 7029  climconst3 7033  iserzshft2 7044  serzclim0 7046  climub 7090  caucvg3t 7104  cvgcmp3cetlem1 7124  cvgcmp3cetlem2 7125  cvgcmp3cet 7126  expcnvlem3 7164  geolim 7172  geolim1 7174  cvgratlem2ALT 7183  efseq1ex 7248  reefclt 7260  efcjt 7279  efaddlem24 7303  eftlext 7320  ef4pt 7341  efgt0t 7346  eflegeot 7356  efm1legeot 7358  reeff1olem2 7365  reeff1olem2OLD 7367  ruclem25 7477  ruclem29 7481  ruclem32 7484  ruclem33 7485  ruclem35 7487  ruclem37 7489  ruclem39 7491  methaus 7821  bcth 7966  imsmet 8262  nmcn 8274  nmlno0i 8386  nmblolbi 8391  blocn 8398  ipdir 8433  ipass 8436  siilem2 8443  ubthi 8475  efifolem1 8637  normlem6 8902  normlem7tALT 8906  normsqt 8922  hlimcaui 9027  hlimcau 9028  hhssnvt 9055  hhsssh 9059  occlt 9098  projlem1 9102  projlem16 9117  projlem17 9118  projlem28 9129  projlem29 9130  pjthlem8 9141  pjthlem9 9142  pjthlem14 9147  pjth 9148  pjtheut 9151  ococt 9163  shintclt 9209  chintclt 9211  chm0t 9329  chne0t 9332  chocint 9333  chj0t 9335  chjot 9353  h1de2ct 9395  spansnt 9398  elspansnt 9405  pjch1t 9532  pjinormt 9549  pjige0t 9553  hoaddid1t 9634  hodidt 9635  nmlnop0t 9838  lnopunilem2 9851  elunop2t 9853  lnophmt 9859  nmbdoplbt 9865  nmcopext 9874  nmcoplbt 9875  lnopcont 9879  lnfn0t 9891  lnfnmult 9892  nmbdfnlbt 9894  nmcfnext 9903  nmcfnlbt 9904  lnfncont 9906  riesz4t 9912  riesz1t 9913  cnlnadjeut 9926  pjhmopt 9988  hmopidmcht 9992  hmopidmpjt 9993  pjss2co 10003  pjssmt 10004  pjssge0t 10005  pjdifnormt 10006  pjidmcot 10019  mdslmd1lem3 10162  mdslmd1lem4 10163  csmdsym 10169  hatomict 10195  atordt 10223  atcvat2t 10224  irredt 10230  cayleythlem 10320  erdisj2 10343  moec 10357  ishomd 10562

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-if 2352

Copyright terms: Public domain