Metamath Proof Explorer
Description: A contradiction implies anything. Equality/inequality deduction form.
(Contributed by David Moews, 28Feb2017)


Ref 
Expression 

Hypotheses 
pm2.21ddne.1 
 ( ph > A = B ) 


pm2.21ddne.2 
 ( ph > A =/= B ) 

Assertion 
pm2.21ddne 
 ( ph > ps ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

pm2.21ddne.1 
 ( ph > A = B ) 
2 

pm2.21ddne.2 
 ( ph > A =/= B ) 
3 
2

neneqd 
 ( ph > . A = B ) 
4 
1 3

pm2.21dd 
 ( ph > ps ) 