Theorem dedth 4546

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1570  ifcif 4487

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-if 4488

This theorem is referenced by:  dedth2h  4547  dedth3h  4548  orduninsuc  7835  oeoe  8581  limensuc  9138  axcc4dom  10420  inar1  10755  supsr  11092  renegcl  11516  peano5uzti  12681  uzenom  13996  seqfn  14045  seq1  14046  seqp1  14048  hashxp  14467  smadiadetr  22832  imsmet  31043  smcn  31050  nmlno0i  31146  nmblolbi  31152  blocn  31159  dipdir  31194  dipass  31197  siilem2  31204  htth  31270  normlem6  31467  normlem7tALT  31471  normsq  31486  hhssablo  31615  hhssnvt  31617  hhsssh  31621  shintcl  31682  chintcl  31684  pjhth  31745  ococ  31758  chm0  31843  chne0  31846  chocin  31847  chj0  31849  chjo  31867  h1de2ci  31908  spansn  31911  elspansn  31918  pjch1  32022  pjinormi  32039  pjige0  32043  hoaddrid  32143  hodid  32144  nmlnop0  32350  lnopunilem2  32363  elunop2  32365  lnophm  32371  nmbdoplb  32377  nmcopex  32381  nmcoplb  32382  lnopcon  32387  lnfn0  32399  lnfnmul  32400  nmbdfnlb  32402  nmcfnex  32405  nmcfnlb  32406  lnfncon  32408  riesz4  32416  riesz1  32417  cnlnadjeu  32430  pjhmop  32502  hmopidmch  32505  hmopidmpj  32506  pjss2coi  32516  pjssmi  32517  pjssge0i  32518  pjdifnormi  32519  pjidmco  32533  mdslmd1lem3  32679  mdslmd1lem4  32680  csmdsymi  32686  hatomic  32712  atord  32740  atcvat2  32741  chirred  32747  bnj941  35161  bnj944  35326  sqdivzi  36220  onsucconn  36949  onsucsuccmp  36955  limsucncmp  36957  dedths  39736  dedths2  39739  bnd2d  50459