Theorem dedth 4588

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-if 4531

This theorem is referenced by:  dedth2h  4589  dedth3h  4590  orduninsuc  7848  oeoe  8620  limensuc  9179  axcc4dom  10466  inar1  10800  supsr  11137  renegcl  11555  peano5uzti  12685  uzenom  13965  seqfn  14014  seq1  14015  seqp1  14017  hashxp  14429  smadiadetr  22621  imsmet  30573  smcn  30580  nmlno0i  30676  nmblolbi  30682  blocn  30689  dipdir  30724  dipass  30727  siilem2  30734  htth  30800  normlem6  30997  normlem7tALT  31001  normsq  31016  hhssablo  31145  hhssnvt  31147  hhsssh  31151  shintcl  31212  chintcl  31214  pjhth  31275  ococ  31288  chm0  31373  chne0  31376  chocin  31377  chj0  31379  chjo  31397  h1de2ci  31438  spansn  31441  elspansn  31448  pjch1  31552  pjinormi  31569  pjige0  31573  hoaddrid  31673  hodid  31674  nmlnop0  31880  lnopunilem2  31893  elunop2  31895  lnophm  31901  nmbdoplb  31907  nmcopex  31911  nmcoplb  31912  lnopcon  31917  lnfn0  31929  lnfnmul  31930  nmbdfnlb  31932  nmcfnex  31935  nmcfnlb  31936  lnfncon  31938  riesz4  31946  riesz1  31947  cnlnadjeu  31960  pjhmop  32032  hmopidmch  32035  hmopidmpj  32036  pjss2coi  32046  pjssmi  32047  pjssge0i  32048  pjdifnormi  32049  pjidmco  32063  mdslmd1lem3  32209  mdslmd1lem4  32210  csmdsymi  32216  hatomic  32242  atord  32270  atcvat2  32271  chirred  32277  bnj941  34534  bnj944  34700  sqdivzi  35453  onsucconn  36053  onsucsuccmp  36059  limsucncmp  36061  dedths  38564  dedths2  38567  bnd2d  48298