Metamath Proof Explorer

Theorem iscnrm3lem4

Description: Lemma for iscnrm3lem5 and iscnrm3r . (Contributed by Zhi Wang, 4-Sep-2024)

Ref Expression
Hypotheses iscnrm3lem4.1 ⊢ η → ψ → ζ
iscnrm3lem4.2 ⊢ φ ∧ χ ∧ θ → η
iscnrm3lem4.3 ⊢ φ ∧ χ ∧ θ → ζ → τ
Assertion iscnrm3lem4 ⊢ φ → ψ → χ → θ → τ

Proof

Step Hyp Ref Expression
1 iscnrm3lem4.1 ⊢ η → ψ → ζ
2 iscnrm3lem4.2 ⊢ φ ∧ χ ∧ θ → η
3 iscnrm3lem4.3 ⊢ φ ∧ χ ∧ θ → ζ → τ
4 4anpull2 ⊢ φ ∧ ψ ∧ χ ∧ θ ↔ φ ∧ χ ∧ θ ∧ ψ
5 2 1 syl ⊢ φ ∧ χ ∧ θ → ψ → ζ
6 5 3 syld ⊢ φ ∧ χ ∧ θ → ψ → τ
7 6 imp ⊢ φ ∧ χ ∧ θ ∧ ψ → τ
8 4 7 sylbi ⊢ φ ∧ ψ ∧ χ ∧ θ → τ
9 8 exp43 ⊢ φ → ψ → χ → θ → τ