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

Metamath Proof Explorer

Theorem syl1111anc

Description: Four-hypothesis elimination deduction for an assertion with a singleton virtual hypothesis collection. Similar to syl112anc except the unification theorem uses left-nested conjunction. (Contributed by Alan Sare, 17-Oct-2017)

	Ref	Expression
Hypotheses	syl1111anc.1	⊢ ( 𝜑 → 𝜓 )
	syl1111anc.2	⊢ ( 𝜑 → 𝜒 )
	syl1111anc.3	⊢ ( 𝜑 → 𝜃 )
	syl1111anc.4	⊢ ( 𝜑 → 𝜏 )
	syl1111anc.5	⊢ ( ( ( ( 𝜓 ∧ 𝜒 ) ∧ 𝜃 ) ∧ 𝜏 ) → 𝜂 )
Assertion	syl1111anc	⊢ ( 𝜑 → 𝜂 )

Proof

Step	Hyp	Ref	Expression
1		syl1111anc.1	⊢ ( 𝜑 → 𝜓 )
2		syl1111anc.2	⊢ ( 𝜑 → 𝜒 )
3		syl1111anc.3	⊢ ( 𝜑 → 𝜃 )
4		syl1111anc.4	⊢ ( 𝜑 → 𝜏 )
5		syl1111anc.5	⊢ ( ( ( ( 𝜓 ∧ 𝜒 ) ∧ 𝜃 ) ∧ 𝜏 ) → 𝜂 )
6	1 2	jca	⊢ ( 𝜑 → ( 𝜓 ∧ 𝜒 ) )
7	6 3 4 5	syl21anc	⊢ ( 𝜑 → 𝜂 )