Theorem con3i 98

Description: A contraposition inference.

Hypothesis

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

Assertion

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

Proof of Theorem con3i

Step	Hyp	Ref	Expression
1		nega 84	. . 3 |- (-. -. ph -> ph)
2		con3.a	. . 3 |- (ph -> ps)
3	1, 2	syl 10	. 2 |- (-. -. ph -> ps)
4	3	con1i 96	1 |- (-. ps -> -. ph)

Syntax hints:  -. wn 2   -> wi 3

This theorem is referenced by:  pm2.5 100  pm2.51 101  pm2.52 102  mto 106  nsyl 116  negbii 187  pm2.45 277  pm2.46 278  orim12i 336  pm5.14 665  pm5.21ni 678  con3th 766  ax4 972  ax67 1020  ax67to6 1021  ax467to6 1025  19.29 1071  sbn 1231  ax11indalem 1368  a12lem2 1377  moexex 1438  necon3ai 1606  necon3bi 1607  sbc2or 1958  difrab 2273  noel 2284  mosubopt 2804  eldifpw 2910  nlimsucg 3112  findsg 3157  tfindsg 3162  vtoclibr 3213  soirri 3442  nfvres 3748  fvopab4ndm 3784  fvopabn 3786  canth 3907  oprprc1 3984  ndmoprass 4048  ndmoprdistr 4049  curry1val 4100  eceqopreq 4313  ensdomtr 4471  sdomirr 4472  sdomen2 4482  pwuninel 4486  2pwuninel 4487  en2lp 4602  isfiniteOLD 4634  nnsdom 4635  rankxplim3 4714  rankxpsuc 4715  ac6n 4757  ac9s 4764  kmlem2 4766  alephnbtwn 4868  alephnbtwn2 4869  alephval2 4902  dominf 4904  cdainf 4937  nd3 4940  axrepnd 4946  nlt1pi 5033  lt1nnn 5947  zeot 6199  uzssz 6430  sumsqne0 6634  nnesq 6662  climcl 6978  clmi1 7086  ruclem28 7537  issubg 8116  avril1 8784  nonbool 9596  chpssat 10290  fiiu 10453  fiiuOLD 10454  neiopne 10474  hmeogrp 10538  fgsb 10570  fgsbOLD 10571  fgsb2 10580  cnfilca 10583  cnfilcaOLD 10584  rcfpfillem2 10587  rcfpfillem2OLD 10588

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

Copyright terms: Public domain