Theorem iscnrm3lem4 45682

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

Hypotheses

Ref	Expression
iscnrm3lem4.1	⊢ (𝜂 → (𝜓 → 𝜁))
iscnrm3lem4.2	⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜂)
iscnrm3lem4.3	⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → (𝜁 → 𝜏))

Assertion

Ref	Expression
iscnrm3lem4	⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Proof of Theorem iscnrm3lem4

Step	Hyp	Ref	Expression
1		iscnrm3lem3 45681	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜒 ∧ 𝜃) ∧ 𝜓))
2		iscnrm3lem4.2	. . . . . 6 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜂)
3		iscnrm3lem4.1	. . . . . 6 ⊢ (𝜂 → (𝜓 → 𝜁))
4	2, 3	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → (𝜓 → 𝜁))
5		iscnrm3lem4.3	. . . . 5 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → (𝜁 → 𝜏))
6	4, 5	syld 47	. . . 4 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → (𝜓 → 𝜏))
7	6	imp 410	. . 3 ⊢ (((𝜑 ∧ 𝜒 ∧ 𝜃) ∧ 𝜓) → 𝜏)
8	1, 7	sylbi 220	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏)
9	8	exp43 440	1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1087

This theorem is referenced by:  iscnrm3lem5  45683  iscnrm3r  45694