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  850  falim  1384  nfnth  1602  axc5sp1  2233  rex0  3762  0ss  3777  abf  3782  r19.2zb  3881  ral0  3895  rabsnifsb  4054  snsssn  4152  int0  4253  axnulALT  4530  axc16b  4595  dtrucor  4636  bropopvvv  6766  tfrlem16  6965  omordi  7118  nnmordi  7183  omabs  7199  omsmolem  7205  0er  7249  pssnn  7645  fiint  7702  cantnfle  7994  cantnfleOLD  8024  r1sdom  8096  alephordi  8359  axdc3lem2  8735  canthp1  8936  elnnnn0b  10739  xltnegi  11301  xmulasslem2  11360  xrinfm0  11414  elixx3g  11428  elfz2  11565  om2uzlti  11894  hashf1lem2  12331  sum0  13320  fsum2dlem  13359  exprmfct  13918  4sqlem18  14145  vdwap0  14159  ram0  14205  prmlem1a  14256  prmlem2  14269  xpsfrnel2  14626  0catg  14748  alexsub  19759  0met  20083  vitali  21236  plyeq0  21822  jensen  22525  ppiublem1  22684  ppiublem2  22685  lgsdir2lem3  22807  rpvmasum  22918  usgraedgprv  23474  4cycl4dv  23732  isarchi  26371  sibf0  26887  sgn3da  27091  sgnnbi  27095  sgnpbi  27096  signstfvneq0  27140  prod0  27623  fprod2dlem  27658  sltsolem1  27976  bisym1  28432  unqsym1  28438  amosym1  28439  subsym1  28440  areaquad  29763  fveqvfvv  30201  ndmaovcl  30280  2wlkonot3v  30565  2spthonot3v  30566  clwwlknprop  30606  frgrareggt1  30880  bnj98  32215  bj-dfif5ALT  32441  bj-godellob  32486  bj-axc16b  32676  bj-dtrucor  32678