Metamath Proof Explorer

Theorem imor

Description: Implication in terms of disjunction. Theorem *4.6 of WhiteheadRussell p. 120. (Contributed by NM, 3-Jan-1993)

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

Proof

Step Hyp Ref Expression
1 notnotb 
 |-  ( ph <-> -. -. ph )
2 1 imbi1i 
 |-  ( ( ph -> ps ) <-> ( -. -. ph -> ps ) )
3 df-or 
 |-  ( ( -. ph \/ ps ) <-> ( -. -. ph -> ps ) )
4 2 3 bitr4i 
 |-  ( ( ph -> ps ) <-> ( -. ph \/ ps ) )