ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  pm2.21d Structured version   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  610  2falsed  617  mtord  696  prlem1  879  eq0rdv  3255  csbprc  3256  rzal  3312  poirr2  4660  nnawordex  6037  swoord2  6072  elni2  6298  cauappcvgprlemdisj  6622  lelttr  6883  nnsub  7713  nn0ge2m1nn  7998  elnnz  8011  elnn0z  8014  indstr  8292  indstr2  8302  xrltnsym  8464  xrlttr  8466  xrltso  8467  xrlelttr  8472  xltnegi  8498  ixxdisj  8522  icodisj  8610  fzm1  8712  frec2uzlt2d  8851  expival  8891
  Copyright terms: Public domain W3C validator