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 ηφψηχ