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  852  falim  1413  nfnth  1636  rex0  3726  0ss  3741  abf  3746  r19.2zb  3835  ral0  3850  rabsnifsb  4012  snsssn  4112  int0  4213  axnulALT  4494  axc16b  4557  dtrucor  4595  bropopvvv  6779  tfrlem16  6980  omordi  7133  nnmordi  7198  omabs  7214  omsmolem  7220  0er  7264  pssnn  7654  fiint  7712  cantnfle  8003  cantnfleOLD  8033  r1sdom  8105  alephordi  8368  axdc3lem2  8744  canthp1  8943  elnnnn0b  10757  xltnegi  11336  xmulasslem2  11395  xrinfm0  11449  elixx3g  11463  elfz2  11600  om2uzlti  11964  hashf1lem2  12409  sum0  13545  fsum2dlem  13587  prod0  13752  fprod2dlem  13786  exprmfct  14253  4sqlem18  14482  vdwap0  14496  ram0  14542  prmlem1a  14594  prmlem2  14607  xpsfrnel2  14972  0catg  15094  alexsub  20630  0met  20954  vitali  22107  plyeq0  22693  jensen  23435  ppiublem1  23594  ppiublem2  23595  lgsdir2lem3  23717  rpvmasum  23828  usgraedgprv  24497  4cycl4dv  24788  clwwlknprop  24893  2wlkonot3v  24996  2spthonot3v  24997  frgrareggt1  25237  isarchi  27879  sibf0  28459  sgn3da  28663  sgnnbi  28667  sgnpbi  28668  signstfvneq0  28712  sltsolem1  29593  bisym1  30037  unqsym1  30043  amosym1  30044  subsym1  30045  areaquad  31352  iblempty  31930  fveqvfvv  32375  ndmaovcl  32454  nn0enne  33336  bnj98  34272  bj-godellob  34540  bj-axc16b  34731  bj-dtrucor  34733  axc5sp1  35066