Theorem dedth 4531

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  ifcif 4472

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-if 4473

This theorem is referenced by:  dedth2h  4532  dedth3h  4533  orduninsuc  7773  oeoe  8514  limensuc  9067  axcc4dom  10332  inar1  10666  supsr  11003  renegcl  11424  peano5uzti  12563  uzenom  13871  seqfn  13920  seq1  13921  seqp1  13923  hashxp  14341  smadiadetr  22590  imsmet  30671  smcn  30678  nmlno0i  30774  nmblolbi  30780  blocn  30787  dipdir  30822  dipass  30825  siilem2  30832  htth  30898  normlem6  31095  normlem7tALT  31099  normsq  31114  hhssablo  31243  hhssnvt  31245  hhsssh  31249  shintcl  31310  chintcl  31312  pjhth  31373  ococ  31386  chm0  31471  chne0  31474  chocin  31475  chj0  31477  chjo  31495  h1de2ci  31536  spansn  31539  elspansn  31546  pjch1  31650  pjinormi  31667  pjige0  31671  hoaddrid  31771  hodid  31772  nmlnop0  31978  lnopunilem2  31991  elunop2  31993  lnophm  31999  nmbdoplb  32005  nmcopex  32009  nmcoplb  32010  lnopcon  32015  lnfn0  32027  lnfnmul  32028  nmbdfnlb  32030  nmcfnex  32033  nmcfnlb  32034  lnfncon  32036  riesz4  32044  riesz1  32045  cnlnadjeu  32058  pjhmop  32130  hmopidmch  32133  hmopidmpj  32134  pjss2coi  32144  pjssmi  32145  pjssge0i  32146  pjdifnormi  32147  pjidmco  32161  mdslmd1lem3  32307  mdslmd1lem4  32308  csmdsymi  32314  hatomic  32340  atord  32368  atcvat2  32369  chirred  32375  bnj941  34784  bnj944  34950  sqdivzi  35772  onsucconn  36480  onsucsuccmp  36486  limsucncmp  36488  dedths  39009  dedths2  39012  bnd2d  49721