Mathbox for David A. Wheeler 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > Mathboxes > 19.8ad  Unicode version 
Description: If a wff is true, it is true for at least one instance. Deductive form of 19.8a 1758. (Contributed by DAW, 13Feb2017.) 
Ref  Expression 

19.8ad.1 
Ref  Expression 

19.8ad 
Step  Hyp  Ref  Expression 

1  19.8ad.1  . 2  
2  19.8a 1758  . 2  
3  1, 2  syl 17  1 
Colors of variables: wff set class 
Syntax hints: wi 6 wex 1537 
This theorem was proved from axioms: ax1 7 ax2 8 ax3 9 axmp 10 ax4 1692 
This theorem depends on definitions: dfbi 179 dfex 1538 
Copyright terms: Public domain  W3C validator 