Theorem dedth 4584

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-if 4526

This theorem is referenced by:  dedth2h  4585  dedth3h  4586  orduninsuc  7864  oeoe  8637  limensuc  9194  axcc4dom  10481  inar1  10815  supsr  11152  renegcl  11572  peano5uzti  12708  uzenom  14005  seqfn  14054  seq1  14055  seqp1  14057  hashxp  14473  smadiadetr  22681  imsmet  30710  smcn  30717  nmlno0i  30813  nmblolbi  30819  blocn  30826  dipdir  30861  dipass  30864  siilem2  30871  htth  30937  normlem6  31134  normlem7tALT  31138  normsq  31153  hhssablo  31282  hhssnvt  31284  hhsssh  31288  shintcl  31349  chintcl  31351  pjhth  31412  ococ  31425  chm0  31510  chne0  31513  chocin  31514  chj0  31516  chjo  31534  h1de2ci  31575  spansn  31578  elspansn  31585  pjch1  31689  pjinormi  31706  pjige0  31710  hoaddrid  31810  hodid  31811  nmlnop0  32017  lnopunilem2  32030  elunop2  32032  lnophm  32038  nmbdoplb  32044  nmcopex  32048  nmcoplb  32049  lnopcon  32054  lnfn0  32066  lnfnmul  32067  nmbdfnlb  32069  nmcfnex  32072  nmcfnlb  32073  lnfncon  32075  riesz4  32083  riesz1  32084  cnlnadjeu  32097  pjhmop  32169  hmopidmch  32172  hmopidmpj  32173  pjss2coi  32183  pjssmi  32184  pjssge0i  32185  pjdifnormi  32186  pjidmco  32200  mdslmd1lem3  32346  mdslmd1lem4  32347  csmdsymi  32353  hatomic  32379  atord  32407  atcvat2  32408  chirred  32414  bnj941  34786  bnj944  34952  sqdivzi  35728  onsucconn  36439  onsucsuccmp  36445  limsucncmp  36447  dedths  38963  dedths2  38966  bnd2d  49200