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

Theorem pm2.65da 622
Description: Deduction 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 621 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 579  ax-in2 580
This theorem is referenced by:  condandc  813  nelrdva  2820  exmid01  4023  frirrg  4168  fimax2gtrilemstep  6596  unsnfidcex  6610  unsnfidcel  6611  fodjuomnilem0  6781  exmidfodomrlemr  6807  exmidfodomrlemrALT  6808  prodgt0  8285  ixxdisj  9290  icodisj  9378  iseqf1olemnab  9882  seq3f1olemqsumk  9893  ltabs  10485  divalglemnqt  11002  zsupcllemstep  11023  infssuzex  11027  sqnprm  11199  znnen  11293  peano3nninf  11543
  Copyright terms: Public domain W3C validator