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

Theorem elimhyp 4096
 Description: Eliminate a hypothesis containing class variable 𝐴 when it is known for a specific class 𝐵. For more information, see comments in dedth 4089. (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 4042 . . . . 5 (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
21eqcomd 2616 . . . 4 (𝜑𝐴 = if(𝜑, 𝐴, 𝐵))
3 elimhyp.1 . . . 4 (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜑𝜓))
42, 3syl 17 . . 3 (𝜑 → (𝜑𝜓))
54ibi 255 . 2 (𝜑𝜓)
6 elimhyp.3 . . 3 𝜒
7 iffalse 4045 . . . . 5 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)
87eqcomd 2616 . . . 4 𝜑𝐵 = if(𝜑, 𝐴, 𝐵))
9 elimhyp.2 . . . 4 (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒𝜓))
108, 9syl 17 . . 3 𝜑 → (𝜒𝜓))
116, 10mpbii 222 . 2 𝜑𝜓)
125, 11pm2.61i 175 1 𝜓
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   = wceq 1475  ifcif 4036 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-if 4037 This theorem is referenced by:  elimel  4100  elimf  5957  oeoa  7564  oeoe  7566  limensuc  8022  axcc4dom  9146  elimne0  9909  elimgt0  10738  elimge0  10739  2ndcdisj  21069  siilem2  27091  normlem7tALT  27360  hhsssh  27510  shintcl  27573  chintcl  27575  spanun  27788  elunop2  28256  lnophm  28262  nmbdfnlb  28293  hmopidmch  28396  hmopidmpj  28397  chirred  28638  limsucncmp  31615  elimhyps  33265  elimhyps2  33268
 Copyright terms: Public domain W3C validator