Theorem con3i 90

Description: A contraposition inference.

Hypothesis

Ref	Expression
con3.a	⊢ (φ → ψ)

Assertion

Ref	Expression
con3i	⊢ (¬ ψ → ¬ φ)

Proof of Theorem con3i

Step	Hyp	Ref	Expression
1		nega 78	. . 3 ⊢ (¬ ¬ φ → φ)
2		con3.a	. . 3 ⊢ (φ → ψ)
3	1, 2	syl 12	. 2 ⊢ (¬ ¬ φ → ψ)
4	3	con1i 88	1 ⊢ (¬ ψ → ¬ φ)

Syntax hints:  ¬ wn 1   → wi 2

This theorem is referenced by:  mto 93  nsyl 102  negbii 162  pm2.45 228  pm2.46 229  orim12i 271  pm5.21ni 503  con3th 573  hbne 699  19.9r 718  19.29 752  sbn2 881  moexex 1058  sbc2or 1454  difrab 1695  noel 1711  disjsn2 1837  mosubop 1911  fr2nr 2177  fr3nr 2178  nlimsuc 2363  findsg 2398  tfindsg 2402  vtoclibr 2451  soirri 2629  nfvres 2850  fvopabn 2873  canth 2945  oprprc1 3019  ndmoprass 3062  ndmoprdistr 3063  eceqopreq 3249  sdomirr 3314  ensdomtr 3372  sdomen2 3380  en2lp 3453  inf3lem2 3465  isfinite 3480  nnsdom 3481  kmlem2 3581  alephnbtwn 3674  alephnbtwn2 3675  alephord 3680  cdainf 3731  nd3 3734  axrepnd 3740  nlt1pi 3827  lt1nnn 4442  nnesq 4720  ruclem28 4912  chpssat 5756

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

metamath.org