Theorem dedth 4172

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 4179. If the inference has other hypotheses with class variable 𝐴, these can be kept by assigning keephyp 4185 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 4125	. . . 4 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
3	2	eqcomd 2657	. . 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 1523  ifcif 4119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-if 4120

This theorem is referenced by:  dedth2h  4173  dedth3h  4174  orduninsuc  7085  oeoe  7724  limensuc  8178  axcc4dom  9301  inar1  9635  supsr  9971  renegcl  10382  peano5uzti  11505  uzenom  12803  seqfn  12853  seq1  12854  seqp1  12856  hashxp  13259  smadiadetr  20529  imsmet  27674  smcn  27681  nmlno0i  27777  nmblolbi  27783  blocn  27790  dipdir  27825  dipass  27828  siilem2  27835  htth  27903  normlem6  28100  normlem7tALT  28104  normsq  28119  hhssablo  28248  hhssnvt  28250  hhsssh  28254  shintcl  28317  chintcl  28319  pjhth  28380  ococ  28393  chm0  28478  chne0  28481  chocin  28482  chj0  28484  chjo  28502  h1de2ci  28543  spansn  28546  elspansn  28553  pjch1  28657  pjinormi  28674  pjige0  28678  hoaddid1  28778  hodid  28779  nmlnop0  28985  lnopunilem2  28998  elunop2  29000  lnophm  29006  nmbdoplb  29012  nmcopex  29016  nmcoplb  29017  lnopcon  29022  lnfn0  29034  lnfnmul  29035  nmbdfnlb  29037  nmcfnex  29040  nmcfnlb  29041  lnfncon  29043  riesz4  29051  riesz1  29052  cnlnadjeu  29065  pjhmop  29137  hmopidmch  29140  hmopidmpj  29141  pjss2coi  29151  pjssmi  29152  pjssge0i  29153  pjdifnormi  29154  pjidmco  29168  mdslmd1lem3  29314  mdslmd1lem4  29315  csmdsymi  29321  hatomic  29347  atord  29375  atcvat2  29376  chirred  29382  bnj941  30969  bnj944  31134  sqdivzi  31736  onsucconn  32562  onsucsuccmp  32568  limsucncmp  32570  dedths  34566  dedths2  34569  bnd2d  42753