Theorem pm2.21i 136

Description: A contradiction implies anything. Inference associated with pm2.21 111. Its associated inference is pm2.24ii 137. (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 135	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  137  pm2.21dd  179  pm3.2ni  872  falim  1466  nfnth  1687  rex0  3737  0ss  3766  r19.2zb  3850  ral0  3865  rabsnifsb  4031  snsssn  4132  int0  4240  axnulALT  4524  axc16b  4593  dtrucor  4633  brfvopab  6355  bropopvvv  6893  bropfvvvv  6895  tfrlem16  7129  omordi  7285  nnmordi  7350  omabs  7366  omsmolem  7372  0er  7416  pssnn  7808  fiint  7866  cantnfle  8194  r1sdom  8263  alephordi  8523  axdc3lem2  8899  canthp1  9097  elnnnn0b  10938  xltnegi  11532  xmulasslem2  11593  xrinf0  11648  xrinfm0OLD  11652  elixx3g  11673  elfz2  11817  om2uzlti  12202  hashf1lem2  12660  sum0  13864  fsum2dlem  13908  prod0  14074  fprod2dlem  14111  exprmfct  14727  4sqlem18OLD  14985  4sqlem18  14991  vdwap0  15005  ram0  15059  prmlem1a  15156  prmlem2  15169  xpsfrnel2  15549  0catg  15671  alexsub  21138  0met  21459  vitali  22650  plyeq0  23244  jensen  23993  ppiublem1  24209  ppiublem2  24210  lgsdir2lem3  24332  rpvmasum  24443  usgraedgprv  25182  4cycl4dv  25474  clwwlknprop  25579  2wlkonot3v  25682  2spthonot3v  25683  frgrareggt1  25923  topnfbey  25985  isarchi  28573  sibf0  29240  sgn3da  29485  sgnnbi  29489  sgnpbi  29490  signstfvneq0  29533  bnj98  29750  sltsolem1  30628  bisym1  31150  unqsym1  31156  amosym1  31157  subsym1  31158  bj-godellob  31253  bj-axc16b  31479  bj-dtrucor  31481  poimirlem30  32034  axc5sp1  32558  areaquad  36172  fiiuncl  37465  iblempty  37939  fveqvfvv  38770  ndmaovcl  38850  sgoldbaltlem1  39025  bgoldbtbndlem1  39045  xnn0xadd0  39238  vtxdg0v  39698  wlkbProp  39819  nn0enne  40834