Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > stoic4a  Unicode version 
Description: Stoic logic Thema 4
version a.
Statement T4 of [Bobzien] p. 117 shows a reconstructed version of Stoic logic thema 4: "When from two assertibles a third follows, and from the third and one (or both) of the two and one (or more) external assertible(s) another follows, then this other follows from the first two and the external(s)." We use to represent the "external" assertibles. This is version a, which is without the phrase "or both"; see stoic4b 1611 for the version with the phrase "or both". (Contributed by David A. Wheeler, 17Feb2019.) 
Ref  Expression 

stoic4a.1  
stoic4a.2 
Ref  Expression 

stoic4a 
Step  Hyp  Ref  Expression 

1  stoic4a.1  . . 3  
2  1  3adant3 1016  . 2 
3  simp1 996  . 2  
4  simp3 998  . 2  
5  stoic4a.2  . 2  
6  2, 3, 4, 5  syl3anc 1228  1 
Colors of variables: wff setvar class 
Syntax hints: > wi 4 /\ wa 369
/\ w3a 973 
This theorem was proved from axioms: axmp 5 ax1 6 ax2 7 ax3 8 
This theorem depends on definitions: dfbi 185 dfan 371 df3an 975 
Copyright terms: Public domain  W3C validator 