Theorem dedth 4538

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-if 4480

This theorem is referenced by:  dedth2h  4539  dedth3h  4540  orduninsuc  7785  oeoe  8527  limensuc  9082  axcc4dom  10351  inar1  10686  supsr  11023  renegcl  11444  peano5uzti  12582  uzenom  13887  seqfn  13936  seq1  13937  seqp1  13939  hashxp  14357  smadiadetr  22619  imsmet  30766  smcn  30773  nmlno0i  30869  nmblolbi  30875  blocn  30882  dipdir  30917  dipass  30920  siilem2  30927  htth  30993  normlem6  31190  normlem7tALT  31194  normsq  31209  hhssablo  31338  hhssnvt  31340  hhsssh  31344  shintcl  31405  chintcl  31407  pjhth  31468  ococ  31481  chm0  31566  chne0  31569  chocin  31570  chj0  31572  chjo  31590  h1de2ci  31631  spansn  31634  elspansn  31641  pjch1  31745  pjinormi  31762  pjige0  31766  hoaddrid  31866  hodid  31867  nmlnop0  32073  lnopunilem2  32086  elunop2  32088  lnophm  32094  nmbdoplb  32100  nmcopex  32104  nmcoplb  32105  lnopcon  32110  lnfn0  32122  lnfnmul  32123  nmbdfnlb  32125  nmcfnex  32128  nmcfnlb  32129  lnfncon  32131  riesz4  32139  riesz1  32140  cnlnadjeu  32153  pjhmop  32225  hmopidmch  32228  hmopidmpj  32229  pjss2coi  32239  pjssmi  32240  pjssge0i  32241  pjdifnormi  32242  pjidmco  32256  mdslmd1lem3  32402  mdslmd1lem4  32403  csmdsymi  32409  hatomic  32435  atord  32463  atcvat2  32464  chirred  32470  bnj941  34928  bnj944  35094  sqdivzi  35922  onsucconn  36632  onsucsuccmp  36638  limsucncmp  36640  dedths  39222  dedths2  39225  bnd2d  49926