Theorem dedth 4540

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569  ifcif 4481

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-if 4482

This theorem is used by:  dedth2h  4541  dedth3h  4542  orduninsuc  7858  oeoe  8615  limensuc  9180  bnd2d  9975  axcc4dom  10526  inar1  10867  supsr  11204  renegcl  11628  peano5uzti  12796  uzenom  14114  seqfn  14163  seq1  14164  seqp1  14166  hashxp  14586  smadiadetr  22999  imsmet  31302  smcn  31309  nmlno0i  31405  nmblolbi  31411  blocn  31418  dipdir  31453  dipass  31456  siilem2  31463  htth  31529  normlem6  31726  normlem7tALT  31730  normsq  31745  hhssablo  31874  hhssnvt  31876  hhsssh  31880  shintcl  31941  chintcl  31943  pjhth  32004  ococ  32017  chm0  32102  chne0  32105  chocin  32106  chj0  32108  chjo  32126  h1de2ci  32167  spansn  32170  elspansn  32177  pjch1  32281  pjinormi  32298  pjige0  32302  hoaddrid  32402  hodid  32403  nmlnop0  32609  lnopunilem2  32622  elunop2  32624  lnophm  32630  nmbdoplb  32636  nmcopex  32640  nmcoplb  32641  lnopcon  32646  lnfn0  32658  lnfnmul  32659  nmbdfnlb  32661  nmcfnex  32664  nmcfnlb  32665  lnfncon  32667  riesz4  32675  riesz1  32676  cnlnadjeu  32689  pjhmop  32761  hmopidmch  32764  hmopidmpj  32765  pjss2coi  32775  pjssmi  32776  pjssge0i  32777  pjdifnormi  32778  pjidmco  32792  mdslmd1lem3  32938  mdslmd1lem4  32939  csmdsymi  32945  hatomic  32971  atord  32999  atcvat2  33000  chirred  33006  bnj941  35453  bnj944  35618  sqdivzi  36589  onsucconn  37322  onsucsuccmp  37328  limsucncmp  37330  dedths  40128  dedths2  40131