Metamath Proof Explorer

Theorem pm4.87

Description: Theorem *4.87 of WhiteheadRussell p. 122. (Contributed by NM, 3-Jan-2005) (Proof shortened by Eric Schmidt, 26-Oct-2006)

Ref Expression
Assertion pm4.87 
|- ( ( ( ( ( ph /\ ps ) -> ch ) <-> ( ph -> ( ps -> ch ) ) ) /\ ( ( ph -> ( ps -> ch ) ) <-> ( ps -> ( ph -> ch ) ) ) ) /\ ( ( ps -> ( ph -> ch ) ) <-> ( ( ps /\ ph ) -> ch ) ) )

Proof

Step Hyp Ref Expression
1 impexp 
 |-  ( ( ( ph /\ ps ) -> ch ) <-> ( ph -> ( ps -> ch ) ) )
2 bi2.04 
 |-  ( ( ph -> ( ps -> ch ) ) <-> ( ps -> ( ph -> ch ) ) )
3 1 2 pm3.2i 
 |-  ( ( ( ( ph /\ ps ) -> ch ) <-> ( ph -> ( ps -> ch ) ) ) /\ ( ( ph -> ( ps -> ch ) ) <-> ( ps -> ( ph -> ch ) ) ) )
4 impexp 
 |-  ( ( ( ps /\ ph ) -> ch ) <-> ( ps -> ( ph -> ch ) ) )
5 4 bicomi 
 |-  ( ( ps -> ( ph -> ch ) ) <-> ( ( ps /\ ph ) -> ch ) )
6 3 5 pm3.2i 
 |-  ( ( ( ( ( ph /\ ps ) -> ch ) <-> ( ph -> ( ps -> ch ) ) ) /\ ( ( ph -> ( ps -> ch ) ) <-> ( ps -> ( ph -> ch ) ) ) ) /\ ( ( ps -> ( ph -> ch ) ) <-> ( ( ps /\ ph ) -> ch ) ) )