Theorem dedth 4513

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547  ifcif 4454

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-if 4455

This theorem is referenced by:  dedth2h  4514  dedth3h  4515  orduninsuc  7783  oeoe  8525  limensuc  9082  axcc4dom  10354  inar1  10689  supsr  11026  renegcl  11448  peano5uzti  12610  uzenom  13917  seqfn  13966  seq1  13967  seqp1  13969  hashxp  14387  smadiadetr  22658  imsmet  30780  smcn  30787  nmlno0i  30883  nmblolbi  30889  blocn  30896  dipdir  30931  dipass  30934  siilem2  30941  htth  31007  normlem6  31204  normlem7tALT  31208  normsq  31223  hhssablo  31352  hhssnvt  31354  hhsssh  31358  shintcl  31419  chintcl  31421  pjhth  31482  ococ  31495  chm0  31580  chne0  31583  chocin  31584  chj0  31586  chjo  31604  h1de2ci  31645  spansn  31648  elspansn  31655  pjch1  31759  pjinormi  31776  pjige0  31780  hoaddrid  31880  hodid  31881  nmlnop0  32087  lnopunilem2  32100  elunop2  32102  lnophm  32108  nmbdoplb  32114  nmcopex  32118  nmcoplb  32119  lnopcon  32124  lnfn0  32136  lnfnmul  32137  nmbdfnlb  32139  nmcfnex  32142  nmcfnlb  32143  lnfncon  32145  riesz4  32153  riesz1  32154  cnlnadjeu  32167  pjhmop  32239  hmopidmch  32242  hmopidmpj  32243  pjss2coi  32253  pjssmi  32254  pjssge0i  32255  pjdifnormi  32256  pjidmco  32270  mdslmd1lem3  32416  mdslmd1lem4  32417  csmdsymi  32423  hatomic  32449  atord  32477  atcvat2  32478  chirred  32484  bnj941  34955  bnj944  35120  sqdivzi  35956  onsucconn  36666  onsucsuccmp  36672  limsucncmp  36674  dedths  39454  dedths2  39457  bnd2d  50171