Theorem dedth 4544

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-if 4486

This theorem is used by:  dedth2h  4545  dedth3h  4546  orduninsuc  7888  oeoe  8646  limensuc  9211  bnd2d  10005  axcc4dom  10558  inar1  10899  supsr  11236  renegcl  11660  peano5uzti  12829  uzenom  14147  seqfn  14196  seq1  14197  seqp1  14199  hashxp  14620  smadiadetr  23045  imsmet  31350  smcn  31357  nmlno0i  31453  nmblolbi  31459  blocn  31466  dipdir  31501  dipass  31504  siilem2  31511  htth  31577  normlem6  31774  normlem7tALT  31778  normsq  31793  hhssablo  31922  hhssnvt  31924  hhsssh  31928  shintcl  31989  chintcl  31991  pjhth  32052  ococ  32065  chm0  32150  chne0  32153  chocin  32154  chj0  32156  chjo  32174  h1de2ci  32215  spansn  32218  elspansn  32225  pjch1  32329  pjinormi  32346  pjige0  32350  hoaddrid  32450  hodid  32451  nmlnop0  32657  lnopunilem2  32670  elunop2  32672  lnophm  32678  nmbdoplb  32684  nmcopex  32688  nmcoplb  32689  lnopcon  32694  lnfn0  32706  lnfnmul  32707  nmbdfnlb  32709  nmcfnex  32712  nmcfnlb  32713  lnfncon  32715  riesz4  32723  riesz1  32724  cnlnadjeu  32737  pjhmop  32809  hmopidmch  32812  hmopidmpj  32813  pjss2coi  32823  pjssmi  32824  pjssge0i  32825  pjdifnormi  32826  pjidmco  32840  mdslmd1lem3  32986  mdslmd1lem4  32987  csmdsymi  32993  hatomic  33019  atord  33047  atcvat2  33048  chirred  33054  bnj941  35514  bnj944  35679  sqdivzi  36708  onsucconn  37441  onsucsuccmp  37447  limsucncmp  37449  dedths  40285  dedths2  40288