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  2250  rex0  3633  0ss  3648  abf  3653  r19.2zb  3710  ral0  3724  snsssn  3959  int0  4056  axnulALT  4328  ax16b  4383  dtrucor  4389  bropopvvv  6418  tfrlem16  6646  omordi  6801  nnmordi  6866  omabs  6882  omsmolem  6888  0er  6932  pssnn  7319  fiint  7375  cantnfle  7618  r1sdom  7692  alephordi  7947  axdc3lem2  8323  canthp1  8521  elnnnn0b  10256  xltnegi  10794  xmulasslem2  10853  xrinfm0  10907  elixx3g  10921  elfz2  11042  om2uzlti  11282  hashf1lem2  11697  sum0  12507  fsum2dlem  12546  exprmfct  13102  4sqlem18  13322  vdwap0  13336  ram0  13382  prmlem1a  13421  prmlem2  13434  xpsfrnel2  13782  0catg  13904  alexsub  18068  0met  18388  vitali  19497  plyeq0  20122  jensen  20819  ppiublem1  20978  ppiublem2  20979  lgsdir2lem3  21101  rpvmasum  21212  usgraedgprv  21388  4cycl4dv  21646  isarchi  24244  sibf0  24641  prod0  25261  fprod2dlem  25296  sltsolem1  25615  bisym1  26161  unqsym1  26167  amosym1  26168  subsym1  26169  fveqvfvv  27955  ndmaovcl  28034  2wlkonot3v  28295  2spthonot3v  28296  bnj98  29175  ax7w7AUX7  29590  ax7w11AUX7  29600
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator