Theorem dedth 1784

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 1790. If the inference has other hypotheses with class variable A, these can be kept by assigning keephyp 1794 to them. For more information, see the Deduction Theorem link on the Metamath Proof Explorer home page.

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 1780	. . . 4 |- (ph -> if(ph, A, B) = A)
3	2	cleqcomd 1106	. . 3 |- (ph -> A = if(ph, A, B))
4		dedth.1	. . 3 |- (A = if(ph, A, B) -> (ps <-> ch))
5	3, 4	syl 12	. 2 |- (ph -> (ps <-> ch))
6	1, 5	mpbiri 169	1 |- (ph -> ps)

Syntax hints:   -> wi 2   <-> wb 127   = wceq 1091  ifcif 1776

This theorem is referenced by:  dedth2h 1787  dedth3h 1788  orduninsuc 2365  rdgsuct 2983  rdglimt 2986  limensuc 3402  supsr 4025  negnegt 4157  subidt 4159  subid1t 4160  renegclt 4172  mulzer1t 4188  mulcant2 4209  divmulz 4219  divclz 4222  divcan1z 4226  divcan2z 4227  recneq0z 4232  recidt 4235  divrecz 4237  divdistrz 4245  divcan3z 4249  dividt 4256  div1t 4258  recrect 4260  redivcl 4274  redivclz 4275  gt0ne0t 4346  ltsqt 4376  recgt0 4386  prodgt0 4388  divgt0 4390  divge0 4392  ltmul1 4394  ltdiv 4399  recgt0t 4401  2timest 4490  halfpost 4508  sqege0t 4708  discrlem2 4714  nneo 4719  sqrlem6 4736  sqrlem12 4742  sqrlem20 4750  sqrlem21 4751  sqrlem22 4752  sqrth 4757  sqrcl 4758  sqrgt0 4759  sqrclt 4767  sqrgt0t 4768  sqrge0t 4769  sqr00t 4770  sqsqrt 4776  cjret 4829  cjcjt 4830  absclt 4848  absidt 4862  absgt0t 4863  abslem2 4867  ruclem25 4909  ruclem29 4913  ruclem32 4916  ruclem33 4917  ruclem35 4919  ruclem37 4921  ruclem39 4923  hiidrclt 5053  normlem6 5068  normlem7t 5072  hlimcaui 5141  hlimcau 5142  occlt 5189  projlem1 5193  projlem16 5208  projlem17 5209  projlem28 5220  projlem29 5221  pjthlem8 5232  pjthlem9 5233  pjthlem14 5238  pjth 5239  pjthut 5243  ococt 5253  pjoc2t 5274  shintclt 5295  chintclt 5297  chj0t 5414  chne0t 5452  h1de2ct 5461  spansnt 5464  elspansnt 5471  pjch1t 5560  pjss2co 5634  pjssmt 5635  pjssge0t 5636  pjdifnormt 5637  atcvat2t 5773

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-if 1777

metamath.org