ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  pm2.21d Unicode version

Theorem pm2.21d 582
Description: A contradiction implies anything. Deduction from pm2.21 580. (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 . 2  |-  ( ph  ->  -.  ps )
2 pm2.21 580 . 2  |-  ( -. 
ps  ->  ( ps  ->  ch ) )
31, 2syl 14 1  |-  ( ph  ->  ( ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-in2 578
This theorem is referenced by:  pm2.21dd  583  pm5.21  644  2falsed  651  mtord  730  prlem1  915  eq0rdv  3295  csbprc  3296  rzal  3346  poirr2  4747  nnsucuniel  6139  nnawordex  6167  swoord2  6202  elni2  6566  cauappcvgprlemdisj  6903  caucvgprlemdisj  6926  caucvgprprlemdisj  6954  caucvgsr  7040  lelttr  7266  nnsub  8144  nn0ge2m1nn  8415  elnnz  8442  elnn0z  8445  indstr  8762  indstr2  8777  xrltnsym  8944  xrlttr  8946  xrltso  8947  xrlelttr  8952  xltnegi  8978  ixxdisj  9002  icodisj  9090  fzm1  9193  qbtwnxr  9344  frec2uzlt2d  9486  expival  9575  facdiv  9762  resqrexlemgt0  10044  climuni  10270  dvdsle  10389  prmdvdsexpr  10673  prmfac1  10675  sqrt2irr  10685
  Copyright terms: Public domain W3C validator