Theorem mtbiri 632

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 142	. 2 |- ( ph -> ( ps -> ch ) )
4	1, 3	mtoi 622	1 |- ( ph -> -. ps )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-in1 576  ax-in2 577

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  n0i  3256  axnul  3903  intexr  3925  intnexr  3926  iin0r  3943  ordtriexmidlem  4263  ordtriexmidlem2  4264  ordtri2or2exmidlem  4269  onsucelsucexmidlem  4272  sucprcreg  4292  preleq  4298  reg3exmidlemwe  4321  nn0eln0  4359  0nelelxp  4391  tfrlemisucaccv  5962  nndceq  6100  nndcel  6101  2dom  6308  snnen2oprc  6346  elni2  6504  ltsopi  6510  ltsonq  6588  renepnf  7166  renemnf  7167  lt0ne0d  7614  nnne0  8067  nn0ge2m1nn  8348  xrltnr  8855  pnfnlt  8862  nltmnf  8863  xrltnsym  8868  xrlttri3  8872  nltpnft  8884  ngtmnft  8885  xrrebnd  8886  fzpreddisj  9088  fzm1  9117  exfzdc  9249  m1exp1  10301  3prm  10510  bj-intexr  10699  bj-intnexr  10700