Mathbox for BJ 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > Mathboxes > pm4.81ALT  Structured version Unicode version 
Description: Alternate proof of pm4.81 367. (Contributed by BJ, 30Mar2020.) (Proof modification is discouraged.) (New usage is discouraged.) 
Ref  Expression 

pm4.81ALT 
Step  Hyp  Ref  Expression 

1  pm2.18 113  . 2  
2  ax1 6  . 2  
3  1, 2  impbii 190  1 
Colors of variables: wff setvar class 
Syntax hints: wn 3 wi 4 wb 187 
This theorem was proved from axioms: axmp 5 ax1 6 ax2 7 ax3 8 
This theorem depends on definitions: dfbi 188 
This theorem is referenced by: (None) 
Copyright terms: Public domain  W3C validator 