Theorem dedth 4539

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1560  ifcif 4480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-if 4481

This theorem is referenced by:  dedth2h  4540  dedth3h  4541  orduninsuc  7823  oeoe  8569  limensuc  9126  axcc4dom  10398  inar1  10733  supsr  11070  renegcl  11494  peano5uzti  12663  uzenom  13977  seqfn  14026  seq1  14027  seqp1  14029  hashxp  14447  smadiadetr  22735  imsmet  30894  smcn  30901  nmlno0i  30997  nmblolbi  31003  blocn  31010  dipdir  31045  dipass  31048  siilem2  31055  htth  31121  normlem6  31318  normlem7tALT  31322  normsq  31337  hhssablo  31466  hhssnvt  31468  hhsssh  31472  shintcl  31533  chintcl  31535  pjhth  31596  ococ  31609  chm0  31694  chne0  31697  chocin  31698  chj0  31700  chjo  31718  h1de2ci  31759  spansn  31762  elspansn  31769  pjch1  31873  pjinormi  31890  pjige0  31894  hoaddrid  31994  hodid  31995  nmlnop0  32201  lnopunilem2  32214  elunop2  32216  lnophm  32222  nmbdoplb  32228  nmcopex  32232  nmcoplb  32233  lnopcon  32238  lnfn0  32250  lnfnmul  32251  nmbdfnlb  32253  nmcfnex  32256  nmcfnlb  32257  lnfncon  32259  riesz4  32267  riesz1  32268  cnlnadjeu  32281  pjhmop  32353  hmopidmch  32356  hmopidmpj  32357  pjss2coi  32367  pjssmi  32368  pjssge0i  32369  pjdifnormi  32370  pjidmco  32384  mdslmd1lem3  32530  mdslmd1lem4  32531  csmdsymi  32537  hatomic  32563  atord  32591  atcvat2  32592  chirred  32598  bnj941  35068  bnj944  35233  sqdivzi  36078  onsucconn  36798  onsucsuccmp  36804  limsucncmp  36806  dedths  39586  dedths2  39589  bnd2d  50302