Theorem con2i 134

Description: A contraposition inference. Its associated inference is mt2 191. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Mel L. O'Cat, 28-Nov-2008.) (Proof shortened by Wolf Lammen, 13-Jun-2013.)

Hypothesis

Ref	Expression
con2i.a	|- ( ph -> -. ps )

Assertion

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

Proof of Theorem con2i

Step	Hyp	Ref	Expression
1		con2i.a	. 2 |- ( ph -> -. ps )
2		id 22	. 2 |- ( ps -> ps )
3	1, 2	nsyl3 133	1 |- ( ps -> -. ph )

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:  nsyl  135  notnot  136  pm2.65i  185  pm3.14  523  pclem6  971  hba1w  1974  hba1wOLD  1975  axc4  2130  festino  2571  calemes  2581  fresison  2583  calemos  2584  fesapo  2585  necon3ai  2819  necon2ai  2823  necon2bi  2824  eueq3  3381  ssnpss  3710  psstr  3711  elndif  3734  n0i  3920  axnulALT  4787  nfcvb  4898  zfpair  4904  onxpdisj  5847  funtpgOLD  5943  ftpg  6423  nlimsucg  7042  reldmtpos  7360  bren2  7986  sdom0  8092  domunsn  8110  sdom1  8160  enp1i  8195  alephval3  8933  dfac2  8953  cdainflem  9013  ackbij1lem18  9059  isfin4-3  9137  fincssdom  9145  fin23lem41  9174  fin45  9214  fin17  9216  fin1a2lem7  9228  axcclem  9279  pwcfsdom  9405  canthp1lem1  9474  hargch  9495  winainflem  9515  ltxrlt  10108  xmullem2  12095  rexmul  12101  xlemul1a  12118  fzdisj  12368  lcmfunsnlem2lem2  15352  pmtrdifellem4  17899  psgnunilem3  17916  frgpcyg  19922  dvlog2lem  24398  lgsval2lem  25032  strlem1  29109  chrelat2i  29224  dfrdg4  32058  finminlem  32312  bj-nimn  32551  bj-modald  32661  finxpreclem3  33230  finxpreclem5  33232  hba1-o  34182  hlrelat2  34689  cdleme50ldil  35836  or3or  38319  stoweidlem14  40231  alneu  41201  2nodd  41812  elsetrecslem  42444