Theorem dedth 4535

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-if 4477

This theorem is referenced by:  dedth2h  4536  dedth3h  4537  orduninsuc  7776  oeoe  8517  limensuc  9071  axcc4dom  10335  inar1  10669  supsr  11006  renegcl  11427  peano5uzti  12566  uzenom  13871  seqfn  13920  seq1  13921  seqp1  13923  hashxp  14341  smadiadetr  22560  imsmet  30635  smcn  30642  nmlno0i  30738  nmblolbi  30744  blocn  30751  dipdir  30786  dipass  30789  siilem2  30796  htth  30862  normlem6  31059  normlem7tALT  31063  normsq  31078  hhssablo  31207  hhssnvt  31209  hhsssh  31213  shintcl  31274  chintcl  31276  pjhth  31337  ococ  31350  chm0  31435  chne0  31438  chocin  31439  chj0  31441  chjo  31459  h1de2ci  31500  spansn  31503  elspansn  31510  pjch1  31614  pjinormi  31631  pjige0  31635  hoaddrid  31735  hodid  31736  nmlnop0  31942  lnopunilem2  31955  elunop2  31957  lnophm  31963  nmbdoplb  31969  nmcopex  31973  nmcoplb  31974  lnopcon  31979  lnfn0  31991  lnfnmul  31992  nmbdfnlb  31994  nmcfnex  31997  nmcfnlb  31998  lnfncon  32000  riesz4  32008  riesz1  32009  cnlnadjeu  32022  pjhmop  32094  hmopidmch  32097  hmopidmpj  32098  pjss2coi  32108  pjssmi  32109  pjssge0i  32110  pjdifnormi  32111  pjidmco  32125  mdslmd1lem3  32271  mdslmd1lem4  32272  csmdsymi  32278  hatomic  32304  atord  32332  atcvat2  32333  chirred  32339  bnj941  34739  bnj944  34905  sqdivzi  35701  onsucconn  36412  onsucsuccmp  36418  limsucncmp  36420  dedths  38941  dedths2  38944  bnd2d  49666