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 2743	. . 3 ⊢ (𝜑 → 𝐴 = if(𝜑, 𝐴, 𝐵))
4		dedth.1	. . 3 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜒))
5	3, 4	syl 17	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
6	1, 5	mpbiri 258	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  ifcif 4481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-if 4482

This theorem is referenced by:  dedth2h  4541  dedth3h  4542  orduninsuc  7795  oeoe  8537  limensuc  9094  axcc4dom  10363  inar1  10698  supsr  11035  renegcl  11456  peano5uzti  12594  uzenom  13899  seqfn  13948  seq1  13949  seqp1  13951  hashxp  14369  smadiadetr  22631  imsmet  30779  smcn  30786  nmlno0i  30882  nmblolbi  30888  blocn  30895  dipdir  30930  dipass  30933  siilem2  30940  htth  31006  normlem6  31203  normlem7tALT  31207  normsq  31222  hhssablo  31351  hhssnvt  31353  hhsssh  31357  shintcl  31418  chintcl  31420  pjhth  31481  ococ  31494  chm0  31579  chne0  31582  chocin  31583  chj0  31585  chjo  31603  h1de2ci  31644  spansn  31647  elspansn  31654  pjch1  31758  pjinormi  31775  pjige0  31779  hoaddrid  31879  hodid  31880  nmlnop0  32086  lnopunilem2  32099  elunop2  32101  lnophm  32107  nmbdoplb  32113  nmcopex  32117  nmcoplb  32118  lnopcon  32123  lnfn0  32135  lnfnmul  32136  nmbdfnlb  32138  nmcfnex  32141  nmcfnlb  32142  lnfncon  32144  riesz4  32152  riesz1  32153  cnlnadjeu  32166  pjhmop  32238  hmopidmch  32241  hmopidmpj  32242  pjss2coi  32252  pjssmi  32253  pjssge0i  32254  pjdifnormi  32255  pjidmco  32269  mdslmd1lem3  32415  mdslmd1lem4  32416  csmdsymi  32422  hatomic  32448  atord  32476  atcvat2  32477  chirred  32483  bnj941  34949  bnj944  35114  sqdivzi  35944  onsucconn  36654  onsucsuccmp  36660  limsucncmp  36662  dedths  39338  dedths2  39341  bnd2d  50040