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

Theorem pm2.21d 100
Description: A contradiction implies anything. Deduction from pm2.21 102. (Contributed by NM, 10-Feb-1996.)
Hypothesis
Ref Expression
pm2.21d.1  |-  ( ph  ->  -.  ps )
Assertion
Ref Expression
pm2.21d  |-  ( ph  ->  ( ps  ->  ch ) )

Proof of Theorem pm2.21d
StepHypRef Expression
1 pm2.21d.1 . . 3  |-  ( ph  ->  -.  ps )
21a1d 24 . 2  |-  ( ph  ->  ( -.  ch  ->  -. 
ps ) )
32con4d 99 1  |-  ( ph  ->  ( ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6
This theorem is referenced by:  pm2.21dd  101  pm2.21  102  2falsed  342  pm5.14  861  ecase2d  911  prlem1  933  sbc2or  2943  eq0rdv  3431  rzal  3497  reusv2lem2  4473  dfwe2  4510  tfindsg  4588  findsg  4620  poirr2  5020  sofld  5074  omopth2  6515  swoord2  6623  unxpdomlem3  7002  suc11reg  7253  wemapwe  7333  r111  7380  r1pwss  7389  cflim2  7822  axunndlem1  8150  axunnd  8151  axpowndlem3  8154  axpownd  8156  axregndlem1  8157  axregndlem2  8158  axinfndlem1  8160  axinfnd  8161  axacndlem1  8162  axacndlem2  8163  axacndlem3  8164  axacndlem4  8165  axacndlem5  8166  axacnd  8167  fpwwe2lem13  8197  gchpwdom  8229  winalim2  8251  ltapr  8602  prodgt0  9534  squeeze0  9592  nnsub  9717  nn0sub  9946  elnnz  9966  indstr2  10228  uzsupss  10242  xrltnsym  10403  xrlttr  10406  qbtwnxr  10458  xltnegi  10474  xmullem  10515  xlemul1a  10539  xrsupsslem  10556  xrinfmsslem  10557  xrub  10561  xrsup0  10573  xrinfm0  10586  ixxdisj  10602  icodisj  10692  facdiv  11231  climuni  11956  rlimno1  12057  sqr2irr  12454  prmdvdsexpr  12722  prmfac1  12724  ramlb  12993  ram0  12996  prmlem1  13036  prmlem2  13048  pospo  14034  symgbas  14699  efgredlemc  14981  efgred  14984  psrvscafval  16062  prmirred  16375  0top  16648  pnfnei  16877  mnfnei  16878  cmpfi  17062  1stccnp  17115  filcon  17505  nmoleub2lem3  18523  ivthlem2  18739  ivthlem3  18740  ovolicc2lem3  18805  itg1addlem4  18981  itg2seq  19024  dvcnvlem  19250  lhop2  19289  bpos1  20449  lgsdir2lem2  20490  lgsqrlem2  20508  lgseisenlem2  20516  pntlem3  20685  ostth3  20714  ifeqeqx  22959  erdszelem4  23062  erdszelem8  23066  axlowdimlem15  23924  ordcmp  24226  nbssntrs  25479  finminlem  25563  nn0prpwlem  25570  nn0prpw  25571  smprngopr  26009  prtlem14  26074  jm2.23  26421  sdrgacs  26841  rzalf  27021  ax12-2  28233  a12stdy4  28259  lkrpssN  28483  atltcvr  28754  cdleme27a  29686  dihord6apre  30576  dihord6b  30580
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator