Theorem dedth 4523

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542  ifcif 4465

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-if 4466

This theorem is referenced by:  dedth2h  4524  dedth3h  4525  orduninsuc  7684  oeoe  8415  limensuc  8923  axcc4dom  10198  inar1  10532  supsr  10869  renegcl  11284  peano5uzti  12410  uzenom  13682  seqfn  13731  seq1  13732  seqp1  13734  hashxp  14147  smadiadetr  21822  imsmet  29049  smcn  29056  nmlno0i  29152  nmblolbi  29158  blocn  29165  dipdir  29200  dipass  29203  siilem2  29210  htth  29276  normlem6  29473  normlem7tALT  29477  normsq  29492  hhssablo  29621  hhssnvt  29623  hhsssh  29627  shintcl  29688  chintcl  29690  pjhth  29751  ococ  29764  chm0  29849  chne0  29852  chocin  29853  chj0  29855  chjo  29873  h1de2ci  29914  spansn  29917  elspansn  29924  pjch1  30028  pjinormi  30045  pjige0  30049  hoaddid1  30149  hodid  30150  nmlnop0  30356  lnopunilem2  30369  elunop2  30371  lnophm  30377  nmbdoplb  30383  nmcopex  30387  nmcoplb  30388  lnopcon  30393  lnfn0  30405  lnfnmul  30406  nmbdfnlb  30408  nmcfnex  30411  nmcfnlb  30412  lnfncon  30414  riesz4  30422  riesz1  30423  cnlnadjeu  30436  pjhmop  30508  hmopidmch  30511  hmopidmpj  30512  pjss2coi  30522  pjssmi  30523  pjssge0i  30524  pjdifnormi  30525  pjidmco  30539  mdslmd1lem3  30685  mdslmd1lem4  30686  csmdsymi  30692  hatomic  30718  atord  30746  atcvat2  30747  chirred  30753  bnj941  32748  bnj944  32914  sqdivzi  33689  onsucconn  34623  onsucsuccmp  34629  limsucncmp  34631  dedths  36972  dedths2  36975  bnd2d  46356