Metamath Proof Explorer

Theorem 3jcadALT

Description: Alternate proof of 3jcad . (Contributed by Hongxiu Chen, 29-Jun-2025) (Proof modification is discouraged.) Use 3jcad instead. (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		3jcadALT.1	$⊢ φ \to (ψ \to χ)$
2		3jcadALT.2	$⊢ φ \to (ψ \to θ)$
3		3jcadALT.3	$⊢ φ \to (ψ \to τ)$
4	1 2	jcad	$⊢ φ \to (ψ \to (χ \land θ))$
5	4 3	jcad	$⊢ φ \to (ψ \to ((χ \land θ) \land τ))$
6		df-3an	$⊢ (χ \land θ \land τ) \leftrightarrow ((χ \land θ) \land τ)$
7	5 6	imbitrrdi	$⊢ φ \to (ψ \to (χ \land θ \land τ))$