Theorem dedth 4587

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542  ifcif 4529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-if 4530

This theorem is referenced by:  dedth2h  4588  dedth3h  4589  orduninsuc  7832  oeoe  8599  limensuc  9154  axcc4dom  10436  inar1  10770  supsr  11107  renegcl  11523  peano5uzti  12652  uzenom  13929  seqfn  13978  seq1  13979  seqp1  13981  hashxp  14394  smadiadetr  22177  imsmet  29944  smcn  29951  nmlno0i  30047  nmblolbi  30053  blocn  30060  dipdir  30095  dipass  30098  siilem2  30105  htth  30171  normlem6  30368  normlem7tALT  30372  normsq  30387  hhssablo  30516  hhssnvt  30518  hhsssh  30522  shintcl  30583  chintcl  30585  pjhth  30646  ococ  30659  chm0  30744  chne0  30747  chocin  30748  chj0  30750  chjo  30768  h1de2ci  30809  spansn  30812  elspansn  30819  pjch1  30923  pjinormi  30940  pjige0  30944  hoaddrid  31044  hodid  31045  nmlnop0  31251  lnopunilem2  31264  elunop2  31266  lnophm  31272  nmbdoplb  31278  nmcopex  31282  nmcoplb  31283  lnopcon  31288  lnfn0  31300  lnfnmul  31301  nmbdfnlb  31303  nmcfnex  31306  nmcfnlb  31307  lnfncon  31309  riesz4  31317  riesz1  31318  cnlnadjeu  31331  pjhmop  31403  hmopidmch  31406  hmopidmpj  31407  pjss2coi  31417  pjssmi  31418  pjssge0i  31419  pjdifnormi  31420  pjidmco  31434  mdslmd1lem3  31580  mdslmd1lem4  31581  csmdsymi  31587  hatomic  31613  atord  31641  atcvat2  31642  chirred  31648  bnj941  33783  bnj944  33949  sqdivzi  34697  onsucconn  35323  onsucsuccmp  35329  limsucncmp  35331  dedths  37832  dedths2  37835  bnd2d  47726