Theorem dedth 4547

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-if 4489

This theorem is referenced by:  dedth2h  4548  dedth3h  4549  orduninsuc  7819  oeoe  8563  limensuc  9118  axcc4dom  10394  inar1  10728  supsr  11065  renegcl  11485  peano5uzti  12624  uzenom  13929  seqfn  13978  seq1  13979  seqp1  13981  hashxp  14399  smadiadetr  22562  imsmet  30620  smcn  30627  nmlno0i  30723  nmblolbi  30729  blocn  30736  dipdir  30771  dipass  30774  siilem2  30781  htth  30847  normlem6  31044  normlem7tALT  31048  normsq  31063  hhssablo  31192  hhssnvt  31194  hhsssh  31198  shintcl  31259  chintcl  31261  pjhth  31322  ococ  31335  chm0  31420  chne0  31423  chocin  31424  chj0  31426  chjo  31444  h1de2ci  31485  spansn  31488  elspansn  31495  pjch1  31599  pjinormi  31616  pjige0  31620  hoaddrid  31720  hodid  31721  nmlnop0  31927  lnopunilem2  31940  elunop2  31942  lnophm  31948  nmbdoplb  31954  nmcopex  31958  nmcoplb  31959  lnopcon  31964  lnfn0  31976  lnfnmul  31977  nmbdfnlb  31979  nmcfnex  31982  nmcfnlb  31983  lnfncon  31985  riesz4  31993  riesz1  31994  cnlnadjeu  32007  pjhmop  32079  hmopidmch  32082  hmopidmpj  32083  pjss2coi  32093  pjssmi  32094  pjssge0i  32095  pjdifnormi  32096  pjidmco  32110  mdslmd1lem3  32256  mdslmd1lem4  32257  csmdsymi  32263  hatomic  32289  atord  32317  atcvat2  32318  chirred  32324  bnj941  34762  bnj944  34928  sqdivzi  35715  onsucconn  36426  onsucsuccmp  36432  limsucncmp  36434  dedths  38955  dedths2  38958  bnd2d  49670