Description: Weak deduction theorem eliminating two hypotheses. This theorem is simpler to use than dedth2v but requires that each hypothesis have exactly one class variable. See also comments in dedth . (Contributed by NM, 15May1999)
Ref  Expression  

Hypotheses  dedth2h.1   ( A = if ( ph , A , C ) > ( ch <> th ) ) 

dedth2h.2   ( B = if ( ps , B , D ) > ( th <> ta ) ) 

dedth2h.3   ta 

Assertion  dedth2h   ( ( ph /\ ps ) > ch ) 
Step  Hyp  Ref  Expression 

1  dedth2h.1   ( A = if ( ph , A , C ) > ( ch <> th ) ) 

2  dedth2h.2   ( B = if ( ps , B , D ) > ( th <> ta ) ) 

3  dedth2h.3   ta 

4  1  imbi2d   ( A = if ( ph , A , C ) > ( ( ps > ch ) <> ( ps > th ) ) ) 
5  2 3  dedth   ( ps > th ) 
6  4 5  dedth   ( ph > ( ps > ch ) ) 
7  6  imp   ( ( ph /\ ps ) > ch ) 