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 972  hbnt 1000  ax467 1021  nalequcoms 1142  necon1ai 1605  necon1bi 1606  1st2val 4085  2nd2val 4086  eceqopreq 4303  unbndrank 4663  str 10122  hstr 10130

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

Copyright terms: Public domain