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

Theorem pm2.21d 557
Description: A contradiction implies anything. Deduction from pm2.21 555. (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 555 . 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 553
This theorem is referenced by:  pm2.21dd  558  pm5.21  619  2falsed  626  mtord  705  prlem1  889  eq0rdv  3286  csbprc  3287  rzal  3343  poirr2  4742  nnawordex  6129  swoord2  6164  elni2  6440  cauappcvgprlemdisj  6777  caucvgprlemdisj  6800  caucvgprprlemdisj  6828  caucvgsr  6914  lelttr  7135  nnsub  7998  nn0ge2m1nn  8269  elnnz  8282  elnn0z  8285  indstr  8602  indstr2  8613  xrltnsym  8785  xrlttr  8787  xrltso  8788  xrlelttr  8793  xltnegi  8819  ixxdisj  8843  icodisj  8931  fzm1  9034  frec2uzlt2d  9319  expival  9387  facdiv  9570  resqrexlemgt0  9810  climuni  10008  dvdsle  10119  sqrt2irr  10194
  Copyright terms: Public domain W3C validator