Theorem con1i 96

Description: A contraposition inference.

Hypothesis

Ref	Expression
con1.a	|- (-. ph -> ps)

Assertion

Ref	Expression
con1i	|- (-. ps -> ph)

Proof of Theorem con1i

Step	Hyp	Ref	Expression
1		con1.a	. . 3 |- (-. ph -> ps)
2		negb 86	. . 3 |- (ps -> -. -. ps)
3	1, 2	syl 10	. 2 |- (-. ph -> -. -. ps)
4	3	a3i 74	1 |- (-. ps -> ph)

Syntax hints:  -. wn 2   -> wi 3

This theorem is referenced by:  con3i 98  pm2.24i 104  mt3 112  nsyl2 118  nsyl4 120  pm3.26im 139  pm3.27im 140  con1bii 220  pm3.13 317  pm5.15 665  ax5o 973  hbnt 1001  ax467 1022  nalequcoms 1143  necon1ai 1606  necon1bi 1607  1st2val 4088  2nd2val 4089  eceqopreq 4306  unbndrank 4666  str 10140  hstr 10148

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

Copyright terms: Public domain