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

Theorem pm2.21i 123
Description: A contradiction implies anything. Inference from pm2.21 100. (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 10 . 2  |-  ( -. 
ps  ->  -.  ph )
32con4i 122 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  pm2.24ii  124  pm3.2ni  827  falim  1328  nfnth  1556  ax4sp1  2179  rex0  3544  0ss  3559  abf  3564  r19.2zb  3620  ral0  3634  snsssn  3860  int0  3955  axnulALT  4226  ax16b  4281  dtrucor  4287  smo11  6465  tfrlem16  6493  omordi  6648  nnmordi  6713  omabs  6729  omsmolem  6735  0er  6779  pssnn  7166  fiint  7220  cantnfle  7459  r1sdom  7533  alephordi  7788  ackbij1lem16  7948  cfsmolem  7983  domtriomlem  8155  axdc3lem2  8164  konigthlem  8277  canthp1  8363  grur1  8529  elnnnn0b  10097  xltnegi  10632  xmulasslem2  10691  xrinfm0  10744  elixx3g  10758  elfz2  10878  uzdisj  10945  om2uzlti  11102  hashf1lem2  11484  sum0  12285  fsum2dlem  12324  exprmfct  12880  4sqlem18  13100  vdwap0  13114  ram0  13160  prmlem1a  13199  prmlem2  13212  xpsfrnel2  13560  0catg  13682  alexsub  17835  0met  18026  vitali  19066  i1f0  19140  itg2const2  19194  plyeq0  19691  jensen  20388  ppiublem1  20547  ppiublem2  20548  bposlem3  20631  bposlem9  20637  lgsdir2lem3  20670  rpvmasum  20781  pntpbnd1  20841  derangsn  24105  pconcon  24166  prod0  24570  sltsolem1  24880  bisym1  25417  unqsym1  25423  amosym1  25424  subsym1  25425  itg2addnc  25494  heiborlem8  25865  psgnunilem2  26741  fveqvfvv  27312  ndmaovcl  27391  bropopvvv  27432  usgraedgprv  27543  4cycl4dv  27774  bnj98  28644  ax7w7AUX7  29053  dihglblem6  31582
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator