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 663  pm5.21ni 676  con3th 764  ax4 969  ax67 1016  ax67to6 1017  ax467to6 1021  19.29 1067  sbn 1226  ax11indalem 1361  a12lem2 1370  moexex 1431  necon3ai 1598  necon3bi 1599  sbc2or 1948  difrab 2263  noel 2274  mosubopt 2793  eldifpw 2900  nlimsucg 3102  findsg 3147  tfindsg 3152  vtoclibr 3203  soirri 3428  nfvres 3733  fvopab4ndm 3769  fvopabn 3771  canth 3892  oprprc1 3969  ndmoprass 4034  ndmoprdistr 4035  curry1val 4084  eceqopreq 4297  ensdomtr 4451  sdomirr 4452  sdomen2 4462  en2lp 4574  isfinite 4606  nnsdom 4607  rankxplim3 4686  rankxpsuc 4687  ac6n 4729  ac9s 4736  kmlem2 4738  alephnbtwn 4840  alephnbtwn2 4841  alephval2 4874  dominf 4876  cdainf 4909  nd3 4912  axrepnd 4918  nlt1pi 5005  lt1nnn 5895  zeot 6146  uzssz 6362  sumsqne0 6565  nnesq 6592  climcl 6916  clmi1 7024  ruclem28 7480  issubg 8053  avril1 8723  nonbool 9513  chpssat 10198  fiiu 10350  neiopne 10369  hmeogrp 10425  fgsb 10444  fgsb2 10449  cnfilca 10451

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

Copyright terms: Public domain