Theorem dedth 4329

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 4336. If the inference has other hypotheses with class variable 𝐴, these can be kept by assigning keephyp 4342 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 4279	. . . 4 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
3	2	eqcomd 2808	. . 3 ⊢ (𝜑 → 𝐴 = if(𝜑, 𝐴, 𝐵))
4		dedth.1	. . 3 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜒))
5	3, 4	syl 17	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
6	1, 5	mpbiri 249	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 197   = wceq 1637  ifcif 4273

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-ext 2781

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-clab 2789  df-cleq 2795  df-clel 2798  df-if 4274

This theorem is referenced by:  dedth2h  4330  dedth3h  4331  orduninsuc  7267  oeoe  7910  limensuc  8370  axcc4dom  9542  inar1  9876  supsr  10212  renegcl  10623  peano5uzti  11727  uzenom  12981  seqfn  13030  seq1  13031  seqp1  13033  hashxp  13432  smadiadetr  20687  imsmet  27868  smcn  27875  nmlno0i  27971  nmblolbi  27977  blocn  27984  dipdir  28019  dipass  28022  siilem2  28029  htth  28097  normlem6  28294  normlem7tALT  28298  normsq  28313  hhssablo  28442  hhssnvt  28444  hhsssh  28448  shintcl  28511  chintcl  28513  pjhth  28574  ococ  28587  chm0  28672  chne0  28675  chocin  28676  chj0  28678  chjo  28696  h1de2ci  28737  spansn  28740  elspansn  28747  pjch1  28851  pjinormi  28868  pjige0  28872  hoaddid1  28972  hodid  28973  nmlnop0  29179  lnopunilem2  29192  elunop2  29194  lnophm  29200  nmbdoplb  29206  nmcopex  29210  nmcoplb  29211  lnopcon  29216  lnfn0  29228  lnfnmul  29229  nmbdfnlb  29231  nmcfnex  29234  nmcfnlb  29235  lnfncon  29237  riesz4  29245  riesz1  29246  cnlnadjeu  29259  pjhmop  29331  hmopidmch  29334  hmopidmpj  29335  pjss2coi  29345  pjssmi  29346  pjssge0i  29347  pjdifnormi  29348  pjidmco  29362  mdslmd1lem3  29508  mdslmd1lem4  29509  csmdsymi  29515  hatomic  29541  atord  29569  atcvat2  29570  chirred  29576  bnj941  31160  bnj944  31325  sqdivzi  31926  onsucconn  32748  onsucsuccmp  32754  limsucncmp  32756  dedths  34735  dedths2  34738  bnd2d  42990