Theorem dedth 4522

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ex 1777  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-if 4467

This theorem is referenced by:  dedth2h  4523  dedth3h  4524  orduninsuc  7557  oeoe  8224  limensuc  8693  axcc4dom  9862  inar1  10196  supsr  10533  renegcl  10948  peano5uzti  12071  uzenom  13331  seqfn  13380  seq1  13381  seqp1  13383  hashxp  13794  smadiadetr  21283  imsmet  28467  smcn  28474  nmlno0i  28570  nmblolbi  28576  blocn  28583  dipdir  28618  dipass  28621  siilem2  28628  htth  28694  normlem6  28891  normlem7tALT  28895  normsq  28910  hhssablo  29039  hhssnvt  29041  hhsssh  29045  shintcl  29106  chintcl  29108  pjhth  29169  ococ  29182  chm0  29267  chne0  29270  chocin  29271  chj0  29273  chjo  29291  h1de2ci  29332  spansn  29335  elspansn  29342  pjch1  29446  pjinormi  29463  pjige0  29467  hoaddid1  29567  hodid  29568  nmlnop0  29774  lnopunilem2  29787  elunop2  29789  lnophm  29795  nmbdoplb  29801  nmcopex  29805  nmcoplb  29806  lnopcon  29811  lnfn0  29823  lnfnmul  29824  nmbdfnlb  29826  nmcfnex  29829  nmcfnlb  29830  lnfncon  29832  riesz4  29840  riesz1  29841  cnlnadjeu  29854  pjhmop  29926  hmopidmch  29929  hmopidmpj  29930  pjss2coi  29940  pjssmi  29941  pjssge0i  29942  pjdifnormi  29943  pjidmco  29957  mdslmd1lem3  30103  mdslmd1lem4  30104  csmdsymi  30110  hatomic  30136  atord  30164  atcvat2  30165  chirred  30171  bnj941  32044  bnj944  32210  sqdivzi  32959  onsucconn  33786  onsucsuccmp  33792  limsucncmp  33794  dedths  36097  dedths2  36100  bnd2d  44783