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

Theorem elimhyp 4593
Description: Eliminate a hypothesis containing class variable 𝐴 when it is known for a specific class 𝐵. For more information, see comments in dedth 4586. (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 4534 . . . . 5 (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
21eqcomd 2737 . . . 4 (𝜑𝐴 = if(𝜑, 𝐴, 𝐵))
3 elimhyp.1 . . . 4 (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜑𝜓))
42, 3syl 17 . . 3 (𝜑 → (𝜑𝜓))
54ibi 267 . 2 (𝜑𝜓)
6 elimhyp.3 . . 3 𝜒
7 iffalse 4537 . . . . 5 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)
87eqcomd 2737 . . . 4 𝜑𝐵 = if(𝜑, 𝐴, 𝐵))
9 elimhyp.2 . . . 4 (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒𝜓))
108, 9syl 17 . . 3 𝜑 → (𝜒𝜓))
116, 10mpbii 232 . 2 𝜑𝜓)
125, 11pm2.61i 182 1 𝜓
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205   = wceq 1540  ifcif 4528
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-if 4529
This theorem is referenced by:  elimel  4597  elimf  6716  oeoa  8601  oeoe  8603  limensuc  9158  axcc4dom  10440  elimne0  11209  elimgt0  12057  elimge0  12058  2ndcdisj  23181  siilem2  30373  normlem7tALT  30640  hhsssh  30790  shintcl  30851  chintcl  30853  spanun  31066  elunop2  31534  lnophm  31540  nmbdfnlb  31571  hmopidmch  31674  hmopidmpj  31675  chirred  31916  limsucncmp  35635  elimhyps  38135  elimhyps2  38138
  Copyright terms: Public domain W3C validator