Theorem mtbiri 682

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 670	1 ⊢ (𝜑 → ¬ 𝜓)

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 619  ax-in2 620

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nel02  3501  n0i  3502  axnul  4219  intexr  4245  intnexr  4246  iin0r  4265  exmid01  4294  ordtriexmidlem  4623  ordtriexmidlem2  4624  ordtri2or2exmidlem  4630  onsucelsucexmidlem  4633  sucprcreg  4653  preleq  4659  reg3exmidlemwe  4683  dcextest  4685  nn0eln0  4724  0nelelxp  4760  canth  5979  tfrlemisucaccv  6534  nnsucuniel  6706  nndceq  6710  nndcel  6711  2dom  7023  snnen2oprc  7089  snexxph  7192  elfi2  7214  djune  7320  updjudhcoinrg  7323  omp1eomlem  7336  nnnninfeq  7370  ismkvnex  7397  mkvprop  7400  omniwomnimkv  7409  nninfwlpoimlemginf  7418  exmidfodomrlemrALT  7457  exmidaclem  7466  netap  7516  2omotaplemap  7519  elni2  7577  ltsopi  7583  ltsonq  7661  renepnf  8270  renemnf  8271  lt0ne0d  8736  sup3exmid  9180  nnne0  9214  nn0ge2m1nn  9505  nn0nepnf  9516  xrltnr  10057  pnfnlt  10065  nltmnf  10066  xrltnsym  10071  xrlttri3  10075  nltpnft  10092  ngtmnft  10095  xrrebnd  10097  xrpnfdc  10120  xrmnfdc  10121  xsubge0  10159  xposdif  10160  xleaddadd  10165  fzpreddisj  10349  fzm1  10378  exfzdc  10530  xnn0nnen  10743  hashtpglem  11154  lsw0  11208  cats1un  11349  xrbdtri  11897  m1exp1  12523  bitsfzolem  12576  bitsfzo  12577  bitsinv1lem  12583  3prm  12761  prmdc  12763  pcgcd1  12962  pc2dvds  12964  pcmpt  12977  exmidunben  13108  unct  13124  fvprif  13487  blssioo  15344  pilem3  15574  perfectlem1  15793  lgsval2lem  15809  umgredgnlp  16073  clwwlkn0  16329  clwwlknnn  16333  trlsegvdegfi  16388  eupth2lem3lem4fi  16394  konigsberg  16414  bj-charfunbi  16507  bj-intexr  16604  bj-intnexr  16605  3dom  16688  2omap  16695  subctctexmid  16702  nninfsellemeq  16720  exmidsbthrlem  16730