Theorem con3i 98

Description: A contraposition inference.

Hypothesis

Ref	Expression
con3.a	⊢ (φ → ψ)

Assertion

Ref	Expression
con3i	⊢ (¬ ψ → ¬ φ)

Proof of Theorem con3i

Step	Hyp	Ref	Expression
1		nega 84	. . 3 ⊢ (¬ ¬ φ → φ)
2		con3.a	. . 3 ⊢ (φ → ψ)
3	1, 2	syl 10	. 2 ⊢ (¬ ¬ φ → ψ)
4	3	con1i 96	1 ⊢ (¬ ψ → ¬ φ)

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 664  pm5.21ni 677  con3th 765  ax4 971  ax67 1019  ax67to6 1020  ax467to6 1024  19.29 1070  sbn 1230  ax11indalem 1367  a12lem2 1376  moexex 1437  necon3ai 1604  necon3bi 1605  sbc2or 1955  difrab 2270  noel 2281  mosubopt 2800  eldifpw 2906  nlimsucg 3108  findsg 3153  tfindsg 3158  vtoclibr 3209  soirri 3438  nfvres 3743  fvopab4ndm 3779  fvopabn 3781  canth 3902  oprprc1 3979  ndmoprass 4043  ndmoprdistr 4044  curry1val 4093  eceqopreq 4306  ensdomtr 4460  sdomirr 4461  sdomen2 4471  pwuninel 4475  2pwuninel 4476  en2lp 4585  isfinite 4617  nnsdom 4618  rankxplim3 4697  rankxpsuc 4698  ac6n 4740  ac9s 4747  kmlem2 4749  alephnbtwn 4851  alephnbtwn2 4852  alephval2 4885  dominf 4887  cdainf 4920  nd3 4923  axrepnd 4929  nlt1pi 5016  lt1nnn 5905  zeot 6156  uzssz 6375  sumsqne0 6579  nnesq 6607  climcl 6931  clmi1 7039  ruclem28 7497  issubg 8080  avril1 8739  nonbool 9553  chpssat 10246  fiiu 10408  neiopne 10427  hmeogrp 10484  fgsb 10503  fgsb2 10508  cnfilca 10510  rcfpfillem2 10512

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

Copyright terms: Public domain