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

Theorem mtbiri 675
Description: An inference from a biconditional, similar to modus tollens. (Contributed by NM, 24-Aug-1995.)
Hypotheses
Ref Expression
mtbiri.min ¬ 𝜒
mtbiri.maj (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
mtbiri (𝜑 → ¬ 𝜓)

Proof of Theorem mtbiri
StepHypRef Expression
1 mtbiri.min . 2 ¬ 𝜒
2 mtbiri.maj . . 3 (𝜑 → (𝜓𝜒))
32biimpd 144 . 2 (𝜑 → (𝜓𝜒))
41, 3mtoi 664 1 (𝜑 → ¬ 𝜓)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-in1 614  ax-in2 615
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  nel02  3427  n0i  3428  axnul  4125  intexr  4147  intnexr  4148  iin0r  4166  exmid01  4195  ordtriexmidlem  4514  ordtriexmidlem2  4515  ordtri2or2exmidlem  4521  onsucelsucexmidlem  4524  sucprcreg  4544  preleq  4550  reg3exmidlemwe  4574  dcextest  4576  nn0eln0  4615  0nelelxp  4651  canth  5822  tfrlemisucaccv  6319  nnsucuniel  6489  nndceq  6493  nndcel  6494  2dom  6798  snnen2oprc  6853  snexxph  6942  elfi2  6964  djune  7070  updjudhcoinrg  7073  omp1eomlem  7086  nnnninfeq  7119  ismkvnex  7146  mkvprop  7149  omniwomnimkv  7158  nninfwlpoimlemginf  7167  exmidfodomrlemrALT  7195  exmidaclem  7200  elni2  7291  ltsopi  7297  ltsonq  7375  renepnf  7982  renemnf  7983  lt0ne0d  8447  sup3exmid  8890  nnne0  8923  nn0ge2m1nn  9212  nn0nepnf  9223  xrltnr  9753  pnfnlt  9761  nltmnf  9762  xrltnsym  9767  xrlttri3  9771  nltpnft  9788  ngtmnft  9791  xrrebnd  9793  xrpnfdc  9816  xrmnfdc  9817  xsubge0  9855  xposdif  9856  xleaddadd  9861  fzpreddisj  10044  fzm1  10073  exfzdc  10213  xrbdtri  11255  m1exp1  11876  3prm  12098  prmdc  12100  pcgcd1  12297  pc2dvds  12299  pcmpt  12311  exmidunben  12397  unct  12413  blssioo  13678  pilem3  13837  lgsval2lem  14044  bj-charfunbi  14185  bj-intexr  14282  bj-intnexr  14283  subctctexmid  14373  nninfsellemeq  14386  exmidsbthrlem  14393
  Copyright terms: Public domain W3C validator