Step |
Hyp |
Ref |
Expression |
1 |
|
df-3an |
|- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) ) |
2 |
1
|
sbbii |
|- ( [ y / x ] ( ph /\ ps /\ ch ) <-> [ y / x ] ( ( ph /\ ps ) /\ ch ) ) |
3 |
|
sban |
|- ( [ y / x ] ( ( ph /\ ps ) /\ ch ) <-> ( [ y / x ] ( ph /\ ps ) /\ [ y / x ] ch ) ) |
4 |
|
sban |
|- ( [ y / x ] ( ph /\ ps ) <-> ( [ y / x ] ph /\ [ y / x ] ps ) ) |
5 |
4
|
anbi1i |
|- ( ( [ y / x ] ( ph /\ ps ) /\ [ y / x ] ch ) <-> ( ( [ y / x ] ph /\ [ y / x ] ps ) /\ [ y / x ] ch ) ) |
6 |
|
df-3an |
|- ( ( [ y / x ] ph /\ [ y / x ] ps /\ [ y / x ] ch ) <-> ( ( [ y / x ] ph /\ [ y / x ] ps ) /\ [ y / x ] ch ) ) |
7 |
5 6
|
bitr4i |
|- ( ( [ y / x ] ( ph /\ ps ) /\ [ y / x ] ch ) <-> ( [ y / x ] ph /\ [ y / x ] ps /\ [ y / x ] ch ) ) |
8 |
2 3 7
|
3bitri |
|- ( [ y / x ] ( ph /\ ps /\ ch ) <-> ( [ y / x ] ph /\ [ y / x ] ps /\ [ y / x ] ch ) ) |