Theorem dfor2 199

Description: Logical 'or' expressed in terms of implication only. Theorem *5.25 of [WhiteheadRussell] p. 124.

Assertion

Ref	Expression
dfor2	|- ((ph \/ ps) <-> ((ph -> ps) -> ps))

Proof of Theorem dfor2

Step	Hyp	Ref	Expression
1		df-or 197	. 2 |- ((ph \/ ps) <-> (-. ph -> ps))
2		pm2.61 109	. . . 4 |- ((ph -> ps) -> ((-. ph -> ps) -> ps))
3	2	com12 13	. . 3 |- ((-. ph -> ps) -> ((ph -> ps) -> ps))
4		pm2.21 71	. . . 4 |- (-. ph -> (ph -> ps))
5	4	syl4 19	. . 3 |- (((ph -> ps) -> ps) -> (-. ph -> ps))
6	3, 5	impbi 139	. 2 |- ((-. ph -> ps) <-> ((ph -> ps) -> ps))
7	1, 6	bitr 151	1 |- ((ph \/ ps) <-> ((ph -> ps) -> ps))

Syntax hints:  -. wn 1   -> wi 2   <-> wb 127   \/ wo 195

This theorem is referenced by:  pm2.62 210

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-or 197

metamath.org