Theorem iscnrm3lem4 46118

Description: Lemma for iscnrm3lem5 46119 and iscnrm3r 46130. (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 46117	. . 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 406	. . 3 ⊢ (((𝜑 ∧ 𝜒 ∧ 𝜃) ∧ 𝜓) → 𝜏)
8	1, 7	sylbi 216	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏)
9	8	exp43 436	1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 206  df-an 396  df-3an 1087

This theorem is referenced by:  iscnrm3lem5  46119  iscnrm3r  46130