Theorem dedth 4548

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

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-if 4490

This theorem is used by:  dedth2h  4549  dedth3h  4550  orduninsuc  7845  oeoe  8591  limensuc  9149  axcc4dom  10440  inar1  10775  supsr  11112  renegcl  11536  peano5uzti  12702  uzenom  14018  seqfn  14067  seq1  14068  seqp1  14070  hashxp  14489  smadiadetr  22882  imsmet  31114  smcn  31121  nmlno0i  31217  nmblolbi  31223  blocn  31230  dipdir  31265  dipass  31268  siilem2  31275  htth  31341  normlem6  31538  normlem7tALT  31542  normsq  31557  hhssablo  31686  hhssnvt  31688  hhsssh  31692  shintcl  31753  chintcl  31755  pjhth  31816  ococ  31829  chm0  31914  chne0  31917  chocin  31918  chj0  31920  chjo  31938  h1de2ci  31979  spansn  31982  elspansn  31989  pjch1  32093  pjinormi  32110  pjige0  32114  hoaddrid  32214  hodid  32215  nmlnop0  32421  lnopunilem2  32434  elunop2  32436  lnophm  32442  nmbdoplb  32448  nmcopex  32452  nmcoplb  32453  lnopcon  32458  lnfn0  32470  lnfnmul  32471  nmbdfnlb  32473  nmcfnex  32476  nmcfnlb  32477  lnfncon  32479  riesz4  32487  riesz1  32488  cnlnadjeu  32501  pjhmop  32573  hmopidmch  32576  hmopidmpj  32577  pjss2coi  32587  pjssmi  32588  pjssge0i  32589  pjdifnormi  32590  pjidmco  32604  mdslmd1lem3  32750  mdslmd1lem4  32751  csmdsymi  32757  hatomic  32783  atord  32811  atcvat2  32812  chirred  32818  bnj941  35226  bnj944  35391  sqdivzi  36257  onsucconn  37006  onsucsuccmp  37012  limsucncmp  37014  dedths  39794  dedths2  39797  bnd2d  50516