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

Metamath Proof Explorer

Theorem syl21anbrc

Description: Syllogism inference. (Contributed by Peter Mazsa, 18-Sep-2022)

	Ref	Expression
Hypotheses	syl21anbrc.1	$⊢ φ \to ψ$
	syl21anbrc.2	$⊢ φ \to χ$
	syl21anbrc.3	$⊢ φ \to θ$
	syl21anbrc.4	$⊢ τ \leftrightarrow ((ψ \land χ) \land θ)$
Assertion	syl21anbrc	$⊢ φ \to τ$

Step	Hyp	Ref	Expression
1		syl21anbrc.1	$⊢ φ \to ψ$
2		syl21anbrc.2	$⊢ φ \to χ$
3		syl21anbrc.3	$⊢ φ \to θ$
4		syl21anbrc.4	$⊢ τ \leftrightarrow ((ψ \land χ) \land θ)$
5	1 2 3	jca31	$⊢ φ \to ((ψ \land χ) \land θ)$
6	5 4	sylibr	$⊢ φ \to τ$