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

Theorem elimhyp 4444
Description: Eliminate a hypothesis containing class variable 𝐴 when it is known for a specific class 𝐵. For more information, see comments in dedth 4437. (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 4387 . . . . 5 (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
21eqcomd 2801 . . . 4 (𝜑𝐴 = if(𝜑, 𝐴, 𝐵))
3 elimhyp.1 . . . 4 (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜑𝜓))
42, 3syl 17 . . 3 (𝜑 → (𝜑𝜓))
54ibi 268 . 2 (𝜑𝜓)
6 elimhyp.3 . . 3 𝜒
7 iffalse 4390 . . . . 5 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)
87eqcomd 2801 . . . 4 𝜑𝐵 = if(𝜑, 𝐴, 𝐵))
9 elimhyp.2 . . . 4 (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒𝜓))
108, 9syl 17 . . 3 𝜑 → (𝜒𝜓))
116, 10mpbii 234 . 2 𝜑𝜓)
125, 11pm2.61i 183 1 𝜓
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207   = wceq 1522  ifcif 4381
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-ext 2769
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-ex 1762  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-if 4382
This theorem is referenced by:  elimel  4448  elimf  6381  oeoa  8073  oeoe  8075  limensuc  8541  axcc4dom  9709  elimne0  10477  elimgt0  11326  elimge0  11327  2ndcdisj  21748  siilem2  28320  normlem7tALT  28587  hhsssh  28737  shintcl  28798  chintcl  28800  spanun  29013  elunop2  29481  lnophm  29487  nmbdfnlb  29518  hmopidmch  29621  hmopidmpj  29622  chirred  29863  limsucncmp  33403  elimhyps  35628  elimhyps2  35631
  Copyright terms: Public domain W3C validator