Theorem mtbiri 600

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

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-in1 544  ax-in2 545

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  psstr  3049  sspsstr  3050  psssstr  3051  n0i  3229  axnul  3882  intexr  3904  intnexr  3905  iin0r  3922  ordtriexmidlem  4245  ordtriexmidlem2  4246  ordtri2or2exmidlem  4251  onsucelsucexmidlem  4254  sucprcreg  4273  preleq  4279  reg3exmidlemwe  4303  nn0eln0  4341  0nelelxp  4373  tfrlemisucaccv  5939  nndceq  6077  nndcel  6078  2dom  6285  snnen2oprc  6323  elni2  6412  ltsopi  6418  ltsonq  6496  renepnf  7073  renemnf  7074  lt0ne0d  7505  nnne0  7942  nn0ge2m1nn  8242  xrltnr  8701  pnfnlt  8708  nltmnf  8709  xrltnsym  8714  xrlttri3  8718  nltpnft  8730  ngtmnft  8731  xrrebnd  8732  fzpreddisj  8933  fzm1  8962  bj-intexr  10028  bj-intnexr  10029