Theorem dedth 4089

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

Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475  ifcif 4036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-if 4037

This theorem is referenced by:  dedth2h  4090  dedth3h  4091  orduninsuc  6935  oeoe  7566  limensuc  8022  axcc4dom  9146  inar1  9476  supsr  9812  renegcl  10223  peano5uzti  11343  uzenom  12625  seqfn  12675  seq1  12676  seqp1  12678  hashxp  13081  smadiadetr  20300  imsmet  26930  smcn  26937  nmlno0i  27033  nmblolbi  27039  blocn  27046  dipdir  27081  dipass  27084  siilem2  27091  htth  27159  normlem6  27356  normlem7tALT  27360  normsq  27375  hhssablo  27504  hhssnvt  27506  hhsssh  27510  shintcl  27573  chintcl  27575  pjhth  27636  ococ  27649  chm0  27734  chne0  27737  chocin  27738  chj0  27740  chjo  27758  h1de2ci  27799  spansn  27802  elspansn  27809  pjch1  27913  pjinormi  27930  pjige0  27934  hoaddid1  28034  hodid  28035  nmlnop0  28241  lnopunilem2  28254  elunop2  28256  lnophm  28262  nmbdoplb  28268  nmcopex  28272  nmcoplb  28273  lnopcon  28278  lnfn0  28290  lnfnmul  28291  nmbdfnlb  28293  nmcfnex  28296  nmcfnlb  28297  lnfncon  28299  riesz4  28307  riesz1  28308  cnlnadjeu  28321  pjhmop  28393  hmopidmch  28396  hmopidmpj  28397  pjss2coi  28407  pjssmi  28408  pjssge0i  28409  pjdifnormi  28410  pjidmco  28424  mdslmd1lem3  28570  mdslmd1lem4  28571  csmdsymi  28577  hatomic  28603  atord  28631  atcvat2  28632  chirred  28638  bnj941  30097  bnj944  30262  sqdivzi  30863  onsuccon  31607  onsucsuccmp  31613  limsucncmp  31615  dedths  33266  dedths2  33269  bnd2d  42226