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

Theorem mtbiri 664
 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 143 . 2 (𝜑 → (𝜓𝜒))
41, 3mtoi 653 1 (𝜑 → ¬ 𝜓)
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 104 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-in1 603  ax-in2 604 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  n0i  3368  axnul  4056  intexr  4078  intnexr  4079  iin0r  4096  exmid01  4124  ordtriexmidlem  4438  ordtriexmidlem2  4439  ordtri2or2exmidlem  4444  onsucelsucexmidlem  4447  sucprcreg  4467  preleq  4473  reg3exmidlemwe  4496  dcextest  4498  nn0eln0  4536  0nelelxp  4571  tfrlemisucaccv  6225  nnsucuniel  6394  nndceq  6398  nndcel  6399  2dom  6702  snnen2oprc  6757  snexxph  6841  elfi2  6863  djune  6966  updjudhcoinrg  6969  omp1eomlem  6982  ismkvnex  7032  mkvprop  7035  omniwomnimkv  7044  exmidfodomrlemrALT  7071  exmidaclem  7076  elni2  7141  ltsopi  7147  ltsonq  7225  renepnf  7832  renemnf  7833  lt0ne0d  8294  sup3exmid  8734  nnne0  8767  nn0ge2m1nn  9056  nn0nepnf  9067  xrltnr  9589  pnfnlt  9596  nltmnf  9597  xrltnsym  9602  xrlttri3  9606  nltpnft  9620  ngtmnft  9623  xrrebnd  9625  xrpnfdc  9648  xrmnfdc  9649  xsubge0  9687  xposdif  9688  xleaddadd  9693  fzpreddisj  9875  fzm1  9904  exfzdc  10041  xrbdtri  11069  m1exp1  11621  3prm  11832  exmidunben  11962  unct  11978  blssioo  12740  pilem3  12898  bj-intexr  13250  bj-intnexr  13251  subctctexmid  13342  nninfalllemn  13350  nninfsellemeq  13358  exmidsbthrlem  13365
 Copyright terms: Public domain W3C validator