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	|- (ph -> ps)

Assertion

Ref	Expression
con3i	|- (-. ps -> -. ph)

Proof of Theorem con3i

Step	Hyp	Ref	Expression
1		id 19	. 2 |- (-. ps -> -. ps)
2		con3i.a	. 2 |- (ph -> ps)
3	1, 2	nsyl 113	1 |- (-. ps -> -. ph)

Syntax hints:  -. wn 3   -> wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 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  2559  eueq3  3011  sbc2or  3054  difrab  3529  abvor0  3567  ifeqor  3699  ifan  3701  nelpri  3754  setswith  4321  eqtfinrelk  4486  dfphi2  4569  mosubopt  4612  phialllem2  4617  imasn  5018  dmsnopss  5067  fvprc  5325  tz6.12-2  5346  ndmfv  5349  nfvres  5352  fvopab4ndm  5390  ressnop0  5436  ndmovass  5618  ndmovdistr  5619  fvmptex  5721  clos1nrel  5886  ncprc  6124  frecxp  6314