Theorem con3i 135

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 22	. 2 |- ( -. ps -> -. ps )
2		con3i.a	. 2 |- ( ph -> ps )
3	1, 2	nsyl 121	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  153  pm2.65i  173  pm5.21ni  352  pm2.45  397  pm2.46  398  nbior  851  pm5.14  876  con3th  944  cadanOLD  1439  rb-ax2  1565  rb-ax4  1567  thema1a  1584  ax13  2000  sbequi  2071  sbnOLD  2088  ax13fromc9  2210  axc711  2219  axc711toc7  2221  axc5c711toc7  2225  equidqe  2227  equidq  2229  ax12indalem  2250  euor2  2315  euor2OLD  2316  moexexOLD  2353  baroco  2392  necon1bi  2652  eueq3  3131  sbc2or  3192  sbcimdv  3252  sbcrext  3266  difrab  3621  abvor0  3652  csbprc  3670  sbcel12  3672  sbcne12  3676  sbcel2  3680  ifeqor  3830  ifan  3832  nelpri  3895  nelprd  3896  opprc1  4079  opprc2  4080  sbcbr123  4340  snexALT  4475  mosubopt  4586  csbopab  4618  csbxp  4914  soirri  5221  soirriOLD  5226  csbiota  5407  nfvres  5717  fvco4i  5766  fvmptex  5781  fvopab4ndm  5791  ressnop0  5886  csbriota  6062  ovprc  6117  ovprc1  6118  ovprc2  6119  ndmovass  6250  ndmovdistr  6251  eldifpw  6387  nlimsucg  6452  tfindsg  6470  findsg  6502  curry1val  6664  curry2val  6668  extmptsuppeq  6712  funsssuppss  6714  eceqoveq  7201  fiprc  7387  sdomirr  7444  domtriord  7453  2pwuninel  7462  mapdom1  7472  nfielex  7537  relprcnfsupp  7619  supval2  7701  wemapso2  7764  card2inf  7766  en2lp  7815  wemapwe  7924  wemapweOLD  7925  rankxplim3  8084  fidomtri2  8160  alephnbtwn  8237  kmlem2  8316  isfin7-2  8561  dominf  8610  ac6n  8650  alephval2  8732  dominfac  8733  axpowndlem3  8760  gchdomtri  8792  nlt1pi  9071  adderpq  9121  mulerpq  9122  zeo  10723  fzoval  11550  bcpasc  12093  hashnemnf  12111  hasheq0  12127  hashunx  12145  hashbc  12202  prmreclem4  13976  ressinbas  14230  natfval  14852  fucbas  14866  fuchom  14867  homarcl  14892  arwval  14907  coafval  14928  grpidval  15428  symgbas  15878  efgval  16207  gsum2dlem1  16451  gsum2dlem2  16452  gsum2dOLD  16454  dprddomprc  16472  dprdval0prc  16474  psrvscafval  17439  mavmul0g  18323  mdetralt  18373  mdetunilem9  18385  tgdif0  18556  resstopn  18749  cfinfil  19425  pcofval  20541  i1fima2  21116  i1fd  21118  itgeq2  21214  ibladdlem  21256  cusgrafi  23325  uvtx01vtx  23335  avril1  23591  nmobndseqi  24114  nonbooli  24989  chpssati  25702  xrge0neqmnf  26085  hasheuni  26470  ddemeas  26588  rdgprc0  27536  distel  27546  predpoirr  27587  predfrirr  27588  linedegen  28103  ordcmp  28223  wl-naev  28287  wl-ax11-lem8  28333  cnambfre  28365  itg2addnclem3  28370  ibladdnclem  28373  frinfm  28554  tsbi3  28871  jm2.22  29269  pm10.251  29537  axc5c4c711toc7  29583  infrglb  29696  ndmafv  29971  nfunsnafv  29973  afvprc  29975  afvnufveq  29978  aovprc  30019  ndmaovass  30037  ndmaovdistr  30038  frgra2v  30516  2spotiundisj  30580  numclwwlkdisj  30598  en3lpVD  31415  ax6e2ndeqVD  31479  2sb5ndVD  31480  ax6e2ndeqALT  31501  2sb5ndALT  31502  sineq0ALT  31507  bnj1143  31618  bj-babygodel  31917  bj-csbprc  32149  bj-projval  32219  hdmap1eulem  35191  hdmapevec  35205