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

Theorem cdeqi 2976
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 2975 . 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 1623  CondEqwcdeq 2974
This theorem is referenced by:  cdeqth  2978  cdeqnot  2979  cdeqal  2980  cdeqab  2981  cdeqal1  2982  cdeqab1  2983  cdeqim  2984  cdeqcv  2985  cdeqeq  2986  cdeqel  2987  cdeqbox  25029  cdeqnxt  25030  cdequnt  25031
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 2975
  Copyright terms: Public domain W3C validator