Theorem dedth 4543

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 4550. If the inference has other hypotheses with class variable 𝐴, these can be kept by assigning keephyp 4556 to them. For more information, see the Weak Deduction Theorem page mmdeduction.html 4556. (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 4490	. . . 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 4484

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 4485

This theorem is referenced by:  dedth2h  4544  dedth3h  4545  orduninsuc  7799  oeoe  8540  limensuc  9095  axcc4dom  10370  inar1  10704  supsr  11041  renegcl  11461  peano5uzti  12600  uzenom  13905  seqfn  13954  seq1  13955  seqp1  13957  hashxp  14375  smadiadetr  22595  imsmet  30670  smcn  30677  nmlno0i  30773  nmblolbi  30779  blocn  30786  dipdir  30821  dipass  30824  siilem2  30831  htth  30897  normlem6  31094  normlem7tALT  31098  normsq  31113  hhssablo  31242  hhssnvt  31244  hhsssh  31248  shintcl  31309  chintcl  31311  pjhth  31372  ococ  31385  chm0  31470  chne0  31473  chocin  31474  chj0  31476  chjo  31494  h1de2ci  31535  spansn  31538  elspansn  31545  pjch1  31649  pjinormi  31666  pjige0  31670  hoaddrid  31770  hodid  31771  nmlnop0  31977  lnopunilem2  31990  elunop2  31992  lnophm  31998  nmbdoplb  32004  nmcopex  32008  nmcoplb  32009  lnopcon  32014  lnfn0  32026  lnfnmul  32027  nmbdfnlb  32029  nmcfnex  32032  nmcfnlb  32033  lnfncon  32035  riesz4  32043  riesz1  32044  cnlnadjeu  32057  pjhmop  32129  hmopidmch  32132  hmopidmpj  32133  pjss2coi  32143  pjssmi  32144  pjssge0i  32145  pjdifnormi  32146  pjidmco  32160  mdslmd1lem3  32306  mdslmd1lem4  32307  csmdsymi  32313  hatomic  32339  atord  32367  atcvat2  32368  chirred  32374  bnj941  34755  bnj944  34921  sqdivzi  35708  onsucconn  36419  onsucsuccmp  36425  limsucncmp  36427  dedths  38948  dedths2  38951  bnd2d  49663