Theorem con3i 127

Description: A contraposition inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 20-Jun-2013.)

Hypothesis

Ref	Expression
con3i.a	⊢ (φ → ψ)

Assertion

Ref	Expression
con3i	⊢ (¬ ψ → ¬ φ)

Proof of Theorem con3i

Step	Hyp	Ref	Expression
1		id 19	. 2 ⊢ (¬ ψ → ¬ ψ)
2		con3i.a	. 2 ⊢ (φ → ψ)
3	1, 2	nsyl 113	1 ⊢ (¬ ψ → ¬ φ)

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  pm2.51  145  pm2.65i  165  pm5.21ni  341  pm2.45  386  pm2.46  387  pm5.14  856  con3th  924  cadan  1392  rb-ax2  1518  rb-ax4  1520  equidOLD  1677  hbn1fw  1705  spOLD  1748  hbnOLD  1777  spimehOLD  1821  cbv3hvOLD  1851  ax12  1935  dvelimv  1939  ax9  1949  sbn  2062  sbcom  2089  ax12from12o  2156  ax67  2165  ax67to6  2167  ax467to6  2171  equidqe  2173  equidq  2175  ax11indalem  2197  euor2  2272  moexex  2273  baroco  2310  necon1bi  2560  eueq3  3012  sbc2or  3055  difrab  3530  abvor0  3568  ifeqor  3700  ifan  3702  nelpri  3755  setswith  4322  eqtfinrelk  4487  dfphi2  4570  mosubopt  4613  phialllem2  4618  imasn  5019  dmsnopss  5068  fvprc  5326  tz6.12-2  5347  ndmfv  5350  nfvres  5353  fvopab4ndm  5391  ressnop0  5437  ndmovass  5619  ndmovdistr  5620  fvmptex  5722  clos1nrel  5887  ncprc  6125  frecxp  6315