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

Theorem elimhyp 4504
Description: Eliminate a hypothesis containing class variable 𝐴 when it is known for a specific class 𝐵. For more information, see comments in dedth 4497. (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 4445 . . . . 5 (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
21eqcomd 2743 . . . 4 (𝜑𝐴 = if(𝜑, 𝐴, 𝐵))
3 elimhyp.1 . . . 4 (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜑𝜓))
42, 3syl 17 . . 3 (𝜑 → (𝜑𝜓))
54ibi 270 . 2 (𝜑𝜓)
6 elimhyp.3 . . 3 𝜒
7 iffalse 4448 . . . . 5 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)
87eqcomd 2743 . . . 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 1543  ifcif 4439
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-if 4440
This theorem is referenced by:  elimel  4508  elimf  6544  oeoa  8325  oeoe  8327  limensuc  8823  axcc4dom  10055  elimne0  10823  elimgt0  11670  elimge0  11671  2ndcdisj  22353  siilem2  28933  normlem7tALT  29200  hhsssh  29350  shintcl  29411  chintcl  29413  spanun  29626  elunop2  30094  lnophm  30100  nmbdfnlb  30131  hmopidmch  30234  hmopidmpj  30235  chirred  30476  limsucncmp  34372  elimhyps  36712  elimhyps2  36715
  Copyright terms: Public domain W3C validator