Theorem dedth 4559

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 4566. If the inference has other hypotheses with class variable 𝐴, these can be kept by assigning keephyp 4572 to them. For more information, see the Weak Deduction Theorem page mmdeduction.html 4572. (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 4506	. . . 4 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
3	2	eqcomd 2741	. . 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 1540  ifcif 4500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-if 4501

This theorem is referenced by:  dedth2h  4560  dedth3h  4561  orduninsuc  7838  oeoe  8611  limensuc  9168  axcc4dom  10455  inar1  10789  supsr  11126  renegcl  11546  peano5uzti  12683  uzenom  13982  seqfn  14031  seq1  14032  seqp1  14034  hashxp  14452  smadiadetr  22613  imsmet  30672  smcn  30679  nmlno0i  30775  nmblolbi  30781  blocn  30788  dipdir  30823  dipass  30826  siilem2  30833  htth  30899  normlem6  31096  normlem7tALT  31100  normsq  31115  hhssablo  31244  hhssnvt  31246  hhsssh  31250  shintcl  31311  chintcl  31313  pjhth  31374  ococ  31387  chm0  31472  chne0  31475  chocin  31476  chj0  31478  chjo  31496  h1de2ci  31537  spansn  31540  elspansn  31547  pjch1  31651  pjinormi  31668  pjige0  31672  hoaddrid  31772  hodid  31773  nmlnop0  31979  lnopunilem2  31992  elunop2  31994  lnophm  32000  nmbdoplb  32006  nmcopex  32010  nmcoplb  32011  lnopcon  32016  lnfn0  32028  lnfnmul  32029  nmbdfnlb  32031  nmcfnex  32034  nmcfnlb  32035  lnfncon  32037  riesz4  32045  riesz1  32046  cnlnadjeu  32059  pjhmop  32131  hmopidmch  32134  hmopidmpj  32135  pjss2coi  32145  pjssmi  32146  pjssge0i  32147  pjdifnormi  32148  pjidmco  32162  mdslmd1lem3  32308  mdslmd1lem4  32309  csmdsymi  32315  hatomic  32341  atord  32369  atcvat2  32370  chirred  32376  bnj941  34803  bnj944  34969  sqdivzi  35745  onsucconn  36456  onsucsuccmp  36462  limsucncmp  36464  dedths  38980  dedths2  38983  bnd2d  49545