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  4258  intexr  4286  intnexr  4287  iin0r  4306  exmid01  4335  ordtriexmidlem  4666  ordtriexmidlem2  4667  ordtri2or2exmidlem  4673  onsucelsucexmidlem  4676  sucprcreg  4696  preleq  4702  reg3exmidlemwe  4726  dcextest  4728  nn0eln0  4767  0nelelxp  4803  canth  6036  tfrlemisucaccv  6596  nnsucuniel  6768  nndceq  6772  nndcel  6773  2dom  7093  snnen2oprc  7161  snexxph  7267  elfi2  7306  2omap  7318  djune  7418  updjudhcoinrg  7421  omp1eomlem  7434  nnnninfeq  7468  ismkvnex  7495  mkvprop  7498  omniwomnimkv  7507  nninfwlpoimlemginf  7516  exmidfodomrlemrALT  7555  exmidaclem  7564  netap  7620  2omotaplemap  7623  elni2  7681  ltsopi  7687  ltsonq  7765  renepnf  8373  renemnf  8374  lt0ne0d  8841  sup3exmid  9288  nnne0  9333  nn0ge2m1nn  9629  nn0nepnf  9640  xrltnr  10183  pnfnlt  10191  nltmnf  10192  xrltnsym  10197  xrlttri3  10201  nltpnft  10218  ngtmnft  10221  xrrebnd  10223  xrpnfdc  10246  xrmnfdc  10247  xsubge0  10285  xposdif  10286  xleaddadd  10291  fzpreddisj  10480  fzm1  10509  exfzdc  10661  xnn0nnen  10876  hashtpglem  11300  lsw0  11354  cats1un  11495  xrbdtri  12044  m1exp1  12670  bitsfzolem  12723  bitsfzo  12724  bitsinv1lem  12730  3prm  12908  prmdc  12910  pcgcd1  13109  pc2dvds  13111  pcmpt  13124  ballotfilem4  13243  exmidunben  13319  unct  13335  fvprif  13666  blssioo  15656  pilem3  15887  perfectlem1  16119  lgsval2lem  16141  umgredgnlp  16405  clwwlkn0  16661  clwwlknnn  16665  trlsegvdegfi  16720  eupth2lem3lem4fi  16726  konigsberg  16746  bj-charfunbi  16849  bj-intexr  16946  bj-intnexr  16947  3dom  17030  subctctexmid  17042  nninfsellemeq  17069  exmidsbthrlem  17079