Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  elimhyp Structured version   Visualization version   GIF version

Theorem elimhyp 4488
 Description: Eliminate a hypothesis containing class variable 𝐴 when it is known for a specific class 𝐵. For more information, see comments in dedth 4481. (Contributed by NM, 15-May-1999.)
Hypotheses
Ref Expression
elimhyp.1 (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜑𝜓))
elimhyp.2 (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒𝜓))
elimhyp.3 𝜒
Assertion
Ref Expression
elimhyp 𝜓

Proof of Theorem elimhyp
StepHypRef Expression
1 iftrue 4431 . . . . 5 (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
21eqcomd 2804 . . . 4 (𝜑𝐴 = if(𝜑, 𝐴, 𝐵))
3 elimhyp.1 . . . 4 (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜑𝜓))
42, 3syl 17 . . 3 (𝜑 → (𝜑𝜓))
54ibi 270 . 2 (𝜑𝜓)
6 elimhyp.3 . . 3 𝜒
7 iffalse 4434 . . . . 5 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)
87eqcomd 2804 . . . 4 𝜑𝐵 = if(𝜑, 𝐴, 𝐵))
9 elimhyp.2 . . . 4 (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒𝜓))
108, 9syl 17 . . 3 𝜑 → (𝜒𝜓))
116, 10mpbii 236 . 2 𝜑𝜓)
125, 11pm2.61i 185 1 𝜓
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   = wceq 1538  ifcif 4425 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-if 4426 This theorem is referenced by:  elimel  4492  elimf  6486  oeoa  8208  oeoe  8210  limensuc  8680  axcc4dom  9854  elimne0  10622  elimgt0  11469  elimge0  11470  2ndcdisj  22068  siilem2  28642  normlem7tALT  28909  hhsssh  29059  shintcl  29120  chintcl  29122  spanun  29335  elunop2  29803  lnophm  29809  nmbdfnlb  29840  hmopidmch  29943  hmopidmpj  29944  chirred  30185  limsucncmp  33919  elimhyps  36273  elimhyps2  36276
 Copyright terms: Public domain W3C validator