MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cdeqi Unicode version

Theorem cdeqi 2989
Description: Deduce conditional equality. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypothesis
Ref Expression
cdeqi.1  |-  ( x  =  y  ->  ph )
Assertion
Ref Expression
cdeqi  |- CondEq ( x  =  y  ->  ph )

Proof of Theorem cdeqi
StepHypRef Expression
1 cdeqi.1 . 2  |-  ( x  =  y  ->  ph )
2 df-cdeq 2988 . 2  |-  (CondEq (
x  =  y  ->  ph )  <->  ( x  =  y  ->  ph ) )
31, 2mpbir 200 1  |- CondEq ( x  =  y  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632  CondEqwcdeq 2987
This theorem is referenced by:  cdeqth  2991  cdeqnot  2992  cdeqal  2993  cdeqab  2994  cdeqal1  2995  cdeqab1  2996  cdeqim  2997  cdeqcv  2998  cdeqeq  2999  cdeqel  3000  cdeqbox  25132  cdeqnxt  25133  cdequnt  25134
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-cdeq 2988
  Copyright terms: Public domain W3C validator