Theorem dedth 4483

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1543  ifcif 4425

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-if 4426

This theorem is referenced by:  dedth2h  4484  dedth3h  4485  orduninsuc  7600  oeoe  8305  limensuc  8801  axcc4dom  10020  inar1  10354  supsr  10691  renegcl  11106  peano5uzti  12232  uzenom  13502  seqfn  13551  seq1  13552  seqp1  13554  hashxp  13966  smadiadetr  21526  imsmet  28726  smcn  28733  nmlno0i  28829  nmblolbi  28835  blocn  28842  dipdir  28877  dipass  28880  siilem2  28887  htth  28953  normlem6  29150  normlem7tALT  29154  normsq  29169  hhssablo  29298  hhssnvt  29300  hhsssh  29304  shintcl  29365  chintcl  29367  pjhth  29428  ococ  29441  chm0  29526  chne0  29529  chocin  29530  chj0  29532  chjo  29550  h1de2ci  29591  spansn  29594  elspansn  29601  pjch1  29705  pjinormi  29722  pjige0  29726  hoaddid1  29826  hodid  29827  nmlnop0  30033  lnopunilem2  30046  elunop2  30048  lnophm  30054  nmbdoplb  30060  nmcopex  30064  nmcoplb  30065  lnopcon  30070  lnfn0  30082  lnfnmul  30083  nmbdfnlb  30085  nmcfnex  30088  nmcfnlb  30089  lnfncon  30091  riesz4  30099  riesz1  30100  cnlnadjeu  30113  pjhmop  30185  hmopidmch  30188  hmopidmpj  30189  pjss2coi  30199  pjssmi  30200  pjssge0i  30201  pjdifnormi  30202  pjidmco  30216  mdslmd1lem3  30362  mdslmd1lem4  30363  csmdsymi  30369  hatomic  30395  atord  30423  atcvat2  30424  chirred  30430  bnj941  32419  bnj944  32585  sqdivzi  33362  onsucconn  34313  onsucsuccmp  34319  limsucncmp  34321  dedths  36662  dedths2  36665  bnd2d  46001