Theorem dedth 4585

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541  ifcif 4527

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-if 4528

This theorem is referenced by:  dedth2h  4586  dedth3h  4587  orduninsuc  7828  oeoe  8595  limensuc  9150  axcc4dom  10432  inar1  10766  supsr  11103  renegcl  11519  peano5uzti  12648  uzenom  13925  seqfn  13974  seq1  13975  seqp1  13977  hashxp  14390  smadiadetr  22168  imsmet  29931  smcn  29938  nmlno0i  30034  nmblolbi  30040  blocn  30047  dipdir  30082  dipass  30085  siilem2  30092  htth  30158  normlem6  30355  normlem7tALT  30359  normsq  30374  hhssablo  30503  hhssnvt  30505  hhsssh  30509  shintcl  30570  chintcl  30572  pjhth  30633  ococ  30646  chm0  30731  chne0  30734  chocin  30735  chj0  30737  chjo  30755  h1de2ci  30796  spansn  30799  elspansn  30806  pjch1  30910  pjinormi  30927  pjige0  30931  hoaddrid  31031  hodid  31032  nmlnop0  31238  lnopunilem2  31251  elunop2  31253  lnophm  31259  nmbdoplb  31265  nmcopex  31269  nmcoplb  31270  lnopcon  31275  lnfn0  31287  lnfnmul  31288  nmbdfnlb  31290  nmcfnex  31293  nmcfnlb  31294  lnfncon  31296  riesz4  31304  riesz1  31305  cnlnadjeu  31318  pjhmop  31390  hmopidmch  31393  hmopidmpj  31394  pjss2coi  31404  pjssmi  31405  pjssge0i  31406  pjdifnormi  31407  pjidmco  31421  mdslmd1lem3  31567  mdslmd1lem4  31568  csmdsymi  31574  hatomic  31600  atord  31628  atcvat2  31629  chirred  31635  bnj941  33771  bnj944  33937  sqdivzi  34685  onsucconn  35311  onsucsuccmp  35317  limsucncmp  35319  dedths  37820  dedths2  37823  bnd2d  47679