Theorem con3i 135

Description: A contraposition inference. Inference associated with con3 134. Its associated inference is mto 176. (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 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  350  pm2.45  395  pm2.46  396  nbiorOLD  859  pm5.14  884  con3th  956  rb-ax2  1593  rb-ax4  1595  stoic1aOLD  1613  ax13  2053  sbequi  2120  euor2  2266  baroco  2330  necon3bi  2611  necon1biOLD  2616  eueq3  3199  sbc2or  3261  sbcimdv  3314  sbcrext  3326  difrab  3697  abvor0  3730  csbprc  3748  sbcel12  3750  sbcne12  3753  sbcel2  3756  ifeqor  3901  ifan  3903  nelpri  3965  nelprd  3966  opprc1  4154  opprc2  4155  sbcbr123  4418  snexALT  4551  mosubopt  4659  csbopab  4693  csbxp  4995  soirri  5306  csbiota  5489  nfvres  5804  fvco4i  5852  fvmptex  5868  fvopab4ndm  5880  ressnop0  5980  csbriota  6170  ovprc  6226  ovprc1  6227  ovprc2  6228  ndmovass  6362  ndmovdistr  6363  eldifpw  6511  nlimsucg  6576  tfindsg  6594  findsg  6626  curry1val  6792  curry2val  6796  extmptsuppeq  6842  funsssuppss  6844  eceqoveq  7334  fiprc  7516  sdomirr  7573  domtriord  7582  2pwuninel  7591  mapdom1  7601  nfielex  7664  relprcnfsupp  7747  supval2  7829  wemapso2  7894  card2inf  7896  en2lp  7944  wemapwe  8052  wemapweOLD  8053  rankxplim3  8212  fidomtri2  8288  alephnbtwn  8365  kmlem2  8444  isfin7-2  8689  dominf  8738  ac6n  8778  alephval2  8860  dominfac  8861  axpowndlem3  8887  gchdomtri  8918  nlt1pi  9195  adderpq  9245  mulerpq  9246  zeo  10865  fzoval  11723  bcpasc  12301  hashnemnf  12319  hasheq0  12336  hashunx  12357  hashbc  12406  prmreclem4  14439  ressinbas  14697  natfval  15352  fucbas  15366  fuchom  15367  homarcl  15424  arwval  15439  coafval  15460  grpidval  16004  symgbas  16522  efgval  16852  gsum2dlem1  17111  gsum2dlem2  17112  gsum2dOLD  17114  dprddomprc  17144  dprdval0prc  17146  psrvscafval  18156  mavmul0g  19140  mdetralt  19195  mdetunilem9  19207  tgdif0  19579  resstopn  19773  cfinfil  20479  pcofval  21595  i1fima2  22171  i1fd  22173  itgeq2  22269  ibladdlem  22311  cusgrafi  24603  uvtx01vtx  24613  frgra2v  25120  2spotiundisj  25183  numclwwlkdisj  25201  avril1  25292  nmobndseqi  25811  nonbooli  26686  chpssati  27398  xrge0neqmnf  27832  hasheuni  28233  ddemeas  28364  rdgprc0  29391  distel  29401  predpoirr  29442  predfrirr  29443  linedegen  29946  ordcmp  30065  wl-naev  30147  wl-ax11-lem8  30197  cnambfre  30228  itg2addnclem3  30234  ibladdnclem  30237  frinfm  30392  tsbi3  30708  jm2.22  31103  nanorxor  31353  binomcxplemfrat  31424  binomcxplemradcnv  31425  pm10.251  31433  axc5c4c711toc7  31479  fzdifsuc2  31678  infrglb  31750  cncfiooicc  31863  itgcoscmulx  31934  ndmafv  32391  nfunsnafv  32393  afvprc  32395  afvnufveq  32398  aovprc  32439  ndmaovass  32457  ndmaovdistr  32458  en3lpVD  33991  ax6e2ndeqVD  34056  2sb5ndVD  34057  ax6e2ndeqALT  34078  2sb5ndALT  34079  sineq0ALT  34084  bnj1143  34196  bj-con3thALT  34509  bj-babygodel  34538  bj-nexrt  34592  bj-csbprc  34823  bj-projval  34902  ax13fromc9  35048  axc711  35057  axc711toc7  35059  axc5c711toc7  35063  equidqe  35065  equidq  35067  ax12indalem  35088  hdmap1eulem  37964  hdmapevec  37978  rp-fakeimass  38166