Theorem iscnrm3lem4 50013

Description: Lemma for iscnrm3lem5 50014 and iscnrm3r 50025. (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		4anpull2 1382	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜒 ∧ 𝜃) ∧ 𝜓))
2		iscnrm3lem4.2	. . . . . 6 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜂)
3		iscnrm3lem4.1	. . . . . 6 ⊢ (𝜂 → (𝜓 → 𝜁))
4	2, 3	syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → (𝜓 → 𝜁))
5		iscnrm3lem4.3	. . . . 5 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → (𝜁 → 𝜏))
6	4, 5	syld 48	. . . 4 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → (𝜓 → 𝜏))
7	6	imp 412	. . 3 ⊢ (((𝜑 ∧ 𝜒 ∧ 𝜃) ∧ 𝜓) → 𝜏)
8	1, 7	sylbi 220	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏)
9	8	exp43 442	1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  iscnrm3lem5  50014  iscnrm3r  50025