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

Theorem pm2.21d 620
Description: A contradiction implies anything. Deduction from pm2.21 618. (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 618 . 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 616
This theorem is referenced by:  pm2.21dd  621  pm5.21  696  2falsed  703  mtord  784  prlem1  975  eq0rdv  3504  csbprc  3505  rzal  3557  poirr2  5072  nnsucuniel  6571  nnawordex  6605  swoord2  6640  difinfsnlem  7183  exmidomni  7226  elni2  7409  cauappcvgprlemdisj  7746  caucvgprlemdisj  7769  caucvgprprlemdisj  7797  caucvgsr  7897  lelttr  8143  nnsub  9057  nn0ge2m1nn  9337  elnnz  9364  elnn0z  9367  indstr  9696  indstr2  9712  xrltnsym  9897  xrlttr  9899  xrltso  9900  xrlelttr  9910  xltnegi  9939  xsubge0  9985  ixxdisj  10007  icodisj  10096  fzm1  10204  qbtwnxr  10381  frec2uzlt2d  10530  nn0ltexp2  10835  facdiv  10864  resqrexlemgt0  11250  climuni  11523  fsumcl2lem  11628  dvdsle  12074  prmdvdsexpr  12391  prmfac1  12393  sqrt2irr  12403  phibndlem  12457  dvdsprmpweqle  12579  isxmet2d  14738  lgsdir2lem2  15424  lgseisenlem2  15466  trilpolemres  15845
  Copyright terms: Public domain W3C validator