Theorem dedth 4431

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1520  ifcif 4375

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-ext 2767

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-ex 1760  df-sb 2041  df-clab 2774  df-cleq 2786  df-clel 2861  df-if 4376

This theorem is referenced by:  dedth2h  4432  dedth3h  4433  orduninsuc  7405  oeoe  8066  limensuc  8531  axcc4dom  9698  inar1  10032  supsr  10369  renegcl  10786  peano5uzti  11910  uzenom  13170  seqfn  13219  seq1  13220  seqp1  13222  hashxp  13631  smadiadetr  20956  imsmet  28147  smcn  28154  nmlno0i  28250  nmblolbi  28256  blocn  28263  dipdir  28298  dipass  28301  siilem2  28308  htth  28374  normlem6  28571  normlem7tALT  28575  normsq  28590  hhssablo  28719  hhssnvt  28721  hhsssh  28725  shintcl  28786  chintcl  28788  pjhth  28849  ococ  28862  chm0  28947  chne0  28950  chocin  28951  chj0  28953  chjo  28971  h1de2ci  29012  spansn  29015  elspansn  29022  pjch1  29126  pjinormi  29143  pjige0  29147  hoaddid1  29247  hodid  29248  nmlnop0  29454  lnopunilem2  29467  elunop2  29469  lnophm  29475  nmbdoplb  29481  nmcopex  29485  nmcoplb  29486  lnopcon  29491  lnfn0  29503  lnfnmul  29504  nmbdfnlb  29506  nmcfnex  29509  nmcfnlb  29510  lnfncon  29512  riesz4  29520  riesz1  29521  cnlnadjeu  29534  pjhmop  29606  hmopidmch  29609  hmopidmpj  29610  pjss2coi  29620  pjssmi  29621  pjssge0i  29622  pjdifnormi  29623  pjidmco  29637  mdslmd1lem3  29783  mdslmd1lem4  29784  csmdsymi  29790  hatomic  29816  atord  29844  atcvat2  29845  chirred  29851  bnj941  31617  bnj944  31782  sqdivzi  32512  onsucconn  33339  onsucsuccmp  33345  limsucncmp  33347  dedths  35579  dedths2  35582  bnd2d  44218