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  1319  nfnth  1546  ax4sp1  2126  rex0  3481  0ss  3496  abf  3501  r19.2zb  3557  ral0  3571  snsssn  3797  int0  3892  axnulALT  4163  ax16b  4218  dtrucor  4224  smo11  6397  tfrlem16  6425  omordi  6580  nnmordi  6645  omabs  6661  omsmolem  6667  0er  6711  pssnn  7097  fiint  7149  cantnfle  7388  r1sdom  7462  alephordi  7717  ackbij1lem16  7877  cfsmolem  7912  domtriomlem  8084  axdc3lem2  8093  konigthlem  8206  canthp1  8292  grur1  8458  elnnnn0b  10024  xltnegi  10559  xmulasslem2  10618  xrinfm0  10671  elixx3g  10685  elfz2  10805  uzdisj  10872  om2uzlti  11029  hashf1lem2  11410  sum0  12210  fsum2dlem  12249  exprmfct  12805  4sqlem18  13025  vdwap0  13039  ram0  13085  prmlem1a  13124  prmlem2  13137  xpsfrnel2  13483  0catg  13605  alexsub  17755  0met  17946  vitali  18984  i1f0  19058  itg2const2  19112  plyeq0  19609  jensen  20299  ppiublem1  20457  ppiublem2  20458  bposlem3  20541  bposlem9  20547  lgsdir2lem3  20580  rpvmasum  20691  pntpbnd1  20751  derangsn  23716  pconcon  23777  cprod0  24168  sltsolem1  24393  bisym1  24930  unqsym1  24936  amosym1  24937  subsym1  24938  itg2addnc  25005  elioo1t3  25605  hdrmp  25809  0ded  25860  0catOLD  25861  inttarcar  26004  heiborlem8  26645  psgnunilem2  27521  fveqvfvv  28092  ndmaovcl  28171  usgraedgprv  28256  trlonprop  28341  4cycl4dv  28413  bnj98  29215  ax7w7AUX7  29623  dihglblem6  32152
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator