Description: /\ -manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | bnj887.1 | ⊢ ( 𝜑 ↔ 𝜑′ ) | |
bnj887.2 | ⊢ ( 𝜓 ↔ 𝜓′ ) | ||
bnj887.3 | ⊢ ( 𝜒 ↔ 𝜒′ ) | ||
bnj887.4 | ⊢ ( 𝜃 ↔ 𝜃′ ) | ||
Assertion | bnj887 | ⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃 ) ↔ ( 𝜑′ ∧ 𝜓′ ∧ 𝜒′ ∧ 𝜃′ ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bnj887.1 | ⊢ ( 𝜑 ↔ 𝜑′ ) | |
2 | bnj887.2 | ⊢ ( 𝜓 ↔ 𝜓′ ) | |
3 | bnj887.3 | ⊢ ( 𝜒 ↔ 𝜒′ ) | |
4 | bnj887.4 | ⊢ ( 𝜃 ↔ 𝜃′ ) | |
5 | 1 2 3 | 3anbi123i | ⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ↔ ( 𝜑′ ∧ 𝜓′ ∧ 𝜒′ ) ) |
6 | 5 4 | anbi12i | ⊢ ( ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ∧ 𝜃 ) ↔ ( ( 𝜑′ ∧ 𝜓′ ∧ 𝜒′ ) ∧ 𝜃′ ) ) |
7 | df-bnj17 | ⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃 ) ↔ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ∧ 𝜃 ) ) | |
8 | df-bnj17 | ⊢ ( ( 𝜑′ ∧ 𝜓′ ∧ 𝜒′ ∧ 𝜃′ ) ↔ ( ( 𝜑′ ∧ 𝜓′ ∧ 𝜒′ ) ∧ 𝜃′ ) ) | |
9 | 6 7 8 | 3bitr4i | ⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃 ) ↔ ( 𝜑′ ∧ 𝜓′ ∧ 𝜒′ ∧ 𝜃′ ) ) |