This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )