Theorem dedth 4088

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

Syntax hints:   → wi 4   ↔ wb 194   = wceq 1474  ifcif 4035

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589

This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-if 4036

This theorem is referenced by:  dedth2h  4089  dedth3h  4090  orduninsuc  6912  oeoe  7543  limensuc  7999  axcc4dom  9123  inar1  9453  supsr  9789  renegcl  10195  peano5uzti  11299  uzenom  12580  seqfn  12630  seq1  12631  seqp1  12633  hashxp  13033  smadiadetr  20242  imsmet  26727  smcn  26738  nmlno0i  26839  nmblolbi  26845  blocn  26852  dipdir  26887  dipass  26890  siilem2  26897  htth  26965  normlem6  27162  normlem7tALT  27166  normsq  27181  hhssablo  27310  hhssnvt  27312  hhsssh  27316  shintcl  27379  chintcl  27381  pjhth  27442  ococ  27455  chm0  27540  chne0  27543  chocin  27544  chj0  27546  chjo  27564  h1de2ci  27605  spansn  27608  elspansn  27615  pjch1  27719  pjinormi  27736  pjige0  27740  hoaddid1  27840  hodid  27841  nmlnop0  28047  lnopunilem2  28060  elunop2  28062  lnophm  28068  nmbdoplb  28074  nmcopex  28078  nmcoplb  28079  lnopcon  28084  lnfn0  28096  lnfnmul  28097  nmbdfnlb  28099  nmcfnex  28102  nmcfnlb  28103  lnfncon  28105  riesz4  28113  riesz1  28114  cnlnadjeu  28127  pjhmop  28199  hmopidmch  28202  hmopidmpj  28203  pjss2coi  28213  pjssmi  28214  pjssge0i  28215  pjdifnormi  28216  pjidmco  28230  mdslmd1lem3  28376  mdslmd1lem4  28377  csmdsymi  28383  hatomic  28409  atord  28437  atcvat2  28438  chirred  28444  bnj941  29903  bnj944  30068  sqdivzi  30669  onsuccon  31413  onsucsuccmp  31419  limsucncmp  31421  dedths  33062  dedths2  33065