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

Theorem pm2.65da 620
Description: Deduction rule for proof by contradiction. (Contributed by NM, 12-Jun-2014.)
Hypotheses
Ref Expression
pm2.65da.1 ((𝜑𝜓) → 𝜒)
pm2.65da.2 ((𝜑𝜓) → ¬ 𝜒)
Assertion
Ref Expression
pm2.65da (𝜑 → ¬ 𝜓)

Proof of Theorem pm2.65da
StepHypRef Expression
1 pm2.65da.1 . . 3 ((𝜑𝜓) → 𝜒)
21ex 113 . 2 (𝜑 → (𝜓𝜒))
3 pm2.65da.2 . . 3 ((𝜑𝜓) → ¬ 𝜒)
43ex 113 . 2 (𝜑 → (𝜓 → ¬ 𝜒))
52, 4pm2.65d 619 1 (𝜑 → ¬ 𝜓)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106  ax-in1 577  ax-in2 578
This theorem is referenced by:  condandc  809  nelrdva  2808  exmid01  3996  frirrg  4141  unsnfidcex  6557  unsnfidcel  6558  fodjuomnilem0  6707  exmidfodomrlemr  6731  exmidfodomrlemrALT  6732  prodgt0  8207  ixxdisj  9216  icodisj  9304  ltabs  10347  divalglemnqt  10700  zsupcllemstep  10721  infssuzex  10725  sqnprm  10897  znnen  10991  nnsn0  11238
  Copyright terms: Public domain W3C validator