Theorem con3i 140

Description: A contraposition inference. Inference associated with con3 139. Its associated inference is mto 179. (Contributed by NM, 3-Jan-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 23	. 2 |- ( -. ps -> -. ps )
2		con3i.a	. 2 |- ( ph -> ps )
3	1, 2	nsyl 124	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:  pm2.51  156  pm2.65i  176  pm5.21ni  353  pm2.45  398  pm2.46  399  nbiorOLD  869  pm5.14  894  con3th  966  rb-ax2  1632  rb-ax4  1634  stoic1aOLD  1652  ax13  2103  sbequi  2170  euor2  2313  baroco  2377  necon3bi  2660  necon1biOLD  2665  eueq3  3252  sbc2or  3314  sbcimdv  3367  sbcrext  3379  difrab  3753  abvor0  3786  csbprc  3804  sbcel12  3806  sbcne12  3809  sbcel2  3812  ifeqor  3959  ifan  3961  nelpri  4023  nelprd  4024  opprc1  4213  opprc2  4214  sbcbr123  4477  snexALT  4611  mosubopt  4719  csbopab  4753  csbxp  4936  soirri  5246  predpoirr  5427  predfrirr  5428  csbiota  5594  nfvres  5911  fvco4i  5959  fvmptex  5976  fvopab4ndm  5988  ressnop0  6086  csbriota  6279  ovprc  6335  ovprc1  6336  ovprc2  6337  ndmovass  6471  ndmovdistr  6472  eldifpw  6617  nlimsucg  6683  tfindsg  6701  findsg  6734  curry1val  6900  curry2val  6904  extmptsuppeq  6950  funsssuppss  6952  eceqoveq  7476  fiprc  7658  sdomirr  7715  domtriord  7724  2pwuninel  7733  mapdom1  7743  nfielex  7806  relprcnfsupp  7892  supval2  7975  wemapso2  8068  card2inf  8070  en2lp  8118  wemapwe  8201  rankxplim3  8351  fidomtri2  8427  alephnbtwn  8500  kmlem2  8579  isfin7-2  8824  dominf  8873  ac6n  8913  alephval2  8995  dominfac  8996  axpowndlem3  9022  gchdomtri  9053  nlt1pi  9330  adderpq  9380  mulerpq  9381  zeo  11021  fzoval  11919  bcpasc  12503  hashnemnf  12524  hasheq0  12541  hashunx  12562  hashbc  12611  prmreclem4  14826  ressinbas  15147  natfval  15802  fucbas  15816  fuchom  15817  homarcl  15874  arwval  15889  coafval  15910  grpidval  16454  symgbas  16972  efgval  17302  gsum2dlem1  17537  gsum2dlem2  17538  dprddomprc  17567  dprdval0prc  17569  psrvscafval  18549  mavmul0g  19509  mdetralt  19564  mdetunilem9  19576  tgdif0  19939  resstopn  20133  cfinfil  20839  pcofval  21934  i1fima2  22514  i1fd  22516  itgeq2  22612  ibladdlem  22654  cusgrafi  25055  uvtx01vtx  25065  frgra2v  25572  2spotiundisj  25635  numclwwlkdisj  25653  avril1  25745  nmobndseqi  26265  nonbooli  27139  chpssati  27851  xrge0neqmnf  28290  hasheuni  28745  inelpisys  28815  ddemeas  28898  bnj1143  29390  rdgprc0  30227  distel  30237  linedegen  30695  ordcmp  30892  bj-con3thALT  30940  bj-babygodel  30970  bj-nexrt  31025  bj-csbprc  31261  bj-projval  31339  wl-naev  31569  wl-ax11-lem8  31626  poimirlem26  31670  poimirlem27  31671  poimirlem31  31675  cnambfre  31693  itg2addnclem3  31699  ibladdnclem  31702  frinfm  31766  tsbi3  32081  ax13fromc9  32185  axc711  32194  axc711toc7  32196  axc5c711toc7  32200  equidqe  32202  equidq  32204  ax12indalem  32225  hdmap1eulem  35101  hdmapevec  35115  jm2.22  35556  rp-fakeimass  35855  nanorxor  36290  binomcxplemfrat  36337  binomcxplemradcnv  36338  pm10.251  36346  axc5c4c711toc7  36392  en3lpVD  36881  ax6e2ndeqVD  36946  2sb5ndVD  36947  ax6e2ndeqALT  36968  2sb5ndALT  36969  sineq0ALT  36974  fzdifsuc2  37139  infrglbOLD  37241  cncfiooicc  37344  itgcoscmulx  37415  sge0sn  37755  iundjiunlem  37806  nabctnabc  37919  ndmafv  38032  nfunsnafv  38034  afvprc  38036  afvnufveq  38039  aovprc  38080  ndmaovass  38098  ndmaovdistr  38099