Step |
Hyp |
Ref |
Expression |
1 |
|
sbcan |
|- ( [. A / x ]. ( ( ph /\ ps ) /\ ch ) <-> ( [. A / x ]. ( ph /\ ps ) /\ [. A / x ]. ch ) ) |
2 |
|
sbcan |
|- ( [. A / x ]. ( ph /\ ps ) <-> ( [. A / x ]. ph /\ [. A / x ]. ps ) ) |
3 |
1 2
|
bianbi |
|- ( [. A / x ]. ( ( ph /\ ps ) /\ ch ) <-> ( ( [. A / x ]. ph /\ [. A / x ]. ps ) /\ [. A / x ]. ch ) ) |
4 |
|
df-3an |
|- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) ) |
5 |
4
|
sbcbii |
|- ( [. A / x ]. ( ph /\ ps /\ ch ) <-> [. A / x ]. ( ( ph /\ ps ) /\ ch ) ) |
6 |
|
df-3an |
|- ( ( [. A / x ]. ph /\ [. A / x ]. ps /\ [. A / x ]. ch ) <-> ( ( [. A / x ]. ph /\ [. A / x ]. ps ) /\ [. A / x ]. ch ) ) |
7 |
3 5 6
|
3bitr4i |
|- ( [. A / x ]. ( ph /\ ps /\ ch ) <-> ( [. A / x ]. ph /\ [. A / x ]. ps /\ [. A / x ]. ch ) ) |