Theorem dedth 4525

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-if 4467

This theorem is referenced by:  dedth2h  4526  dedth3h  4527  orduninsuc  7794  oeoe  8535  limensuc  9092  axcc4dom  10363  inar1  10698  supsr  11035  renegcl  11457  peano5uzti  12619  uzenom  13926  seqfn  13975  seq1  13976  seqp1  13978  hashxp  14396  smadiadetr  22640  imsmet  30762  smcn  30769  nmlno0i  30865  nmblolbi  30871  blocn  30878  dipdir  30913  dipass  30916  siilem2  30923  htth  30989  normlem6  31186  normlem7tALT  31190  normsq  31205  hhssablo  31334  hhssnvt  31336  hhsssh  31340  shintcl  31401  chintcl  31403  pjhth  31464  ococ  31477  chm0  31562  chne0  31565  chocin  31566  chj0  31568  chjo  31586  h1de2ci  31627  spansn  31630  elspansn  31637  pjch1  31741  pjinormi  31758  pjige0  31762  hoaddrid  31862  hodid  31863  nmlnop0  32069  lnopunilem2  32082  elunop2  32084  lnophm  32090  nmbdoplb  32096  nmcopex  32100  nmcoplb  32101  lnopcon  32106  lnfn0  32118  lnfnmul  32119  nmbdfnlb  32121  nmcfnex  32124  nmcfnlb  32125  lnfncon  32127  riesz4  32135  riesz1  32136  cnlnadjeu  32149  pjhmop  32221  hmopidmch  32224  hmopidmpj  32225  pjss2coi  32235  pjssmi  32236  pjssge0i  32237  pjdifnormi  32238  pjidmco  32252  mdslmd1lem3  32398  mdslmd1lem4  32399  csmdsymi  32405  hatomic  32431  atord  32459  atcvat2  32460  chirred  32466  bnj941  34915  bnj944  35080  sqdivzi  35910  onsucconn  36620  onsucsuccmp  36626  limsucncmp  36628  dedths  39408  dedths2  39411  bnd2d  50156