Theorem pm2.21i 131

Description: A contradiction implies anything. Inference from 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  852  falim  1393  nfnth  1611  axc5sp1  2246  rex0  3804  0ss  3819  abf  3824  r19.2zb  3924  ral0  3938  rabsnifsb  4101  snsssn  4201  int0  4302  axnulALT  4580  axc16b  4645  dtrucor  4686  bropopvvv  6875  tfrlem16  7074  omordi  7227  nnmordi  7292  omabs  7308  omsmolem  7314  0er  7358  pssnn  7750  fiint  7809  cantnfle  8102  cantnfleOLD  8132  r1sdom  8204  alephordi  8467  axdc3lem2  8843  canthp1  9044  elnnnn0b  10852  xltnegi  11427  xmulasslem2  11486  xrinfm0  11540  elixx3g  11554  elfz2  11691  om2uzlti  12041  hashf1lem2  12486  sum0  13523  fsum2dlem  13565  exprmfct  14127  4sqlem18  14356  vdwap0  14370  ram0  14416  prmlem1a  14467  prmlem2  14480  xpsfrnel2  14837  0catg  14959  alexsub  20413  0met  20737  vitali  21890  plyeq0  22476  jensen  23184  ppiublem1  23343  ppiublem2  23344  lgsdir2lem3  23466  rpvmasum  23577  usgraedgprv  24199  4cycl4dv  24490  clwwlknprop  24595  2wlkonot3v  24698  2spthonot3v  24699  frgrareggt1  24940  isarchi  27550  sibf0  28101  sgn3da  28305  sgnnbi  28309  sgnpbi  28310  signstfvneq0  28354  prod0  29002  fprod2dlem  29037  sltsolem1  29355  bisym1  29811  unqsym1  29817  amosym1  29818  subsym1  29819  areaquad  31113  iblempty  31606  fveqvfvv  31999  ndmaovcl  32078  bnj98  33405  bj-dfif5ALT  33631  bj-godellob  33676  bj-axc16b  33866  bj-dtrucor  33868