Theorem mtt 712

Description: Modus-tollens-like theorem.

Assertion

Ref	Expression
mtt	|- (-. ph -> (-. ps <-> (ps -> ph)))

Proof of Theorem mtt

Step	Hyp	Ref	Expression
1		pm2.21 76	. 2 |- (-. ps -> (ps -> ph))
2		con3 94	. . 3 |- ((ps -> ph) -> (-. ph -> -. ps))
3	2	com12 11	. 2 |- (-. ph -> ((ps -> ph) -> -. ps))
4	1, 3	impbid2 518	1 |- (-. ph -> (-. ps <-> (ps -> ph)))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146

This theorem is referenced by:  axpowndlem3 4951  axpownd 4953  large 10194

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

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain