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

Theorem pm2.21d 619
Description: A contradiction implies anything. Deduction from pm2.21 617. (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 617 . 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 615
This theorem is referenced by:  pm2.21dd  620  pm5.21  695  2falsed  702  mtord  783  prlem1  973  eq0rdv  3467  csbprc  3468  rzal  3520  poirr2  5017  nnsucuniel  6490  nnawordex  6524  swoord2  6559  difinfsnlem  7092  exmidomni  7134  elni2  7301  cauappcvgprlemdisj  7638  caucvgprlemdisj  7661  caucvgprprlemdisj  7689  caucvgsr  7789  lelttr  8033  nnsub  8944  nn0ge2m1nn  9222  elnnz  9249  elnn0z  9252  indstr  9579  indstr2  9595  xrltnsym  9777  xrlttr  9779  xrltso  9780  xrlelttr  9790  xltnegi  9819  xsubge0  9865  ixxdisj  9887  icodisj  9976  fzm1  10083  qbtwnxr  10241  frec2uzlt2d  10387  nn0ltexp2  10671  facdiv  10699  resqrexlemgt0  11010  climuni  11282  fsumcl2lem  11387  dvdsle  11830  prmdvdsexpr  12130  prmfac1  12132  sqrt2irr  12142  phibndlem  12196  dvdsprmpweqle  12316  isxmet2d  13512  lgsdir2lem2  14094  trilpolemres  14443
  Copyright terms: Public domain W3C validator