Theorem dedth 4526

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-if 4468

This theorem is referenced by:  dedth2h  4527  dedth3h  4528  orduninsuc  7788  oeoe  8529  limensuc  9086  axcc4dom  10357  inar1  10692  supsr  11029  renegcl  11451  peano5uzti  12613  uzenom  13920  seqfn  13969  seq1  13970  seqp1  13972  hashxp  14390  smadiadetr  22653  imsmet  30780  smcn  30787  nmlno0i  30883  nmblolbi  30889  blocn  30896  dipdir  30931  dipass  30934  siilem2  30941  htth  31007  normlem6  31204  normlem7tALT  31208  normsq  31223  hhssablo  31352  hhssnvt  31354  hhsssh  31358  shintcl  31419  chintcl  31421  pjhth  31482  ococ  31495  chm0  31580  chne0  31583  chocin  31584  chj0  31586  chjo  31604  h1de2ci  31645  spansn  31648  elspansn  31655  pjch1  31759  pjinormi  31776  pjige0  31780  hoaddrid  31880  hodid  31881  nmlnop0  32087  lnopunilem2  32100  elunop2  32102  lnophm  32108  nmbdoplb  32114  nmcopex  32118  nmcoplb  32119  lnopcon  32124  lnfn0  32136  lnfnmul  32137  nmbdfnlb  32139  nmcfnex  32142  nmcfnlb  32143  lnfncon  32145  riesz4  32153  riesz1  32154  cnlnadjeu  32167  pjhmop  32239  hmopidmch  32242  hmopidmpj  32243  pjss2coi  32253  pjssmi  32254  pjssge0i  32255  pjdifnormi  32256  pjidmco  32270  mdslmd1lem3  32416  mdslmd1lem4  32417  csmdsymi  32423  hatomic  32449  atord  32477  atcvat2  32478  chirred  32484  bnj941  34934  bnj944  35099  sqdivzi  35929  onsucconn  36639  onsucsuccmp  36645  limsucncmp  36647  dedths  39425  dedths2  39428  bnd2d  50171