Theorem dedth 4514

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 4521. If the inference has other hypotheses with class variable 𝐴, these can be kept by assigning keephyp 4527 to them. For more information, see the Weak Deduction Theorem page mmdeduction.html 4527. (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 4462	. . . 4 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
3	2	eqcomd 2744	. . 3 ⊢ (𝜑 → 𝐴 = if(𝜑, 𝐴, 𝐵))
4		dedth.1	. . 3 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜒))
5	3, 4	syl 17	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
6	1, 5	mpbiri 257	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  ifcif 4456

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-if 4457

This theorem is referenced by:  dedth2h  4515  dedth3h  4516  orduninsuc  7665  oeoe  8392  limensuc  8890  axcc4dom  10128  inar1  10462  supsr  10799  renegcl  11214  peano5uzti  12340  uzenom  13612  seqfn  13661  seq1  13662  seqp1  13664  hashxp  14077  smadiadetr  21732  imsmet  28954  smcn  28961  nmlno0i  29057  nmblolbi  29063  blocn  29070  dipdir  29105  dipass  29108  siilem2  29115  htth  29181  normlem6  29378  normlem7tALT  29382  normsq  29397  hhssablo  29526  hhssnvt  29528  hhsssh  29532  shintcl  29593  chintcl  29595  pjhth  29656  ococ  29669  chm0  29754  chne0  29757  chocin  29758  chj0  29760  chjo  29778  h1de2ci  29819  spansn  29822  elspansn  29829  pjch1  29933  pjinormi  29950  pjige0  29954  hoaddid1  30054  hodid  30055  nmlnop0  30261  lnopunilem2  30274  elunop2  30276  lnophm  30282  nmbdoplb  30288  nmcopex  30292  nmcoplb  30293  lnopcon  30298  lnfn0  30310  lnfnmul  30311  nmbdfnlb  30313  nmcfnex  30316  nmcfnlb  30317  lnfncon  30319  riesz4  30327  riesz1  30328  cnlnadjeu  30341  pjhmop  30413  hmopidmch  30416  hmopidmpj  30417  pjss2coi  30427  pjssmi  30428  pjssge0i  30429  pjdifnormi  30430  pjidmco  30444  mdslmd1lem3  30590  mdslmd1lem4  30591  csmdsymi  30597  hatomic  30623  atord  30651  atcvat2  30652  chirred  30658  bnj941  32652  bnj944  32818  sqdivzi  33599  onsucconn  34554  onsucsuccmp  34560  limsucncmp  34562  dedths  36903  dedths2  36906  bnd2d  46273