Theorem dedth 4589

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-if 4532

This theorem is referenced by:  dedth2h  4590  dedth3h  4591  orduninsuc  7864  oeoe  8636  limensuc  9193  axcc4dom  10479  inar1  10813  supsr  11150  renegcl  11570  peano5uzti  12706  uzenom  14002  seqfn  14051  seq1  14052  seqp1  14054  hashxp  14470  smadiadetr  22697  imsmet  30720  smcn  30727  nmlno0i  30823  nmblolbi  30829  blocn  30836  dipdir  30871  dipass  30874  siilem2  30881  htth  30947  normlem6  31144  normlem7tALT  31148  normsq  31163  hhssablo  31292  hhssnvt  31294  hhsssh  31298  shintcl  31359  chintcl  31361  pjhth  31422  ococ  31435  chm0  31520  chne0  31523  chocin  31524  chj0  31526  chjo  31544  h1de2ci  31585  spansn  31588  elspansn  31595  pjch1  31699  pjinormi  31716  pjige0  31720  hoaddrid  31820  hodid  31821  nmlnop0  32027  lnopunilem2  32040  elunop2  32042  lnophm  32048  nmbdoplb  32054  nmcopex  32058  nmcoplb  32059  lnopcon  32064  lnfn0  32076  lnfnmul  32077  nmbdfnlb  32079  nmcfnex  32082  nmcfnlb  32083  lnfncon  32085  riesz4  32093  riesz1  32094  cnlnadjeu  32107  pjhmop  32179  hmopidmch  32182  hmopidmpj  32183  pjss2coi  32193  pjssmi  32194  pjssge0i  32195  pjdifnormi  32196  pjidmco  32210  mdslmd1lem3  32356  mdslmd1lem4  32357  csmdsymi  32363  hatomic  32389  atord  32417  atcvat2  32418  chirred  32424  bnj941  34765  bnj944  34931  sqdivzi  35708  onsucconn  36421  onsucsuccmp  36427  limsucncmp  36429  dedths  38944  dedths2  38947  bnd2d  48912