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

Theorem pm2.65da 650
 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 114 . 2 (𝜑 → (𝜓𝜒))
3 pm2.65da.2 . . 3 ((𝜑𝜓) → ¬ 𝜒)
43ex 114 . 2 (𝜑 → (𝜓 → ¬ 𝜒))
52, 4pm2.65d 649 1 (𝜑 → ¬ 𝜓)
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107  ax-in1 603  ax-in2 604 This theorem is referenced by:  condandc  866  nelrdva  2891  exmid01  4121  frirrg  4272  fimax2gtrilemstep  6794  unsnfidcex  6808  unsnfidcel  6809  difinfsn  6985  fodju0  7019  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059  ltntri  7890  prodgt0  8610  ixxdisj  9686  icodisj  9775  iseqf1olemnab  10261  seq3f1olemqsumk  10272  ltabs  10859  divalglemnqt  11617  zsupcllemstep  11638  infssuzex  11642  sqnprm  11816  znnen  11911  dedekindeulemuub  12764  dedekindeulemlu  12768  dedekindicclemuub  12773  dedekindicclemlu  12777  ivthinclemlopn  12783  ivthinclemuopn  12785  limcimo  12803  cnplimclemle  12806  pilem3  12864  pwtrufal  13192  pwle2  13193  peano3nninf  13201  nninffeq  13216  refeq  13223  trilpolemeq1  13233  taupi  13239
 Copyright terms: Public domain W3C validator