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  22538  imsmet  30593  smcn  30600  nmlno0i  30696  nmblolbi  30702  blocn  30709  dipdir  30744  dipass  30747  siilem2  30754  htth  30820  normlem6  31017  normlem7tALT  31021  normsq  31036  hhssablo  31165  hhssnvt  31167  hhsssh  31171  shintcl  31232  chintcl  31234  pjhth  31295  ococ  31308  chm0  31393  chne0  31396  chocin  31397  chj0  31399  chjo  31417  h1de2ci  31458  spansn  31461  elspansn  31468  pjch1  31572  pjinormi  31589  pjige0  31593  hoaddrid  31693  hodid  31694  nmlnop0  31900  lnopunilem2  31913  elunop2  31915  lnophm  31921  nmbdoplb  31927  nmcopex  31931  nmcoplb  31932  lnopcon  31937  lnfn0  31949  lnfnmul  31950  nmbdfnlb  31952  nmcfnex  31955  nmcfnlb  31956  lnfncon  31958  riesz4  31966  riesz1  31967  cnlnadjeu  31980  pjhmop  32052  hmopidmch  32055  hmopidmpj  32056  pjss2coi  32066  pjssmi  32067  pjssge0i  32068  pjdifnormi  32069  pjidmco  32083  mdslmd1lem3  32229  mdslmd1lem4  32230  csmdsymi  32236  hatomic  32262  atord  32290  atcvat2  32291  chirred  32297  bnj941  34735  bnj944  34901  sqdivzi  35688  onsucconn  36399  onsucsuccmp  36405  limsucncmp  36407  dedths  38928  dedths2  38931  bnd2d  49643