Theorem dedth 4606

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-if 4549

This theorem is referenced by:  dedth2h  4607  dedth3h  4608  orduninsuc  7880  oeoe  8655  limensuc  9220  axcc4dom  10510  inar1  10844  supsr  11181  renegcl  11599  peano5uzti  12733  uzenom  14015  seqfn  14064  seq1  14065  seqp1  14067  hashxp  14483  smadiadetr  22702  imsmet  30723  smcn  30730  nmlno0i  30826  nmblolbi  30832  blocn  30839  dipdir  30874  dipass  30877  siilem2  30884  htth  30950  normlem6  31147  normlem7tALT  31151  normsq  31166  hhssablo  31295  hhssnvt  31297  hhsssh  31301  shintcl  31362  chintcl  31364  pjhth  31425  ococ  31438  chm0  31523  chne0  31526  chocin  31527  chj0  31529  chjo  31547  h1de2ci  31588  spansn  31591  elspansn  31598  pjch1  31702  pjinormi  31719  pjige0  31723  hoaddrid  31823  hodid  31824  nmlnop0  32030  lnopunilem2  32043  elunop2  32045  lnophm  32051  nmbdoplb  32057  nmcopex  32061  nmcoplb  32062  lnopcon  32067  lnfn0  32079  lnfnmul  32080  nmbdfnlb  32082  nmcfnex  32085  nmcfnlb  32086  lnfncon  32088  riesz4  32096  riesz1  32097  cnlnadjeu  32110  pjhmop  32182  hmopidmch  32185  hmopidmpj  32186  pjss2coi  32196  pjssmi  32197  pjssge0i  32198  pjdifnormi  32199  pjidmco  32213  mdslmd1lem3  32359  mdslmd1lem4  32360  csmdsymi  32366  hatomic  32392  atord  32420  atcvat2  32421  chirred  32427  bnj941  34748  bnj944  34914  sqdivzi  35690  onsucconn  36404  onsucsuccmp  36410  limsucncmp  36412  dedths  38918  dedths2  38921  bnd2d  48773