MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.21i 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  1334  nfnth  1562  ax4sp1  2201  rex0  3577  0ss  3592  abf  3597  r19.2zb  3654  ral0  3668  snsssn  3902  int0  3999  axnulALT  4270  dtrucor  4331  bropopvvv  6358  tfrlem16  6583  omordi  6738  nnmordi  6803  omabs  6819  omsmolem  6825  0er  6869  pssnn  7256  fiint  7312  cantnfle  7552  r1sdom  7626  alephordi  7881  axdc3lem2  8257  canthp1  8455  elnnnn0b  10189  xltnegi  10727  xmulasslem2  10786  xrinfm0  10840  elixx3g  10854  elfz2  10975  om2uzlti  11210  hashf1lem2  11625  sum0  12435  fsum2dlem  12474  exprmfct  13030  4sqlem18  13250  vdwap0  13264  ram0  13310  prmlem1a  13349  prmlem2  13362  xpsfrnel2  13710  0catg  13832  alexsub  17990  0met  18297  vitali  19365  plyeq0  19990  jensen  20687  ppiublem1  20846  ppiublem2  20847  lgsdir2lem3  20969  rpvmasum  21080  usgraedgprv  21256  4cycl4dv  21495  prod0  25041  sltsolem1  25339  bisym1  25876  unqsym1  25882  amosym1  25883  subsym1  25884  itg2addnc  25952  fveqvfvv  27650  ndmaovcl  27729  bnj98  28569  ax7w7AUX7  28978
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator