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 664  ax5o 971  hbnt 999  ax467 1019  nalequcoms 1140  necon1ai 1600  necon1bi 1601  1st2val 4079  2nd2val 4080  eceqopreq 4297  unbndrank 4655  str 10094  hstr 10102

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

Copyright terms: Public domain