Metamath Proof Explorer


Theorem iscnrm3lem3

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

Ref Expression
Assertion iscnrm3lem3 ( ( ( 𝜑𝜓 ) ∧ ( 𝜒𝜃 ) ) ↔ ( ( 𝜑𝜒𝜃 ) ∧ 𝜓 ) )

Proof

Step Hyp Ref Expression
1 anass ( ( ( 𝜑𝜓 ) ∧ ( 𝜒𝜃 ) ) ↔ ( 𝜑 ∧ ( 𝜓 ∧ ( 𝜒𝜃 ) ) ) )
2 anass ( ( ( 𝜑 ∧ ( 𝜒𝜃 ) ) ∧ 𝜓 ) ↔ ( 𝜑 ∧ ( ( 𝜒𝜃 ) ∧ 𝜓 ) ) )
3 3anass ( ( 𝜑𝜒𝜃 ) ↔ ( 𝜑 ∧ ( 𝜒𝜃 ) ) )
4 3 anbi1i ( ( ( 𝜑𝜒𝜃 ) ∧ 𝜓 ) ↔ ( ( 𝜑 ∧ ( 𝜒𝜃 ) ) ∧ 𝜓 ) )
5 ancom ( ( 𝜓 ∧ ( 𝜒𝜃 ) ) ↔ ( ( 𝜒𝜃 ) ∧ 𝜓 ) )
6 5 anbi2i ( ( 𝜑 ∧ ( 𝜓 ∧ ( 𝜒𝜃 ) ) ) ↔ ( 𝜑 ∧ ( ( 𝜒𝜃 ) ∧ 𝜓 ) ) )
7 2 4 6 3bitr4ri ( ( 𝜑 ∧ ( 𝜓 ∧ ( 𝜒𝜃 ) ) ) ↔ ( ( 𝜑𝜒𝜃 ) ∧ 𝜓 ) )
8 1 7 bitri ( ( ( 𝜑𝜓 ) ∧ ( 𝜒𝜃 ) ) ↔ ( ( 𝜑𝜒𝜃 ) ∧ 𝜓 ) )