Theorem dedth 4551

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1567  ifcif 4492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-if 4493

This theorem is referenced by:  dedth2h  4552  dedth3h  4553  orduninsuc  7838  oeoe  8584  limensuc  9141  axcc4dom  10424  inar1  10759  supsr  11096  renegcl  11520  peano5uzti  12685  uzenom  13999  seqfn  14048  seq1  14049  seqp1  14051  hashxp  14470  smadiadetr  22800  imsmet  30983  smcn  30990  nmlno0i  31086  nmblolbi  31092  blocn  31099  dipdir  31134  dipass  31137  siilem2  31144  htth  31210  normlem6  31407  normlem7tALT  31411  normsq  31426  hhssablo  31555  hhssnvt  31557  hhsssh  31561  shintcl  31622  chintcl  31624  pjhth  31685  ococ  31698  chm0  31783  chne0  31786  chocin  31787  chj0  31789  chjo  31807  h1de2ci  31848  spansn  31851  elspansn  31858  pjch1  31962  pjinormi  31979  pjige0  31983  hoaddrid  32083  hodid  32084  nmlnop0  32290  lnopunilem2  32303  elunop2  32305  lnophm  32311  nmbdoplb  32317  nmcopex  32321  nmcoplb  32322  lnopcon  32327  lnfn0  32339  lnfnmul  32340  nmbdfnlb  32342  nmcfnex  32345  nmcfnlb  32346  lnfncon  32348  riesz4  32356  riesz1  32357  cnlnadjeu  32370  pjhmop  32442  hmopidmch  32445  hmopidmpj  32446  pjss2coi  32456  pjssmi  32457  pjssge0i  32458  pjdifnormi  32459  pjidmco  32473  mdslmd1lem3  32619  mdslmd1lem4  32620  csmdsymi  32626  hatomic  32652  atord  32680  atcvat2  32681  chirred  32687  bnj941  35105  bnj944  35270  sqdivzi  36118  onsucconn  36837  onsucsuccmp  36843  limsucncmp  36845  dedths  39625  dedths2  39628  bnd2d  50343