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  1675  rex0  3782  0ss  3797  abf  3802  r19.2zb  3893  ral0  3908  rabsnifsb  4071  snsssn  4171  int0  4272  axnulALT  4554  axc16b  4617  dtrucor  4655  bropopvvv  6887  tfrlem16  7119  omordi  7275  nnmordi  7340  omabs  7356  omsmolem  7362  0er  7406  pssnn  7796  fiint  7854  cantnfle  8175  r1sdom  8244  alephordi  8503  axdc3lem2  8879  canthp1  9078  elnnnn0b  10914  xltnegi  11509  xmulasslem2  11568  xrinf0  11623  xrinfm0OLD  11627  elixx3g  11648  elfz2  11789  om2uzlti  12161  hashf1lem2  12614  sum0  13765  fsum2dlem  13809  prod0  13975  fprod2dlem  14012  exprmfct  14619  4sqlem18OLD  14869  4sqlem18  14875  vdwap0  14889  ram0  14943  prmlem1a  15041  prmlem2  15054  xpsfrnel2  15422  0catg  15544  alexsub  20991  0met  21312  vitali  22448  plyeq0  23033  jensen  23779  ppiublem1  23993  ppiublem2  23994  lgsdir2lem3  24116  rpvmasum  24227  usgraedgprv  24949  4cycl4dv  25240  clwwlknprop  25345  2wlkonot3v  25448  2spthonot3v  25449  frgrareggt1  25689  topnfbey  25751  isarchi  28337  sibf0  28995  sgn3da  29200  sgnnbi  29204  sgnpbi  29205  signstfvneq0  29249  bnj98  29466  sltsolem1  30342  bisym1  30864  unqsym1  30870  amosym1  30871  subsym1  30872  bj-godellob  30972  bj-axc16b  31164  bj-dtrucor  31166  poimirlem30  31673  axc5sp1  32202  areaquad  35799  fiiuncl  37047  iblempty  37410  fveqvfvv  38015  ndmaovcl  38094  sgoldbaltlem1  38269  bgoldbtbndlem1  38289  nn0enne  39086