Metamath Proof Explorer

Theorem dedth4h

Description: Weak deduction theorem eliminating four hypotheses. See comments in dedth2h . (Contributed by NM, 16-May-1999)

Ref Expression
Hypotheses dedth4h.1
|- ( A = if ( ph , A , R ) -> ( ta <-> et ) )
dedth4h.2
|- ( B = if ( ps , B , S ) -> ( et <-> ze ) )
dedth4h.3
|- ( C = if ( ch , C , F ) -> ( ze <-> si ) )
dedth4h.4
|- ( D = if ( th , D , G ) -> ( si <-> rh ) )
dedth4h.5
|- rh
Assertion dedth4h
|- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) -> ta )

Proof

Step Hyp Ref Expression
1 dedth4h.1
|-  ( A = if ( ph , A , R ) -> ( ta <-> et ) )
2 dedth4h.2
|-  ( B = if ( ps , B , S ) -> ( et <-> ze ) )
3 dedth4h.3
|-  ( C = if ( ch , C , F ) -> ( ze <-> si ) )
4 dedth4h.4
|-  ( D = if ( th , D , G ) -> ( si <-> rh ) )
5 dedth4h.5
|-  rh
6 1 imbi2d
|-  ( A = if ( ph , A , R ) -> ( ( ( ch /\ th ) -> ta ) <-> ( ( ch /\ th ) -> et ) ) )
7 2 imbi2d
|-  ( B = if ( ps , B , S ) -> ( ( ( ch /\ th ) -> et ) <-> ( ( ch /\ th ) -> ze ) ) )
8 3 4 5 dedth2h
|-  ( ( ch /\ th ) -> ze )
9 6 7 8 dedth2h
|-  ( ( ph /\ ps ) -> ( ( ch /\ th ) -> ta ) )
10 9 imp
|-  ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) -> ta )