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  845  falim  1378  nfnth  1606  axc5sp1  2230  rex0  3648  0ss  3663  abf  3668  r19.2zb  3767  ral0  3781  rabsnifsb  3940  snsssn  4038  int0  4139  axnulALT  4416  axc16b  4481  dtrucor  4522  bropopvvv  6652  tfrlem16  6848  omordi  7001  nnmordi  7066  omabs  7082  omsmolem  7088  0er  7132  pssnn  7527  fiint  7584  cantnfle  7875  cantnfleOLD  7905  r1sdom  7977  alephordi  8240  axdc3lem2  8616  canthp1  8817  elnnnn0b  10620  xltnegi  11182  xmulasslem2  11241  xrinfm0  11295  elixx3g  11309  elfz2  11440  om2uzlti  11769  hashf1lem2  12205  sum0  13194  fsum2dlem  13233  exprmfct  13792  4sqlem18  14019  vdwap0  14033  ram0  14079  prmlem1a  14130  prmlem2  14143  xpsfrnel2  14499  0catg  14621  alexsub  19517  0met  19841  vitali  20993  plyeq0  21622  jensen  22325  ppiublem1  22484  ppiublem2  22485  lgsdir2lem3  22607  rpvmasum  22718  usgraedgprv  23214  4cycl4dv  23472  isarchi  26116  sibf0  26634  sgn3da  26838  sgnnbi  26842  sgnpbi  26843  signstfvneq0  26887  prod0  27369  fprod2dlem  27404  sltsolem1  27722  bisym1  28179  unqsym1  28185  amosym1  28186  subsym1  28187  areaquad  29501  fveqvfvv  29939  ndmaovcl  30018  2wlkonot3v  30303  2spthonot3v  30304  clwwlknprop  30344  frgrareggt1  30618  bnj98  31677  bj-godellob  31902  bj-axc16b  32054  bj-dtrucor  32056