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

Theorem elimhyp 4591
Description: Eliminate a hypothesis containing class variable 𝐴 when it is known for a specific class 𝐵. For more information, see comments in dedth 4584. (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 4531 . . . . 5 (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
21eqcomd 2743 . . . 4 (𝜑𝐴 = if(𝜑, 𝐴, 𝐵))
3 elimhyp.1 . . . 4 (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜑𝜓))
42, 3syl 17 . . 3 (𝜑 → (𝜑𝜓))
54ibi 267 . 2 (𝜑𝜓)
6 elimhyp.3 . . 3 𝜒
7 iffalse 4534 . . . . 5 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)
87eqcomd 2743 . . . 4 𝜑𝐵 = if(𝜑, 𝐴, 𝐵))
9 elimhyp.2 . . . 4 (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒𝜓))
108, 9syl 17 . . 3 𝜑 → (𝜒𝜓))
116, 10mpbii 233 . 2 𝜑𝜓)
125, 11pm2.61i 182 1 𝜓
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206   = wceq 1540  ifcif 4525
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-if 4526
This theorem is referenced by:  elimel  4595  elimf  6735  oeoa  8635  oeoe  8637  limensuc  9194  axcc4dom  10481  elimne0  11251  elimgt0  12105  elimge0  12106  2ndcdisj  23464  siilem2  30871  normlem7tALT  31138  hhsssh  31288  shintcl  31349  chintcl  31351  spanun  31564  elunop2  32032  lnophm  32038  nmbdfnlb  32069  hmopidmch  32172  hmopidmpj  32173  chirred  32414  limsucncmp  36447  elimhyps  38962  elimhyps2  38965
  Copyright terms: Public domain W3C validator