# 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 ${⊢}\left({\phi }\wedge {\psi }\right)\to {\chi }$
stoic4b.2 ${⊢}\left(\left({\chi }\wedge {\phi }\wedge {\psi }\right)\wedge {\theta }\right)\to {\tau }$
Assertion stoic4b ${⊢}\left({\phi }\wedge {\psi }\wedge {\theta }\right)\to {\tau }$

### Proof

Step Hyp Ref Expression
1 stoic4b.1 ${⊢}\left({\phi }\wedge {\psi }\right)\to {\chi }$
2 stoic4b.2 ${⊢}\left(\left({\chi }\wedge {\phi }\wedge {\psi }\right)\wedge {\theta }\right)\to {\tau }$
3 1 3adant3 ${⊢}\left({\phi }\wedge {\psi }\wedge {\theta }\right)\to {\chi }$
4 simp1 ${⊢}\left({\phi }\wedge {\psi }\wedge {\theta }\right)\to {\phi }$
5 simp2 ${⊢}\left({\phi }\wedge {\psi }\wedge {\theta }\right)\to {\psi }$
6 simp3 ${⊢}\left({\phi }\wedge {\psi }\wedge {\theta }\right)\to {\theta }$
7 3 4 5 6 2 syl31anc ${⊢}\left({\phi }\wedge {\psi }\wedge {\theta }\right)\to {\tau }$