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

Theorem pm2.21d 582
Description: A contradiction implies anything. Deduction from pm2.21 580. (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 580 . 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 578
This theorem is referenced by:  pm2.21dd  583  pm5.21  644  2falsed  651  mtord  730  prlem1  917  eq0rdv  3315  csbprc  3316  rzal  3366  poirr2  4791  nnsucuniel  6210  nnawordex  6239  swoord2  6274  exmidomni  6742  elni2  6817  cauappcvgprlemdisj  7154  caucvgprlemdisj  7177  caucvgprprlemdisj  7205  caucvgsr  7291  lelttr  7517  nnsub  8395  nn0ge2m1nn  8666  elnnz  8693  elnn0z  8696  indstr  9013  indstr2  9028  xrltnsym  9195  xrlttr  9197  xrltso  9198  xrlelttr  9203  xltnegi  9229  ixxdisj  9253  icodisj  9341  fzm1  9444  qbtwnxr  9597  frec2uzlt2d  9739  expival  9856  facdiv  10043  resqrexlemgt0  10349  climuni  10576  fsumcl2lem  10677  dvdsle  10727  prmdvdsexpr  11011  prmfac1  11013  sqrt2irr  11023  phibndlem  11074
  Copyright terms: Public domain W3C validator