Mathbox for Anthony Hart 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > Mathboxes > tbax3  Structured version Unicode version 
Description: The third of three axioms
in the TarskiBernays axiom system.
This axiom, along with axmp 8, tbax1 26120, and tbax2 26121, can be used to derive any theorem or rule that uses only . (Contributed by Anthony Hart, 16Aug2011.) (Proof modification is discouraged.) (New usage is discouraged.) 
Ref  Expression 

tbax3 
Step  Hyp  Ref  Expression 

1  peirce 174  1 
Colors of variables: wff set class 
Syntax hints: wi 4 
This theorem is referenced by: re1ax2lem 26124 re1ax2 26125 
This theorem was proved from axioms: ax1 5 ax2 6 ax3 7 axmp 8 
Copyright terms: Public domain  W3C validator 