Theorem dedth 4139

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

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1483  ifcif 4086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-if 4087

This theorem is referenced by:  dedth2h  4140  dedth3h  4141  orduninsuc  7043  oeoe  7679  limensuc  8137  axcc4dom  9263  inar1  9597  supsr  9933  renegcl  10344  peano5uzti  11467  uzenom  12763  seqfn  12813  seq1  12814  seqp1  12816  hashxp  13221  smadiadetr  20481  imsmet  27546  smcn  27553  nmlno0i  27649  nmblolbi  27655  blocn  27662  dipdir  27697  dipass  27700  siilem2  27707  htth  27775  normlem6  27972  normlem7tALT  27976  normsq  27991  hhssablo  28120  hhssnvt  28122  hhsssh  28126  shintcl  28189  chintcl  28191  pjhth  28252  ococ  28265  chm0  28350  chne0  28353  chocin  28354  chj0  28356  chjo  28374  h1de2ci  28415  spansn  28418  elspansn  28425  pjch1  28529  pjinormi  28546  pjige0  28550  hoaddid1  28650  hodid  28651  nmlnop0  28857  lnopunilem2  28870  elunop2  28872  lnophm  28878  nmbdoplb  28884  nmcopex  28888  nmcoplb  28889  lnopcon  28894  lnfn0  28906  lnfnmul  28907  nmbdfnlb  28909  nmcfnex  28912  nmcfnlb  28913  lnfncon  28915  riesz4  28923  riesz1  28924  cnlnadjeu  28937  pjhmop  29009  hmopidmch  29012  hmopidmpj  29013  pjss2coi  29023  pjssmi  29024  pjssge0i  29025  pjdifnormi  29026  pjidmco  29040  mdslmd1lem3  29186  mdslmd1lem4  29187  csmdsymi  29193  hatomic  29219  atord  29247  atcvat2  29248  chirred  29254  bnj941  30843  bnj944  31008  sqdivzi  31610  onsucconn  32437  onsucsuccmp  32443  limsucncmp  32445  dedths  34248  dedths2  34251  bnd2d  42428