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  3517  n0i  3518  ifeqeqxdc  3673  axnul  4240  intexr  4267  intnexr  4268  iin0r  4287  exmid01  4316  ordtriexmidlem  4646  ordtriexmidlem2  4647  ordtri2or2exmidlem  4653  onsucelsucexmidlem  4656  sucprcreg  4676  preleq  4682  reg3exmidlemwe  4706  dcextest  4708  nn0eln0  4747  0nelelxp  4783  canth  6009  tfrlemisucaccv  6569  nnsucuniel  6741  nndceq  6745  nndcel  6746  2dom  7059  snnen2oprc  7127  snexxph  7233  elfi2  7272  2omap  7282  djune  7382  updjudhcoinrg  7385  omp1eomlem  7398  nnnninfeq  7432  ismkvnex  7459  mkvprop  7462  omniwomnimkv  7471  nninfwlpoimlemginf  7480  exmidfodomrlemrALT  7519  exmidaclem  7528  netap  7584  2omotaplemap  7587  elni2  7645  ltsopi  7651  ltsonq  7729  renepnf  8337  renemnf  8338  lt0ne0d  8805  sup3exmid  9251  nnne0  9285  nn0ge2m1nn  9580  nn0nepnf  9591  xrltnr  10134  pnfnlt  10142  nltmnf  10143  xrltnsym  10148  xrlttri3  10152  nltpnft  10169  ngtmnft  10172  xrrebnd  10174  xrpnfdc  10197  xrmnfdc  10198  xsubge0  10236  xposdif  10237  xleaddadd  10242  fzpreddisj  10430  fzm1  10459  exfzdc  10611  xnn0nnen  10826  hashtpglem  11246  lsw0  11300  cats1un  11441  xrbdtri  11989  m1exp1  12615  bitsfzolem  12668  bitsfzo  12669  bitsinv1lem  12675  3prm  12853  prmdc  12855  pcgcd1  13054  pc2dvds  13056  pcmpt  13069  ballotfilem4  13188  exmidunben  13264  unct  13280  fvprif  13610  blssioo  15547  pilem3  15777  perfectlem1  15996  lgsval2lem  16012  umgredgnlp  16276  clwwlkn0  16532  clwwlknnn  16536  trlsegvdegfi  16591  eupth2lem3lem4fi  16597  konigsberg  16617  bj-charfunbi  16720  bj-intexr  16817  bj-intnexr  16818  3dom  16901  subctctexmid  16913  nninfsellemeq  16931  exmidsbthrlem  16941