Theorem zlteq1d ≪ | index | src | ≫

theorem zlteq1d (_G: wff) (_m1 _m2 n: nat):
  $ _G -> _m1 = _m2 $ >
  $ _G -> (_m1  _m2 
    

      

        
Step
Hyp
Ref
Expression
        

          
1
          

          
hyp _h
          
_G -> _m1 = _m2
        
        

          
2
          

          
eqidd
          
_G -> n = n
        
        

          
3
          
1, 2
          
zlteqd
          
_G -> (_m1 <Z n <-> _m2 <Z n)
        
      
    
    
Axiom use
    axs_prop_calc
     (ax_1,
      ax_2,
      ax_3,
      ax_mp,
      itru),
    axs_pred_calc
     (ax_gen,
      ax_4,
      ax_5,
      ax_6,
      ax_7,
      ax_10,
      ax_11,
      ax_12),
    axs_set
     (elab,
      ax_8),
    axs_the
     (theid,
      the0),
    axs_peano
     (peano2,
      addeq,
      muleq)