Metamath Proof Explorer

Theorem bianassc

Description: An inference to merge two lists of conjuncts. (Contributed by Peter Mazsa, 24-Sep-2022)

Ref Expression
Hypothesis bianass.1 ⊢ φ ↔ ψ ∧ χ
Assertion bianassc ⊢ η ∧ φ ↔ ψ ∧ η ∧ χ

Proof

Step Hyp Ref Expression
1 bianass.1 ⊢ φ ↔ ψ ∧ χ
2 1 bianass ⊢ η ∧ φ ↔ η ∧ ψ ∧ χ
3 ancom ⊢ η ∧ ψ ↔ ψ ∧ η
4 3 anbi1i ⊢ η ∧ ψ ∧ χ ↔ ψ ∧ η ∧ χ
5 2 4 bitri ⊢ η ∧ φ ↔ ψ ∧ η ∧ χ