Theorem pm2.21i 125

Description: A contradiction implies anything. Inference from pm2.21 102. (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 124	1 |- ( ph -> ps )

Syntax hints:   -. wn 3   -> wi 4

This theorem is referenced by:  pm2.24ii  126  pm3.2ni  828  falim  1334  nfnth  1562  ax4sp1  2224  rex0  3601  0ss  3616  abf  3621  r19.2zb  3678  ral0  3692  snsssn  3927  int0  4024  axnulALT  4296  ax16b  4351  dtrucor  4357  bropopvvv  6385  tfrlem16  6613  omordi  6768  nnmordi  6833  omabs  6849  omsmolem  6855  0er  6899  pssnn  7286  fiint  7342  cantnfle  7582  r1sdom  7656  alephordi  7911  axdc3lem2  8287  canthp1  8485  elnnnn0b  10220  xltnegi  10758  xmulasslem2  10817  xrinfm0  10871  elixx3g  10885  elfz2  11006  om2uzlti  11245  hashf1lem2  11660  sum0  12470  fsum2dlem  12509  exprmfct  13065  4sqlem18  13285  vdwap0  13299  ram0  13345  prmlem1a  13384  prmlem2  13397  xpsfrnel2  13745  0catg  13867  alexsub  18029  0met  18349  vitali  19458  plyeq0  20083  jensen  20780  ppiublem1  20939  ppiublem2  20940  lgsdir2lem3  21062  rpvmasum  21173  usgraedgprv  21349  4cycl4dv  21607  isarchi  24205  sibf0  24602  prod0  25222  fprod2dlem  25257  sltsolem1  25536  bisym1  26073  unqsym1  26079  amosym1  26080  subsym1  26081  fveqvfvv  27855  ndmaovcl  27934  2wlkonot3v  28072  2spthonot3v  28073  bnj98  28944  ax7w7AUX7  29353

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8