Metamath Proof Explorer


Theorem stoic4b

Description: Stoic logic Thema 4 version b. This is version b, which is with the phrase "or both". See stoic4a for more information. (Contributed by David A. Wheeler, 17-Feb-2019)

Ref Expression
Hypotheses stoic4b.1 φψχ
stoic4b.2 χφψθτ
Assertion stoic4b φψθτ

Proof

Step Hyp Ref Expression
1 stoic4b.1 φψχ
2 stoic4b.2 χφψθτ
3 1 3adant3 φψθχ
4 simp1 φψθφ
5 simp2 φψθψ
6 simp3 φψθθ
7 3 4 5 6 2 syl31anc φψθτ