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 662  pm5.21ni 675  con3th 763  ax67 994  ax67to6 995  ax467to6 999  19.29 1047  sbn 1215  ax11indalem 1345  a12lem2 1354  moexex 1415  necon3ai 1582  necon3bi 1583  sbc2or 1929  difrab 2244  noel 2255  mosubopt 2767  eldifpw 2873  nlimsucg 3075  findsg 3120  tfindsg 3125  vtoclibr 3175  soirri 3391  nfvres 3687  fvopab4ndm 3723  fvopabn 3725  canth 3846  oprprc1 3923  ndmoprass 3988  ndmoprdistr 3989  curry1val 4038  eceqopreq 4251  ensdomtr 4405  sdomirr 4406  sdomen2 4416  en2lp 4526  isfinite 4558  nnsdom 4559  rankxplim3 4638  rankxpsuc 4639  ac6n 4681  ac9s 4688  kmlem2 4690  alephnbtwn 4791  alephnbtwn2 4792  alephval2 4825  dominf 4827  cdainf 4860  nd3 4863  axrepnd 4869  nlt1pi 4956  lt1nnn 5846  zeot 6097  uzssz 6313  sumsqne0 6516  nnesq 6543  climcl 6867  clmi1 6975  ruclem28 7431  issubg 8001  fiiu 8709  neiopne 8728  hmeogrp 8776  fgsb 8794  fgsb2 8799  cnfilca 8801  avril1 8964  nonbool 9727  chpssat 10412

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

Copyright terms: Public domain