Theorem mtbiri 681

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-in1 619  ax-in2 620

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nel02  3499  n0i  3500  axnul  4214  intexr  4240  intnexr  4241  iin0r  4259  exmid01  4288  ordtriexmidlem  4617  ordtriexmidlem2  4618  ordtri2or2exmidlem  4624  onsucelsucexmidlem  4627  sucprcreg  4647  preleq  4653  reg3exmidlemwe  4677  dcextest  4679  nn0eln0  4718  0nelelxp  4754  canth  5968  tfrlemisucaccv  6490  nnsucuniel  6662  nndceq  6666  nndcel  6667  2dom  6979  snnen2oprc  7045  snexxph  7148  elfi2  7170  djune  7276  updjudhcoinrg  7279  omp1eomlem  7292  nnnninfeq  7326  ismkvnex  7353  mkvprop  7356  omniwomnimkv  7365  nninfwlpoimlemginf  7374  exmidfodomrlemrALT  7413  exmidaclem  7422  netap  7472  2omotaplemap  7475  elni2  7533  ltsopi  7539  ltsonq  7617  renepnf  8226  renemnf  8227  lt0ne0d  8692  sup3exmid  9136  nnne0  9170  nn0ge2m1nn  9461  nn0nepnf  9472  xrltnr  10013  pnfnlt  10021  nltmnf  10022  xrltnsym  10027  xrlttri3  10031  nltpnft  10048  ngtmnft  10051  xrrebnd  10053  xrpnfdc  10076  xrmnfdc  10077  xsubge0  10115  xposdif  10116  xleaddadd  10121  fzpreddisj  10305  fzm1  10334  exfzdc  10485  xnn0nnen  10698  lsw0  11160  cats1un  11301  xrbdtri  11836  m1exp1  12461  bitsfzolem  12514  bitsfzo  12515  bitsinv1lem  12521  3prm  12699  prmdc  12701  pcgcd1  12900  pc2dvds  12902  pcmpt  12915  exmidunben  13046  unct  13062  fvprif  13425  blssioo  15276  pilem3  15506  perfectlem1  15722  lgsval2lem  15738  umgredgnlp  16002  clwwlkn0  16258  clwwlknnn  16262  bj-charfunbi  16406  bj-intexr  16503  bj-intnexr  16504  3dom  16587  2omap  16594  subctctexmid  16601  nninfsellemeq  16616  exmidsbthrlem  16626