ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  pm2.21d GIF 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  611  2falsed  618  mtord  697  prlem1  880  eq0rdv  3258  csbprc  3259  rzal  3315  poirr2  4704  nnawordex  6088  swoord2  6123  elni2  6393  cauappcvgprlemdisj  6730  caucvgprlemdisj  6753  caucvgprprlemdisj  6781  caucvgsr  6867  lelttr  7086  nnsub  7928  nn0ge2m1nn  8214  elnnz  8227  elnn0z  8230  indstr  8508  indstr2  8518  xrltnsym  8681  xrlttr  8683  xrltso  8684  xrlelttr  8689  xltnegi  8715  ixxdisj  8739  icodisj  8827  fzm1  8929  frec2uzlt2d  9068  expival  9135  resqrexlemgt0  9496  climuni  9691  sqrt2irr  9755
  Copyright terms: Public domain W3C validator