Metamath Proof Explorer

Theorem pm10.541

Description: Theorem *10.541 in WhiteheadRussell p. 155. (Contributed by Andrew Salmon, 24-May-2011)

Ref Expression
Assertion pm10.541 
|- ( A. x ( ph -> ( ch \/ ps ) ) <-> ( ch \/ A. x ( ph -> ps ) ) )

Proof

Step Hyp Ref Expression
1 bi2.04 
 |-  ( ( ph -> ( -. ch -> ps ) ) <-> ( -. ch -> ( ph -> ps ) ) )
2 1 albii 
 |-  ( A. x ( ph -> ( -. ch -> ps ) ) <-> A. x ( -. ch -> ( ph -> ps ) ) )
3 19.21v 
 |-  ( A. x ( -. ch -> ( ph -> ps ) ) <-> ( -. ch -> A. x ( ph -> ps ) ) )
4 2 3 bitri 
 |-  ( A. x ( ph -> ( -. ch -> ps ) ) <-> ( -. ch -> A. x ( ph -> ps ) ) )
5 df-or 
 |-  ( ( ch \/ ps ) <-> ( -. ch -> ps ) )
6 5 imbi2i 
 |-  ( ( ph -> ( ch \/ ps ) ) <-> ( ph -> ( -. ch -> ps ) ) )
7 6 albii 
 |-  ( A. x ( ph -> ( ch \/ ps ) ) <-> A. x ( ph -> ( -. ch -> ps ) ) )
8 df-or 
 |-  ( ( ch \/ A. x ( ph -> ps ) ) <-> ( -. ch -> A. x ( ph -> ps ) ) )
9 4 7 8 3bitr4i 
 |-  ( A. x ( ph -> ( ch \/ ps ) ) <-> ( ch \/ A. x ( ph -> ps ) ) )