Theorem mtbiri 665

Description: An inference from a biconditional, similar to modus tollens. (Contributed by NM, 24-Aug-1995.)

Hypotheses

Ref	Expression
mtbiri.min	|- -. ch
mtbiri.maj	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
mtbiri	|- ( ph -> -. ps )

Proof of Theorem mtbiri

Step	Hyp	Ref	Expression
1		mtbiri.min	. 2 |- -. ch
2		mtbiri.maj	. . 3 |- ( ph -> ( ps <-> ch ) )
3	2	biimpd 143	. 2 |- ( ph -> ( ps -> ch ) )
4	1, 3	mtoi 654	1 |- ( ph -> -. ps )

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  3399  axnul  4089  intexr  4111  intnexr  4112  iin0r  4130  exmid01  4159  ordtriexmidlem  4477  ordtriexmidlem2  4478  ordtri2or2exmidlem  4484  onsucelsucexmidlem  4487  sucprcreg  4507  preleq  4513  reg3exmidlemwe  4537  dcextest  4539  nn0eln0  4578  0nelelxp  4614  canth  5775  tfrlemisucaccv  6269  nnsucuniel  6439  nndceq  6443  nndcel  6444  2dom  6747  snnen2oprc  6802  snexxph  6891  elfi2  6913  djune  7017  updjudhcoinrg  7020  omp1eomlem  7033  nnnninfeq  7066  ismkvnex  7093  mkvprop  7096  omniwomnimkv  7105  exmidfodomrlemrALT  7133  exmidaclem  7138  elni2  7229  ltsopi  7235  ltsonq  7313  renepnf  7920  renemnf  7921  lt0ne0d  8383  sup3exmid  8823  nnne0  8856  nn0ge2m1nn  9145  nn0nepnf  9156  xrltnr  9681  pnfnlt  9689  nltmnf  9690  xrltnsym  9695  xrlttri3  9699  nltpnft  9713  ngtmnft  9716  xrrebnd  9718  xrpnfdc  9741  xrmnfdc  9742  xsubge0  9780  xposdif  9781  xleaddadd  9786  fzpreddisj  9968  fzm1  9997  exfzdc  10134  xrbdtri  11168  m1exp1  11786  3prm  11999  prmdc  12001  exmidunben  12142  unct  12158  blssioo  12932  pilem3  13091  bj-charfunbi  13373  bj-intexr  13470  bj-intnexr  13471  subctctexmid  13560  nninfsellemeq  13573  exmidsbthrlem  13580