Theorem mtbiri 664

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 653	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 603  ax-in2 604

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  n0i  3368  axnul  4053  intexr  4075  intnexr  4076  iin0r  4093  exmid01  4121  ordtriexmidlem  4435  ordtriexmidlem2  4436  ordtri2or2exmidlem  4441  onsucelsucexmidlem  4444  sucprcreg  4464  preleq  4470  reg3exmidlemwe  4493  dcextest  4495  nn0eln0  4533  0nelelxp  4568  tfrlemisucaccv  6222  nnsucuniel  6391  nndceq  6395  nndcel  6396  2dom  6699  snnen2oprc  6754  snexxph  6838  elfi2  6860  djune  6963  updjudhcoinrg  6966  omp1eomlem  6979  ismkvnex  7029  mkvprop  7032  exmidfodomrlemrALT  7059  exmidaclem  7064  elni2  7122  ltsopi  7128  ltsonq  7206  renepnf  7813  renemnf  7814  lt0ne0d  8275  sup3exmid  8715  nnne0  8748  nn0ge2m1nn  9037  nn0nepnf  9048  xrltnr  9566  pnfnlt  9573  nltmnf  9574  xrltnsym  9579  xrlttri3  9583  nltpnft  9597  ngtmnft  9600  xrrebnd  9602  xrpnfdc  9625  xrmnfdc  9626  xsubge0  9664  xposdif  9665  xleaddadd  9670  fzpreddisj  9851  fzm1  9880  exfzdc  10017  xrbdtri  11045  m1exp1  11598  3prm  11809  exmidunben  11939  unct  11954  blssioo  12714  pilem3  12864  bj-intexr  13106  bj-intnexr  13107  subctctexmid  13196  nninfalllemn  13202  nninfsellemeq  13210  exmidsbthrlem  13217