Theorem dedth 4541

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  ifcif 4482

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-if 4483

This theorem is used by:  dedth2h  4542  dedth3h  4543  orduninsuc  7852  oeoe  8601  limensuc  9166  bnd2d  9961  axcc4dom  10512  inar1  10853  supsr  11190  renegcl  11614  peano5uzti  12782  uzenom  14100  seqfn  14149  seq1  14150  seqp1  14152  hashxp  14572  smadiadetr  22983  imsmet  31286  smcn  31293  nmlno0i  31389  nmblolbi  31395  blocn  31402  dipdir  31437  dipass  31440  siilem2  31447  htth  31513  normlem6  31710  normlem7tALT  31714  normsq  31729  hhssablo  31858  hhssnvt  31860  hhsssh  31864  shintcl  31925  chintcl  31927  pjhth  31988  ococ  32001  chm0  32086  chne0  32089  chocin  32090  chj0  32092  chjo  32110  h1de2ci  32151  spansn  32154  elspansn  32161  pjch1  32265  pjinormi  32282  pjige0  32286  hoaddrid  32386  hodid  32387  nmlnop0  32593  lnopunilem2  32606  elunop2  32608  lnophm  32614  nmbdoplb  32620  nmcopex  32624  nmcoplb  32625  lnopcon  32630  lnfn0  32642  lnfnmul  32643  nmbdfnlb  32645  nmcfnex  32648  nmcfnlb  32649  lnfncon  32651  riesz4  32659  riesz1  32660  cnlnadjeu  32673  pjhmop  32745  hmopidmch  32748  hmopidmpj  32749  pjss2coi  32759  pjssmi  32760  pjssge0i  32761  pjdifnormi  32762  pjidmco  32776  mdslmd1lem3  32922  mdslmd1lem4  32923  csmdsymi  32929  hatomic  32955  atord  32983  atcvat2  32984  chirred  32990  bnj941  35396  bnj944  35561  sqdivzi  36472  onsucconn  37206  onsucsuccmp  37212  limsucncmp  37214  dedths  39999  dedths2  40002