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

Theorem pm2.21d 549
Description: A contradiction implies anything. Deduction from pm2.21 547. (Contributed by NM, 10-Feb-1996.)
Hypothesis
Ref Expression
pm2.21d.1
Assertion
Ref Expression
pm2.21d

Proof of Theorem pm2.21d
StepHypRef Expression
1 pm2.21d.1 . 2
2 pm2.21 547 . 2
31, 2syl 14 1
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 545
This theorem is referenced by:  pm2.21dd  550  pm5.21  610  2falsed  617  mtord  696  prlem1  879  eq0rdv  3255  csbprc  3256  rzal  3312  poirr2  4660  nnawordex  6037  swoord2  6072  elni2  6298  cauappcvgprlemdisj  6623  caucvgprlemdisj  6645  lelttr  6903  nnsub  7733  nn0ge2m1nn  8018  elnnz  8031  elnn0z  8034  indstr  8312  indstr2  8322  xrltnsym  8484  xrlttr  8486  xrltso  8487  xrlelttr  8492  xltnegi  8518  ixxdisj  8542  icodisj  8630  fzm1  8732  frec2uzlt2d  8871  expival  8911
  Copyright terms: Public domain W3C validator