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 φ ψ θ τ


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 φ ψ θ τ