This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜃 ) → 𝜏 )