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  3373  axnul  4061  intexr  4083  intnexr  4084  iin0r  4101  exmid01  4129  ordtriexmidlem  4443  ordtriexmidlem2  4444  ordtri2or2exmidlem  4449  onsucelsucexmidlem  4452  sucprcreg  4472  preleq  4478  reg3exmidlemwe  4501  dcextest  4503  nn0eln0  4541  0nelelxp  4576  tfrlemisucaccv  6230  nnsucuniel  6399  nndceq  6403  nndcel  6404  2dom  6707  snnen2oprc  6762  snexxph  6846  elfi2  6868  djune  6971  updjudhcoinrg  6974  omp1eomlem  6987  ismkvnex  7037  mkvprop  7040  omniwomnimkv  7049  exmidfodomrlemrALT  7076  exmidaclem  7081  elni2  7146  ltsopi  7152  ltsonq  7230  renepnf  7837  renemnf  7838  lt0ne0d  8299  sup3exmid  8739  nnne0  8772  nn0ge2m1nn  9061  nn0nepnf  9072  xrltnr  9596  pnfnlt  9603  nltmnf  9604  xrltnsym  9609  xrlttri3  9613  nltpnft  9627  ngtmnft  9630  xrrebnd  9632  xrpnfdc  9655  xrmnfdc  9656  xsubge0  9694  xposdif  9695  xleaddadd  9700  fzpreddisj  9882  fzm1  9911  exfzdc  10048  xrbdtri  11077  m1exp1  11634  3prm  11845  exmidunben  11975  unct  11991  blssioo  12753  pilem3  12912  bj-intexr  13277  bj-intnexr  13278  subctctexmid  13369  nninfalllemn  13377  nninfsellemeq  13385  exmidsbthrlem  13392