Theorem dedth 4284

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's hypothesis eliminated with elimhyp 4291. If the inference has other hypotheses with class variable 𝐴, these can be kept by assigning keephyp 4297 to them. For more information, see the Weak Deduction Theorem page mmdeduction.html. (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 4237	. . . 4 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
3	2	eqcomd 2767	. . 3 ⊢ (𝜑 → 𝐴 = if(𝜑, 𝐴, 𝐵))
4		dedth.1	. . 3 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜒))
5	3, 4	syl 17	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
6	1, 5	mpbiri 248	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1632  ifcif 4231

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-clab 2748  df-cleq 2754  df-clel 2757  df-if 4232

This theorem is referenced by:  dedth2h  4285  dedth3h  4286  orduninsuc  7210  oeoe  7851  limensuc  8305  axcc4dom  9476  inar1  9810  supsr  10146  renegcl  10557  peano5uzti  11680  uzenom  12978  seqfn  13028  seq1  13029  seqp1  13031  hashxp  13434  smadiadetr  20704  imsmet  27877  smcn  27884  nmlno0i  27980  nmblolbi  27986  blocn  27993  dipdir  28028  dipass  28031  siilem2  28038  htth  28106  normlem6  28303  normlem7tALT  28307  normsq  28322  hhssablo  28451  hhssnvt  28453  hhsssh  28457  shintcl  28520  chintcl  28522  pjhth  28583  ococ  28596  chm0  28681  chne0  28684  chocin  28685  chj0  28687  chjo  28705  h1de2ci  28746  spansn  28749  elspansn  28756  pjch1  28860  pjinormi  28877  pjige0  28881  hoaddid1  28981  hodid  28982  nmlnop0  29188  lnopunilem2  29201  elunop2  29203  lnophm  29209  nmbdoplb  29215  nmcopex  29219  nmcoplb  29220  lnopcon  29225  lnfn0  29237  lnfnmul  29238  nmbdfnlb  29240  nmcfnex  29243  nmcfnlb  29244  lnfncon  29246  riesz4  29254  riesz1  29255  cnlnadjeu  29268  pjhmop  29340  hmopidmch  29343  hmopidmpj  29344  pjss2coi  29354  pjssmi  29355  pjssge0i  29356  pjdifnormi  29357  pjidmco  29371  mdslmd1lem3  29517  mdslmd1lem4  29518  csmdsymi  29524  hatomic  29550  atord  29578  atcvat2  29579  chirred  29585  bnj941  31172  bnj944  31337  sqdivzi  31939  onsucconn  32765  onsucsuccmp  32771  limsucncmp  32773  dedths  34770  dedths2  34773  bnd2d  42957