Theorem dedth 4541

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 4548. If the inference has other hypotheses with class variable 𝐴, these can be kept by assigning keephyp 4554 to them. For more information, see the Weak Deduction Theorem page mmdeduction.html 4554. (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 4488	. . . 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 1570  ifcif 4482

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-if 4483

This theorem is used by:  dedth2h  4542  dedth3h  4543  orduninsuc  7839  oeoe  8587  limensuc  9152  axcc4dom  10443  inar1  10784  supsr  11121  renegcl  11545  peano5uzti  12711  uzenom  14028  seqfn  14077  seq1  14078  seqp1  14080  hashxp  14499  smadiadetr  22897  imsmet  31172  smcn  31179  nmlno0i  31275  nmblolbi  31281  blocn  31288  dipdir  31323  dipass  31326  siilem2  31333  htth  31399  normlem6  31596  normlem7tALT  31600  normsq  31615  hhssablo  31744  hhssnvt  31746  hhsssh  31750  shintcl  31811  chintcl  31813  pjhth  31874  ococ  31887  chm0  31972  chne0  31975  chocin  31976  chj0  31978  chjo  31996  h1de2ci  32037  spansn  32040  elspansn  32047  pjch1  32151  pjinormi  32168  pjige0  32172  hoaddrid  32272  hodid  32273  nmlnop0  32479  lnopunilem2  32492  elunop2  32494  lnophm  32500  nmbdoplb  32506  nmcopex  32510  nmcoplb  32511  lnopcon  32516  lnfn0  32528  lnfnmul  32529  nmbdfnlb  32531  nmcfnex  32534  nmcfnlb  32535  lnfncon  32537  riesz4  32545  riesz1  32546  cnlnadjeu  32559  pjhmop  32631  hmopidmch  32634  hmopidmpj  32635  pjss2coi  32645  pjssmi  32646  pjssge0i  32647  pjdifnormi  32648  pjidmco  32662  mdslmd1lem3  32808  mdslmd1lem4  32809  csmdsymi  32815  hatomic  32841  atord  32869  atcvat2  32870  chirred  32876  bnj941  35282  bnj944  35447  sqdivzi  36307  onsucconn  37057  onsucsuccmp  37063  limsucncmp  37065  dedths  39835  dedths2  39838  bnd2d  50607