Theorem dedth 4536

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

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 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-if 4478

This theorem is referenced by:  dedth2h  4537  dedth3h  4538  orduninsuc  7783  oeoe  8525  limensuc  9080  axcc4dom  10349  inar1  10684  supsr  11021  renegcl  11442  peano5uzti  12580  uzenom  13885  seqfn  13934  seq1  13935  seqp1  13937  hashxp  14355  smadiadetr  22617  imsmet  30715  smcn  30722  nmlno0i  30818  nmblolbi  30824  blocn  30831  dipdir  30866  dipass  30869  siilem2  30876  htth  30942  normlem6  31139  normlem7tALT  31143  normsq  31158  hhssablo  31287  hhssnvt  31289  hhsssh  31293  shintcl  31354  chintcl  31356  pjhth  31417  ococ  31430  chm0  31515  chne0  31518  chocin  31519  chj0  31521  chjo  31539  h1de2ci  31580  spansn  31583  elspansn  31590  pjch1  31694  pjinormi  31711  pjige0  31715  hoaddrid  31815  hodid  31816  nmlnop0  32022  lnopunilem2  32035  elunop2  32037  lnophm  32043  nmbdoplb  32049  nmcopex  32053  nmcoplb  32054  lnopcon  32059  lnfn0  32071  lnfnmul  32072  nmbdfnlb  32074  nmcfnex  32077  nmcfnlb  32078  lnfncon  32080  riesz4  32088  riesz1  32089  cnlnadjeu  32102  pjhmop  32174  hmopidmch  32177  hmopidmpj  32178  pjss2coi  32188  pjssmi  32189  pjssge0i  32190  pjdifnormi  32191  pjidmco  32205  mdslmd1lem3  32351  mdslmd1lem4  32352  csmdsymi  32358  hatomic  32384  atord  32412  atcvat2  32413  chirred  32419  bnj941  34877  bnj944  35043  sqdivzi  35871  onsucconn  36581  onsucsuccmp  36587  limsucncmp  36589  dedths  39161  dedths2  39164  bnd2d  49868