Theorem dedth 4550

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 4557. If the inference has other hypotheses with class variable 𝐴, these can be kept by assigning keephyp 4563 to them. For more information, see the Weak Deduction Theorem page mmdeduction.html 4563. (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 4497	. . . 4 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
3	2	eqcomd 2736	. . 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 4491

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-if 4492

This theorem is referenced by:  dedth2h  4551  dedth3h  4552  orduninsuc  7822  oeoe  8566  limensuc  9124  axcc4dom  10401  inar1  10735  supsr  11072  renegcl  11492  peano5uzti  12631  uzenom  13936  seqfn  13985  seq1  13986  seqp1  13988  hashxp  14406  smadiadetr  22569  imsmet  30627  smcn  30634  nmlno0i  30730  nmblolbi  30736  blocn  30743  dipdir  30778  dipass  30781  siilem2  30788  htth  30854  normlem6  31051  normlem7tALT  31055  normsq  31070  hhssablo  31199  hhssnvt  31201  hhsssh  31205  shintcl  31266  chintcl  31268  pjhth  31329  ococ  31342  chm0  31427  chne0  31430  chocin  31431  chj0  31433  chjo  31451  h1de2ci  31492  spansn  31495  elspansn  31502  pjch1  31606  pjinormi  31623  pjige0  31627  hoaddrid  31727  hodid  31728  nmlnop0  31934  lnopunilem2  31947  elunop2  31949  lnophm  31955  nmbdoplb  31961  nmcopex  31965  nmcoplb  31966  lnopcon  31971  lnfn0  31983  lnfnmul  31984  nmbdfnlb  31986  nmcfnex  31989  nmcfnlb  31990  lnfncon  31992  riesz4  32000  riesz1  32001  cnlnadjeu  32014  pjhmop  32086  hmopidmch  32089  hmopidmpj  32090  pjss2coi  32100  pjssmi  32101  pjssge0i  32102  pjdifnormi  32103  pjidmco  32117  mdslmd1lem3  32263  mdslmd1lem4  32264  csmdsymi  32270  hatomic  32296  atord  32324  atcvat2  32325  chirred  32331  bnj941  34769  bnj944  34935  sqdivzi  35722  onsucconn  36433  onsucsuccmp  36439  limsucncmp  36441  dedths  38962  dedths2  38965  bnd2d  49674