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  1543  ax4sp1  2113  rex0  3468  0ss  3483  abf  3488  r19.2zb  3544  ral0  3558  snsssn  3781  int0  3876  axnulALT  4147  ax16b  4202  dtrucor  4208  smo11  6381  tfrlem16  6409  omordi  6564  nnmordi  6629  omabs  6645  omsmolem  6651  0er  6695  pssnn  7081  fiint  7133  cantnfle  7372  r1sdom  7446  alephordi  7701  ackbij1lem16  7861  cfsmolem  7896  domtriomlem  8068  axdc3lem2  8077  konigthlem  8190  canthp1  8276  grur1  8442  elnnnn0b  10008  xltnegi  10543  xmulasslem2  10602  xrinfm0  10655  elixx3g  10669  elfz2  10789  uzdisj  10856  om2uzlti  11013  hashf1lem2  11394  sum0  12194  fsum2dlem  12233  exprmfct  12789  4sqlem18  13009  vdwap0  13023  ram0  13069  prmlem1a  13108  prmlem2  13121  xpsfrnel2  13467  0catg  13589  alexsub  17739  0met  17930  vitali  18968  i1f0  19042  itg2const2  19096  plyeq0  19593  jensen  20283  ppiublem1  20441  ppiublem2  20442  bposlem3  20525  bposlem9  20531  lgsdir2lem3  20564  rpvmasum  20675  pntpbnd1  20735  derangsn  23701  pconcon  23762  sltsolem1  24322  bisym1  24858  unqsym1  24864  amosym1  24865  subsym1  24866  elioo1t3  25502  hdrmp  25706  0ded  25757  0catOLD  25758  inttarcar  25901  heiborlem8  26542  psgnunilem2  27418  fveqvfvv  27987  ndmaovcl  28063  usgraedgprv  28122  bnj98  28899  dihglblem6  31530
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator