Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  pm2.21d GIF 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 (𝜑 → ¬ 𝜓)
Assertion
Ref Expression
pm2.21d (𝜑 → (𝜓𝜒))

Proof of Theorem pm2.21d
StepHypRef Expression
1 pm2.21d.1 . 2 (𝜑 → ¬ 𝜓)
2 pm2.21 589 . 2 𝜓 → (𝜓𝜒))
31, 2syl 14 1 (𝜑 → (𝜓𝜒))
 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  8716  nn0ge2m1nn  8988  elnnz  9015  elnn0z  9018  indstr  9337  indstr2  9352  xrltnsym  9519  xrlttr  9521  xrltso  9522  xrlelttr  9529  xltnegi  9558  xsubge0  9604  ixxdisj  9626  icodisj  9715  fzm1  9820  qbtwnxr  9975  frec2uzlt2d  10117  facdiv  10424  resqrexlemgt0  10732  climuni  11002  fsumcl2lem  11107  dvdsle  11438  prmdvdsexpr  11724  prmfac1  11726  sqrt2irr  11736  phibndlem  11787  isxmet2d  12412  trilpolemres  13037
 Copyright terms: Public domain W3C validator