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  2960  eq0rdv  3450  rzal  3516  reusv2lem2  4494  dfwe2  4531  tfindsg  4609  findsg  4641  poirr2  5041  sofld  5095  omopth2  6536  swoord2  6644  unxpdomlem3  7023  suc11reg  7274  wemapwe  7354  r111  7401  r1pwss  7410  cflim2  7843  axunndlem1  8171  axunnd  8172  axpowndlem3  8175  axpownd  8177  axregndlem1  8178  axregndlem2  8179  axinfndlem1  8181  axinfnd  8182  axacndlem1  8183  axacndlem2  8184  axacndlem3  8185  axacndlem4  8186  axacndlem5  8187  axacnd  8188  fpwwe2lem13  8218  gchpwdom  8250  winalim2  8272  ltapr  8623  prodgt0  9555  squeeze0  9613  nnsub  9738  nn0sub  9967  elnnz  9987  indstr2  10249  uzsupss  10263  xrltnsym  10424  xrlttr  10427  qbtwnxr  10479  xltnegi  10495  xmullem  10536  xlemul1a  10560  xrsupsslem  10577  xrinfmsslem  10578  xrub  10582  xrsup0  10594  xrinfm0  10607  ixxdisj  10623  icodisj  10713  facdiv  11252  climuni  11977  rlimno1  12078  sqr2irr  12475  prmdvdsexpr  12743  prmfac1  12745  ramlb  13014  ram0  13017  prmlem1  13057  prmlem2  13069  pospo  14055  symgbas  14720  efgredlemc  15002  efgred  15005  psrvscafval  16083  prmirred  16396  0top  16669  pnfnei  16898  mnfnei  16899  cmpfi  17083  1stccnp  17136  filcon  17526  nmoleub2lem3  18544  ivthlem2  18760  ivthlem3  18761  ovolicc2lem3  18826  itg1addlem4  19002  itg2seq  19045  dvcnvlem  19271  lhop2  19310  bpos1  20470  lgsdir2lem2  20511  lgsqrlem2  20529  lgseisenlem2  20537  pntlem3  20706  ostth3  20735  ifeqeqx  22980  erdszelem4  23083  erdszelem8  23087  axlowdimlem15  23945  ordcmp  24247  nbssntrs  25500  finminlem  25584  nn0prpwlem  25591  nn0prpw  25592  smprngopr  26030  prtlem14  26095  jm2.23  26442  sdrgacs  26862  rzalf  27042  ax12-2  28254  a12stdy4  28280  lkrpssN  28504  atltcvr  28775  cdleme27a  29707  dihord6apre  30597  dihord6b  30601
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator