Metamath Proof Explorer

Theorem dedlemb

Description: Lemma for weak deduction theorem. See also ifpfal . (Contributed by NM, 15-May-1999) (Proof shortened by Andrew Salmon, 7-May-2011)

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

Proof

Step Hyp Ref Expression
1 olc 
 |-  ( ( ch /\ -. ph ) -> ( ( ps /\ ph ) \/ ( ch /\ -. ph ) ) )
2 1 expcom 
 |-  ( -. ph -> ( ch -> ( ( ps /\ ph ) \/ ( ch /\ -. ph ) ) ) )
3 pm2.21 
 |-  ( -. ph -> ( ph -> ch ) )
4 3 adantld 
 |-  ( -. ph -> ( ( ps /\ ph ) -> ch ) )
5 simpl 
 |-  ( ( ch /\ -. ph ) -> ch )
6 5 a1i 
 |-  ( -. ph -> ( ( ch /\ -. ph ) -> ch ) )
7 4 6 jaod 
 |-  ( -. ph -> ( ( ( ps /\ ph ) \/ ( ch /\ -. ph ) ) -> ch ) )
8 2 7 impbid 
 |-  ( -. ph -> ( ch <-> ( ( ps /\ ph ) \/ ( ch /\ -. ph ) ) ) )