Theorem mtbiri 686

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

Step	Hyp	Ref	Expression
1		mtbiri.min	. 2 ⊢ ¬ 𝜒
2		mtbiri.maj	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	2	biimpd 144	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1, 3	mtoi 674	1 ⊢ (𝜑 → ¬ 𝜓)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-in1 623  ax-in2 624

This proof depends on definitions:  df-bi 117

This theorem is used by:  nel02  3526  n0i  3527  ifeqeqxdc  3687  axnul  4260  intexr  4288  intnexr  4289  iin0r  4308  exmid01  4337  ordtriexmidlem  4668  ordtriexmidlem2  4669  ordtri2or2exmidlem  4675  onsucelsucexmidlem  4678  sucprcreg  4698  preleq  4704  reg3exmidlemwe  4728  dcextest  4730  nn0eln0  4769  0nelelxp  4805  canth  6039  tfrlemisucaccv  6600  nnsucuniel  6772  nndceq  6776  nndcel  6777  2dom  7098  snnen2oprc  7166  snexxph  7273  elfi2  7312  2omap  7325  djune  7425  updjudhcoinrg  7428  omp1eomlem  7441  nnnninfeq  7475  ismkvnex  7502  mkvprop  7505  omniwomnimkv  7514  nninfwlpoimlemginf  7523  exmidfodomrlemrALT  7562  exmidaclem  7571  netap  7627  2omotaplemap  7630  elni2  7688  ltsopi  7694  ltsonq  7772  renepnf  8380  renemnf  8381  lt0ne0d  8849  sup3exmid  9296  nnne0  9342  nn0ge2m1nn  9639  nn0nepnf  9650  xrltnr  10199  pnfnlt  10207  nltmnf  10208  xrltnsym  10213  xrlttri3  10217  nltpnft  10234  ngtmnft  10237  xrrebnd  10239  xrpnfdc  10262  xrmnfdc  10263  xsubge0  10301  xposdif  10302  xleaddadd  10307  fzpreddisj  10496  fzm1  10525  exfzdc  10677  xnn0nnen  10896  hashtpglem  11321  lsw0  11375  cats1un  11516  xrbdtri  12068  m1exp1  12694  bitsfzolem  12747  bitsfzo  12748  bitsinv1lem  12754  3prm  12932  prmdc  12934  pcgcd1  13137  pc2dvds  13139  pcmpt  13152  ballotfilem4  13300  exmidunben  13376  unct  13392  fvprif  13724  blssioo  15791  pilem3  16022  perfectlem1  16311  bposlem5  16327  lgsval2lem  16346  umgredgnlp  16610  clwwlkn0  16866  clwwlknnn  16870  trlsegvdegfi  16925  eupth2lem3lem4fi  16931  konigsberg  16951  bj-charfunbi  17054  bj-intexr  17151  bj-intnexr  17152  3dom  17235  subctctexmid  17247  nninfsellemeq  17275  exmidsbthrlem  17285