Metamath Proof Explorer

Theorem prtlem70

Description: Lemma for prter3 : a rearrangement of conjuncts. (Contributed by Rodolfo Medina, 20-Oct-2010)

Ref Expression
Assertion prtlem70 ( ( ( ( 𝜓 ∧ 𝜂 ) ∧ ( ( 𝜑 ∧ 𝜃 ) ∧ ( 𝜒 ∧ 𝜏 ) ) ) ∧ 𝜑 ) ↔ ( ( 𝜑 ∧ ( 𝜓 ∧ ( 𝜒 ∧ ( 𝜃 ∧ 𝜏 ) ) ) ) ∧ 𝜂 ) )

Proof

Step Hyp Ref Expression
1 anass ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝜑 ∧ 𝜃 ) ) ∧ ( 𝜒 ∧ 𝜏 ) ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∧ ( ( 𝜑 ∧ 𝜃 ) ∧ ( 𝜒 ∧ 𝜏 ) ) ) )
2 1 anbi1i ⊢ ( ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝜑 ∧ 𝜃 ) ) ∧ ( 𝜒 ∧ 𝜏 ) ) ∧ 𝜂 ) ↔ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( ( 𝜑 ∧ 𝜃 ) ∧ ( 𝜒 ∧ 𝜏 ) ) ) ∧ 𝜂 ) )
3 anandi ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜃 ) ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝜑 ∧ 𝜃 ) ) )
4 3 anbi1i ⊢ ( ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜃 ) ) ∧ ( 𝜒 ∧ 𝜏 ) ) ↔ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝜑 ∧ 𝜃 ) ) ∧ ( 𝜒 ∧ 𝜏 ) ) )
5 4 anbi1i ⊢ ( ( ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜃 ) ) ∧ ( 𝜒 ∧ 𝜏 ) ) ∧ 𝜂 ) ↔ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝜑 ∧ 𝜃 ) ) ∧ ( 𝜒 ∧ 𝜏 ) ) ∧ 𝜂 ) )
6 anass ⊢ ( ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜂 ) ) ∧ ( ( 𝜑 ∧ 𝜃 ) ∧ ( 𝜒 ∧ 𝜏 ) ) ) ↔ ( 𝜑 ∧ ( ( 𝜓 ∧ 𝜂 ) ∧ ( ( 𝜑 ∧ 𝜃 ) ∧ ( 𝜒 ∧ 𝜏 ) ) ) ) )
7 anass ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜂 ) ↔ ( 𝜑 ∧ ( 𝜓 ∧ 𝜂 ) ) )
8 7 anbi1i ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜂 ) ∧ ( ( 𝜑 ∧ 𝜃 ) ∧ ( 𝜒 ∧ 𝜏 ) ) ) ↔ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜂 ) ) ∧ ( ( 𝜑 ∧ 𝜃 ) ∧ ( 𝜒 ∧ 𝜏 ) ) ) )
9 ancom ⊢ ( ( ( ( 𝜓 ∧ 𝜂 ) ∧ ( ( 𝜑 ∧ 𝜃 ) ∧ ( 𝜒 ∧ 𝜏 ) ) ) ∧ 𝜑 ) ↔ ( 𝜑 ∧ ( ( 𝜓 ∧ 𝜂 ) ∧ ( ( 𝜑 ∧ 𝜃 ) ∧ ( 𝜒 ∧ 𝜏 ) ) ) ) )
10 6 8 9 3bitr4ri ⊢ ( ( ( ( 𝜓 ∧ 𝜂 ) ∧ ( ( 𝜑 ∧ 𝜃 ) ∧ ( 𝜒 ∧ 𝜏 ) ) ) ∧ 𝜑 ) ↔ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜂 ) ∧ ( ( 𝜑 ∧ 𝜃 ) ∧ ( 𝜒 ∧ 𝜏 ) ) ) )
11 ancom ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜂 ) ↔ ( 𝜂 ∧ ( 𝜑 ∧ 𝜓 ) ) )
12 11 anbi1i ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜂 ) ∧ ( ( 𝜑 ∧ 𝜃 ) ∧ ( 𝜒 ∧ 𝜏 ) ) ) ↔ ( ( 𝜂 ∧ ( 𝜑 ∧ 𝜓 ) ) ∧ ( ( 𝜑 ∧ 𝜃 ) ∧ ( 𝜒 ∧ 𝜏 ) ) ) )
13 anass ⊢ ( ( ( 𝜂 ∧ ( 𝜑 ∧ 𝜓 ) ) ∧ ( ( 𝜑 ∧ 𝜃 ) ∧ ( 𝜒 ∧ 𝜏 ) ) ) ↔ ( 𝜂 ∧ ( ( 𝜑 ∧ 𝜓 ) ∧ ( ( 𝜑 ∧ 𝜃 ) ∧ ( 𝜒 ∧ 𝜏 ) ) ) ) )
14 ancom ⊢ ( ( 𝜂 ∧ ( ( 𝜑 ∧ 𝜓 ) ∧ ( ( 𝜑 ∧ 𝜃 ) ∧ ( 𝜒 ∧ 𝜏 ) ) ) ) ↔ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( ( 𝜑 ∧ 𝜃 ) ∧ ( 𝜒 ∧ 𝜏 ) ) ) ∧ 𝜂 ) )
15 13 14 bitri ⊢ ( ( ( 𝜂 ∧ ( 𝜑 ∧ 𝜓 ) ) ∧ ( ( 𝜑 ∧ 𝜃 ) ∧ ( 𝜒 ∧ 𝜏 ) ) ) ↔ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( ( 𝜑 ∧ 𝜃 ) ∧ ( 𝜒 ∧ 𝜏 ) ) ) ∧ 𝜂 ) )
16 10 12 15 3bitri ⊢ ( ( ( ( 𝜓 ∧ 𝜂 ) ∧ ( ( 𝜑 ∧ 𝜃 ) ∧ ( 𝜒 ∧ 𝜏 ) ) ) ∧ 𝜑 ) ↔ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( ( 𝜑 ∧ 𝜃 ) ∧ ( 𝜒 ∧ 𝜏 ) ) ) ∧ 𝜂 ) )
17 2 5 16 3bitr4ri ⊢ ( ( ( ( 𝜓 ∧ 𝜂 ) ∧ ( ( 𝜑 ∧ 𝜃 ) ∧ ( 𝜒 ∧ 𝜏 ) ) ) ∧ 𝜑 ) ↔ ( ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜃 ) ) ∧ ( 𝜒 ∧ 𝜏 ) ) ∧ 𝜂 ) )
18 anass ⊢ ( ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜃 ) ) ∧ ( 𝜒 ∧ 𝜏 ) ) ↔ ( 𝜑 ∧ ( ( 𝜓 ∧ 𝜃 ) ∧ ( 𝜒 ∧ 𝜏 ) ) ) )
19 18 anbi1i ⊢ ( ( ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜃 ) ) ∧ ( 𝜒 ∧ 𝜏 ) ) ∧ 𝜂 ) ↔ ( ( 𝜑 ∧ ( ( 𝜓 ∧ 𝜃 ) ∧ ( 𝜒 ∧ 𝜏 ) ) ) ∧ 𝜂 ) )
20 an4 ⊢ ( ( ( 𝜓 ∧ 𝜃 ) ∧ ( 𝜒 ∧ 𝜏 ) ) ↔ ( ( 𝜓 ∧ 𝜒 ) ∧ ( 𝜃 ∧ 𝜏 ) ) )
21 anass ⊢ ( ( ( 𝜓 ∧ 𝜒 ) ∧ ( 𝜃 ∧ 𝜏 ) ) ↔ ( 𝜓 ∧ ( 𝜒 ∧ ( 𝜃 ∧ 𝜏 ) ) ) )
22 20 21 bitri ⊢ ( ( ( 𝜓 ∧ 𝜃 ) ∧ ( 𝜒 ∧ 𝜏 ) ) ↔ ( 𝜓 ∧ ( 𝜒 ∧ ( 𝜃 ∧ 𝜏 ) ) ) )
23 22 anbi2i ⊢ ( ( 𝜑 ∧ ( ( 𝜓 ∧ 𝜃 ) ∧ ( 𝜒 ∧ 𝜏 ) ) ) ↔ ( 𝜑 ∧ ( 𝜓 ∧ ( 𝜒 ∧ ( 𝜃 ∧ 𝜏 ) ) ) ) )
24 23 anbi1i ⊢ ( ( ( 𝜑 ∧ ( ( 𝜓 ∧ 𝜃 ) ∧ ( 𝜒 ∧ 𝜏 ) ) ) ∧ 𝜂 ) ↔ ( ( 𝜑 ∧ ( 𝜓 ∧ ( 𝜒 ∧ ( 𝜃 ∧ 𝜏 ) ) ) ) ∧ 𝜂 ) )
25 17 19 24 3bitri ⊢ ( ( ( ( 𝜓 ∧ 𝜂 ) ∧ ( ( 𝜑 ∧ 𝜃 ) ∧ ( 𝜒 ∧ 𝜏 ) ) ) ∧ 𝜑 ) ↔ ( ( 𝜑 ∧ ( 𝜓 ∧ ( 𝜒 ∧ ( 𝜃 ∧ 𝜏 ) ) ) ) ∧ 𝜂 ) )