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

Theorem pm2.21d 98
Description: A contradiction implies anything. Deduction from pm2.21 100. (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 22 . 2  |-  ( ph  ->  ( -.  ch  ->  -. 
ps ) )
32con4d 97 1  |-  ( ph  ->  ( ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  pm2.21dd  99  pm2.21  100  2falsed  340  pm5.14  856  ecase2d  906  prlem1  928  sbc2or  3000  eq0rdv  3490  rzal  3556  reusv2lem2  4535  dfwe2  4572  tfindsg  4650  findsg  4682  poirr2  5066  sofld  5120  omopth2  6578  swoord2  6686  unxpdomlem3  7065  suc11reg  7316  wemapwe  7396  r111  7443  r1pwss  7452  cflim2  7885  axunndlem1  8213  axunnd  8214  axpowndlem3  8217  axpownd  8219  axregndlem1  8220  axregndlem2  8221  axinfndlem1  8223  axinfnd  8224  axacndlem1  8225  axacndlem2  8226  axacndlem3  8227  axacndlem4  8228  axacndlem5  8229  axacnd  8230  fpwwe2lem13  8260  gchpwdom  8292  winalim2  8314  ltapr  8665  prodgt0  9597  squeeze0  9655  nnsub  9780  nn0sub  10010  elnnz  10030  indstr2  10292  uzsupss  10306  xrltnsym  10467  xrlttr  10470  qbtwnxr  10523  xltnegi  10539  xmullem  10580  xlemul1a  10604  xrsupsslem  10621  xrinfmsslem  10622  xrub  10626  xrsup0  10638  xrinfm0  10651  ixxdisj  10667  icodisj  10757  facdiv  11296  climuni  12022  rlimno1  12123  sqr2irr  12523  prmdvdsexpr  12791  prmfac1  12793  ramlb  13062  ram0  13065  prmlem1  13105  prmlem2  13117  pospo  14103  symgbas  14768  efgredlemc  15050  efgred  15053  psrvscafval  16131  prmirred  16444  0top  16717  pnfnei  16946  mnfnei  16947  cmpfi  17131  1stccnp  17184  filcon  17574  nmoleub2lem3  18592  ivthlem2  18808  ivthlem3  18809  ovolicc2lem3  18874  itg1addlem4  19050  itg2seq  19093  dvcnvlem  19319  lhop2  19358  bpos1  20518  lgsdir2lem2  20559  lgsqrlem2  20577  lgseisenlem2  20585  pntlem3  20754  ostth3  20783  ifeqeqx  23030  erdszelem4  23132  erdszelem8  23136  axlowdimlem15  23994  ordcmp  24296  nbssntrs  25558  finminlem  25642  nn0prpwlem  25649  nn0prpw  25650  smprngopr  26088  prtlem14  26153  jm2.23  26500  sdrgacs  26920  rzalf  27099  ax12-2  28382  a12stdy4  28408  lkrpssN  28632  atltcvr  28903  cdleme27a  29835  dihord6apre  30725  dihord6b  30729
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator