Description: An inference to merge two lists of conjuncts. (Contributed by Peter Mazsa, 24-Sep-2022)
Ref | Expression | ||
---|---|---|---|
Hypothesis | bianass.1 | |- ( ph <-> ( ps /\ ch ) ) |
|
Assertion | bianassc | |- ( ( et /\ ph ) <-> ( ( ps /\ et ) /\ ch ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bianass.1 | |- ( ph <-> ( ps /\ ch ) ) |
|
2 | 1 | bianass | |- ( ( et /\ ph ) <-> ( ( et /\ ps ) /\ ch ) ) |
3 | ancom | |- ( ( et /\ ps ) <-> ( ps /\ et ) ) |
|
4 | 3 | anbi1i | |- ( ( ( et /\ ps ) /\ ch ) <-> ( ( ps /\ et ) /\ ch ) ) |
5 | 2 4 | bitri | |- ( ( et /\ ph ) <-> ( ( ps /\ et ) /\ ch ) ) |