Theorem dedth 4517

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

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-if 4460

This theorem is referenced by:  dedth2h  4518  dedth3h  4519  orduninsuc  7690  oeoe  8430  limensuc  8941  axcc4dom  10197  inar1  10531  supsr  10868  renegcl  11284  peano5uzti  12410  uzenom  13684  seqfn  13733  seq1  13734  seqp1  13736  hashxp  14149  smadiadetr  21824  imsmet  29053  smcn  29060  nmlno0i  29156  nmblolbi  29162  blocn  29169  dipdir  29204  dipass  29207  siilem2  29214  htth  29280  normlem6  29477  normlem7tALT  29481  normsq  29496  hhssablo  29625  hhssnvt  29627  hhsssh  29631  shintcl  29692  chintcl  29694  pjhth  29755  ococ  29768  chm0  29853  chne0  29856  chocin  29857  chj0  29859  chjo  29877  h1de2ci  29918  spansn  29921  elspansn  29928  pjch1  30032  pjinormi  30049  pjige0  30053  hoaddid1  30153  hodid  30154  nmlnop0  30360  lnopunilem2  30373  elunop2  30375  lnophm  30381  nmbdoplb  30387  nmcopex  30391  nmcoplb  30392  lnopcon  30397  lnfn0  30409  lnfnmul  30410  nmbdfnlb  30412  nmcfnex  30415  nmcfnlb  30416  lnfncon  30418  riesz4  30426  riesz1  30427  cnlnadjeu  30440  pjhmop  30512  hmopidmch  30515  hmopidmpj  30516  pjss2coi  30526  pjssmi  30527  pjssge0i  30528  pjdifnormi  30529  pjidmco  30543  mdslmd1lem3  30689  mdslmd1lem4  30690  csmdsymi  30696  hatomic  30722  atord  30750  atcvat2  30751  chirred  30757  bnj941  32752  bnj944  32918  sqdivzi  33693  onsucconn  34627  onsucsuccmp  34633  limsucncmp  34635  dedths  36976  dedths2  36979  bnd2d  46387