Theorem mtbiri 670

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 659	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 609  ax-in2 610

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  nel02  3419  n0i  3420  axnul  4114  intexr  4136  intnexr  4137  iin0r  4155  exmid01  4184  ordtriexmidlem  4503  ordtriexmidlem2  4504  ordtri2or2exmidlem  4510  onsucelsucexmidlem  4513  sucprcreg  4533  preleq  4539  reg3exmidlemwe  4563  dcextest  4565  nn0eln0  4604  0nelelxp  4640  canth  5807  tfrlemisucaccv  6304  nnsucuniel  6474  nndceq  6478  nndcel  6479  2dom  6783  snnen2oprc  6838  snexxph  6927  elfi2  6949  djune  7055  updjudhcoinrg  7058  omp1eomlem  7071  nnnninfeq  7104  ismkvnex  7131  mkvprop  7134  omniwomnimkv  7143  nninfwlpoimlemginf  7152  exmidfodomrlemrALT  7180  exmidaclem  7185  elni2  7276  ltsopi  7282  ltsonq  7360  renepnf  7967  renemnf  7968  lt0ne0d  8432  sup3exmid  8873  nnne0  8906  nn0ge2m1nn  9195  nn0nepnf  9206  xrltnr  9736  pnfnlt  9744  nltmnf  9745  xrltnsym  9750  xrlttri3  9754  nltpnft  9771  ngtmnft  9774  xrrebnd  9776  xrpnfdc  9799  xrmnfdc  9800  xsubge0  9838  xposdif  9839  xleaddadd  9844  fzpreddisj  10027  fzm1  10056  exfzdc  10196  xrbdtri  11239  m1exp1  11860  3prm  12082  prmdc  12084  pcgcd1  12281  pc2dvds  12283  pcmpt  12295  exmidunben  12381  unct  12397  blssioo  13339  pilem3  13498  lgsval2lem  13705  bj-charfunbi  13846  bj-intexr  13943  bj-intnexr  13944  subctctexmid  14034  nninfsellemeq  14047  exmidsbthrlem  14054