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

Theorem pm2.21d 591
Description: A contradiction implies anything. Deduction from pm2.21 589. (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 589 . 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-mp 5  ax-1 6  ax-2 7  ax-in2 587
This theorem is referenced by:  pm2.21dd  592  pm5.21  667  2falsed  674  mtord  755  prlem1  940  eq0rdv  3375  csbprc  3376  rzal  3428  poirr2  4899  nnsucuniel  6357  nnawordex  6390  swoord2  6425  difinfsnlem  6950  exmidomni  6980  elni2  7086  cauappcvgprlemdisj  7423  caucvgprlemdisj  7446  caucvgprprlemdisj  7474  caucvgsr  7574  lelttr  7816  nnsub  8719  nn0ge2m1nn  8991  elnnz  9018  elnn0z  9021  indstr  9340  indstr2  9355  xrltnsym  9530  xrlttr  9532  xrltso  9533  xrlelttr  9540  xltnegi  9569  xsubge0  9615  ixxdisj  9637  icodisj  9726  fzm1  9831  qbtwnxr  9986  frec2uzlt2d  10128  facdiv  10435  resqrexlemgt0  10743  climuni  11013  fsumcl2lem  11118  dvdsle  11449  prmdvdsexpr  11735  prmfac1  11737  sqrt2irr  11747  phibndlem  11798  isxmet2d  12423  trilpolemres  13069
  Copyright terms: Public domain W3C validator