Theorem dedth 4559

Description: Weak deduction theorem that eliminates a hypothesis 𝜑, making it become an antecedent. We assume that a proof exists for 𝜑 when the class variable 𝐴 is replaced with a specific class 𝐵. The hypothesis 𝜒 should be assigned to the inference, and the inference hypothesis eliminated with elimhyp 4566. If the inference has other hypotheses with class variable 𝐴, these can be kept by assigning keephyp 4572 to them. For more information, see the Weak Deduction Theorem page mmdeduction.html 4572. (Contributed by NM, 15-May-1999.)

Hypotheses

Ref	Expression
dedth.1	⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜒))
dedth.2	⊢ 𝜒

Assertion

Ref	Expression
dedth	⊢ (𝜑 → 𝜓)

Proof of Theorem dedth

Step	Hyp	Ref	Expression
1		dedth.2	. 2 ⊢ 𝜒
2		iftrue 4506	. . . 4 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
3	2	eqcomd 2741	. . 3 ⊢ (𝜑 → 𝐴 = if(𝜑, 𝐴, 𝐵))
4		dedth.1	. . 3 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜒))
5	3, 4	syl 17	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
6	1, 5	mpbiri 258	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ifcif 4500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-if 4501

This theorem is referenced by:  dedth2h  4560  dedth3h  4561  orduninsuc  7836  oeoe  8609  limensuc  9166  axcc4dom  10453  inar1  10787  supsr  11124  renegcl  11544  peano5uzti  12681  uzenom  13980  seqfn  14029  seq1  14030  seqp1  14032  hashxp  14450  smadiadetr  22611  imsmet  30618  smcn  30625  nmlno0i  30721  nmblolbi  30727  blocn  30734  dipdir  30769  dipass  30772  siilem2  30779  htth  30845  normlem6  31042  normlem7tALT  31046  normsq  31061  hhssablo  31190  hhssnvt  31192  hhsssh  31196  shintcl  31257  chintcl  31259  pjhth  31320  ococ  31333  chm0  31418  chne0  31421  chocin  31422  chj0  31424  chjo  31442  h1de2ci  31483  spansn  31486  elspansn  31493  pjch1  31597  pjinormi  31614  pjige0  31618  hoaddrid  31718  hodid  31719  nmlnop0  31925  lnopunilem2  31938  elunop2  31940  lnophm  31946  nmbdoplb  31952  nmcopex  31956  nmcoplb  31957  lnopcon  31962  lnfn0  31974  lnfnmul  31975  nmbdfnlb  31977  nmcfnex  31980  nmcfnlb  31981  lnfncon  31983  riesz4  31991  riesz1  31992  cnlnadjeu  32005  pjhmop  32077  hmopidmch  32080  hmopidmpj  32081  pjss2coi  32091  pjssmi  32092  pjssge0i  32093  pjdifnormi  32094  pjidmco  32108  mdslmd1lem3  32254  mdslmd1lem4  32255  csmdsymi  32261  hatomic  32287  atord  32315  atcvat2  32316  chirred  32322  bnj941  34749  bnj944  34915  sqdivzi  35691  onsucconn  36402  onsucsuccmp  36408  limsucncmp  36410  dedths  38926  dedths2  38929  bnd2d  49493