Theorem pm2.21i 134

Description: A contradiction implies anything. Inference associated with pm2.21 111. Its associated inference is pm2.24ii 135. (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 133	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  135  pm2.21dd  177  pm3.2ni  862  falim  1451  nfnth  1673  rex0  3719  0ss  3736  abf  3741  r19.2zb  3832  ral0  3847  rabsnifsb  4011  snsssn  4111  int0  4212  axnulALT  4495  axc16b  4559  dtrucor  4597  bropopvvv  6831  tfrlem16  7066  omordi  7222  nnmordi  7287  omabs  7303  omsmolem  7309  0er  7353  pssnn  7743  fiint  7801  cantnfle  8128  r1sdom  8197  alephordi  8456  axdc3lem2  8832  canthp1  9030  elnnnn0b  10865  xltnegi  11460  xmulasslem2  11519  xrinf0  11574  xrinfm0OLD  11578  elixx3g  11599  elfz2  11742  om2uzlti  12114  hashf1lem2  12567  sum0  13730  fsum2dlem  13774  prod0  13940  fprod2dlem  13977  exprmfct  14591  4sqlem18OLD  14849  4sqlem18  14855  vdwap0  14869  ram0  14923  prmlem1a  15021  prmlem2  15034  xpsfrnel2  15414  0catg  15536  alexsub  21002  0met  21323  vitali  22513  plyeq0  23107  jensen  23856  ppiublem1  24072  ppiublem2  24073  lgsdir2lem3  24195  rpvmasum  24306  usgraedgprv  25045  4cycl4dv  25337  clwwlknprop  25442  2wlkonot3v  25545  2spthonot3v  25546  frgrareggt1  25786  topnfbey  25848  isarchi  28450  sibf0  29119  sgn3da  29364  sgnnbi  29368  sgnpbi  29369  signstfvneq0  29413  bnj98  29630  sltsolem1  30506  bisym1  31028  unqsym1  31034  amosym1  31035  subsym1  31036  bj-godellob  31137  bj-axc16b  31324  bj-dtrucor  31326  poimirlem30  31877  axc5sp1  32406  areaquad  36014  fiiuncl  37322  iblempty  37725  fveqvfvv  38439  ndmaovcl  38518  sgoldbaltlem1  38693  bgoldbtbndlem1  38713  nn0enne  39929