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

Theorem mtoi 590
 Description: Modus tollens inference. (Contributed by NM, 5-Jul-1994.) (Proof shortened by Wolf Lammen, 15-Sep-2012.)
Hypotheses
Ref Expression
mtoi.1 ¬ 𝜒
mtoi.2 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
mtoi (𝜑 → ¬ 𝜓)

Proof of Theorem mtoi
StepHypRef Expression
1 mtoi.1 . . 3 ¬ 𝜒
21a1i 9 . 2 (𝜑 → ¬ 𝜒)
3 mtoi.2 . 2 (𝜑 → (𝜓𝜒))
42, 3mtod 589 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-in1 544  ax-in2 545 This theorem is referenced by:  mtbii  599  mtbiri  600  pwnss  3912  nsuceq0g  4155  reg2exmidlema  4259  ordsuc  4287  onnmin  4292  ssnel  4293  onpsssuc  4295  ordtri2or2exmid  4296  reg3exmidlemwe  4303  acexmidlemab  5506  reldmtpos  5868  dmtpos  5871  2pwuninelg  5898  onunsnss  6355  snon0  6356  ltexprlemdisj  6704  recexprlemdisj  6728  caucvgprlemnkj  6764  caucvgprprlemnkltj  6787  caucvgprprlemnkeqj  6788  caucvgprprlemnjltk  6789  inelr  7575  rimul  7576  recgt0  7816
 Copyright terms: Public domain W3C validator