MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.21i Structured version   Unicode version

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
StepHypRef Expression
1 pm2.21i.1 . . 3  |-  -.  ph
21a1i 11 . 2  |-  ( -. 
ps  ->  -.  ph )
32con4i 124 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  pm2.24ii  126  pm3.2ni  828  falim  1337  nfnth  1565  ax4sp1  2251  rex0  3641  0ss  3656  abf  3661  r19.2zb  3718  ral0  3732  snsssn  3967  int0  4064  axnulALT  4336  ax16b  4391  dtrucor  4397  bropopvvv  6426  tfrlem16  6654  omordi  6809  nnmordi  6874  omabs  6890  omsmolem  6896  0er  6940  pssnn  7327  fiint  7383  cantnfle  7626  r1sdom  7700  alephordi  7955  axdc3lem2  8331  canthp1  8529  elnnnn0b  10264  xltnegi  10802  xmulasslem2  10861  xrinfm0  10915  elixx3g  10929  elfz2  11050  om2uzlti  11290  hashf1lem2  11705  sum0  12515  fsum2dlem  12554  exprmfct  13110  4sqlem18  13330  vdwap0  13344  ram0  13390  prmlem1a  13429  prmlem2  13442  xpsfrnel2  13790  0catg  13912  alexsub  18076  0met  18396  vitali  19505  plyeq0  20130  jensen  20827  ppiublem1  20986  ppiublem2  20987  lgsdir2lem3  21109  rpvmasum  21220  usgraedgprv  21396  4cycl4dv  21654  isarchi  24252  sibf0  24649  prod0  25269  fprod2dlem  25304  sltsolem1  25623  bisym1  26169  unqsym1  26175  amosym1  26176  subsym1  26177  fveqvfvv  27964  ndmaovcl  28043  2wlkonot3v  28342  2spthonot3v  28343  bnj98  29238  ax7w7AUX7  29653  ax7w11AUX7  29663
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator