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  3414  axnul  4107  intexr  4129  intnexr  4130  iin0r  4148  exmid01  4177  ordtriexmidlem  4496  ordtriexmidlem2  4497  ordtri2or2exmidlem  4503  onsucelsucexmidlem  4506  sucprcreg  4526  preleq  4532  reg3exmidlemwe  4556  dcextest  4558  nn0eln0  4597  0nelelxp  4633  canth  5796  tfrlemisucaccv  6293  nnsucuniel  6463  nndceq  6467  nndcel  6468  2dom  6771  snnen2oprc  6826  snexxph  6915  elfi2  6937  djune  7043  updjudhcoinrg  7046  omp1eomlem  7059  nnnninfeq  7092  ismkvnex  7119  mkvprop  7122  omniwomnimkv  7131  exmidfodomrlemrALT  7159  exmidaclem  7164  elni2  7255  ltsopi  7261  ltsonq  7339  renepnf  7946  renemnf  7947  lt0ne0d  8411  sup3exmid  8852  nnne0  8885  nn0ge2m1nn  9174  nn0nepnf  9185  xrltnr  9715  pnfnlt  9723  nltmnf  9724  xrltnsym  9729  xrlttri3  9733  nltpnft  9750  ngtmnft  9753  xrrebnd  9755  xrpnfdc  9778  xrmnfdc  9779  xsubge0  9817  xposdif  9818  xleaddadd  9823  fzpreddisj  10006  fzm1  10035  exfzdc  10175  xrbdtri  11217  m1exp1  11838  3prm  12060  prmdc  12062  pcgcd1  12259  pc2dvds  12261  pcmpt  12273  exmidunben  12359  unct  12375  blssioo  13195  pilem3  13354  lgsval2lem  13561  bj-charfunbi  13703  bj-intexr  13800  bj-intnexr  13801  subctctexmid  13891  nninfsellemeq  13904  exmidsbthrlem  13911