Theorem mtbiri 665

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 143	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1, 3	mtoi 654	1 ⊢ (𝜑 → ¬ 𝜓)

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 604  ax-in2 605

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  n0i  3409  axnul  4101  intexr  4123  intnexr  4124  iin0r  4142  exmid01  4171  ordtriexmidlem  4490  ordtriexmidlem2  4491  ordtri2or2exmidlem  4497  onsucelsucexmidlem  4500  sucprcreg  4520  preleq  4526  reg3exmidlemwe  4550  dcextest  4552  nn0eln0  4591  0nelelxp  4627  canth  5790  tfrlemisucaccv  6284  nnsucuniel  6454  nndceq  6458  nndcel  6459  2dom  6762  snnen2oprc  6817  snexxph  6906  elfi2  6928  djune  7034  updjudhcoinrg  7037  omp1eomlem  7050  nnnninfeq  7083  ismkvnex  7110  mkvprop  7113  omniwomnimkv  7122  exmidfodomrlemrALT  7150  exmidaclem  7155  elni2  7246  ltsopi  7252  ltsonq  7330  renepnf  7937  renemnf  7938  lt0ne0d  8402  sup3exmid  8843  nnne0  8876  nn0ge2m1nn  9165  nn0nepnf  9176  xrltnr  9706  pnfnlt  9714  nltmnf  9715  xrltnsym  9720  xrlttri3  9724  nltpnft  9741  ngtmnft  9744  xrrebnd  9746  xrpnfdc  9769  xrmnfdc  9770  xsubge0  9808  xposdif  9809  xleaddadd  9814  fzpreddisj  9996  fzm1  10025  exfzdc  10165  xrbdtri  11203  m1exp1  11823  3prm  12039  prmdc  12041  pcgcd1  12236  pc2dvds  12238  pcmpt  12250  exmidunben  12296  unct  12312  blssioo  13086  pilem3  13245  bj-charfunbi  13528  bj-intexr  13625  bj-intnexr  13626  subctctexmid  13715  nninfsellemeq  13728  exmidsbthrlem  13735