Theorem pm2.21i 131

Description: A contradiction implies anything. Inference associated with pm2.21 108. (Contributed by NM, 16-Sep-1993.)

Hypothesis

Ref	Expression
pm2.21i.1	|- -. ph

Assertion

Ref	Expression
pm2.21i	|- ( ph -> ps )

Proof of Theorem pm2.21i

Step	Hyp	Ref	Expression
1		pm2.21i.1	. . 3 |- -. ph
2	1	a1i 11	. 2 |- ( -. ps -> -. ph )
3	2	con4i 130	1 |- ( ph -> ps )

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.24ii  132  pm2.21dd  174  pm3.2ni  854  falim  1397  nfnth  1615  axc5sp1  2239  rex0  3785  0ss  3800  abf  3805  r19.2zb  3905  ral0  3919  rabsnifsb  4083  snsssn  4183  int0  4285  axnulALT  4564  axc16b  4629  dtrucor  4670  bropopvvv  6865  tfrlem16  7064  omordi  7217  nnmordi  7282  omabs  7298  omsmolem  7304  0er  7348  pssnn  7740  fiint  7799  cantnfle  8093  cantnfleOLD  8123  r1sdom  8195  alephordi  8458  axdc3lem2  8834  canthp1  9035  elnnnn0b  10846  xltnegi  11424  xmulasslem2  11483  xrinfm0  11537  elixx3g  11551  elfz2  11688  om2uzlti  12040  hashf1lem2  12484  sum0  13522  fsum2dlem  13564  exprmfct  14128  4sqlem18  14357  vdwap0  14371  ram0  14417  prmlem1a  14469  prmlem2  14482  xpsfrnel2  14839  0catg  14961  alexsub  20418  0met  20742  vitali  21895  plyeq0  22481  jensen  23190  ppiublem1  23349  ppiublem2  23350  lgsdir2lem3  23472  rpvmasum  23583  usgraedgprv  24248  4cycl4dv  24539  clwwlknprop  24644  2wlkonot3v  24747  2spthonot3v  24748  frgrareggt1  24988  isarchi  27599  sibf0  28149  sgn3da  28353  sgnnbi  28357  sgnpbi  28358  signstfvneq0  28402  prod0  29050  fprod2dlem  29085  sltsolem1  29403  bisym1  29859  unqsym1  29865  amosym1  29866  subsym1  29867  areaquad  31160  iblempty  31654  fveqvfvv  32047  ndmaovcl  32126  bnj98  33653  bj-dfif5ALT  33891  bj-godellob  33935  bj-axc16b  34126  bj-dtrucor  34128