Theorem mtbiri 679

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 668	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 617  ax-in2 618

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nel02  3496  n0i  3497  axnul  4209  intexr  4234  intnexr  4235  iin0r  4253  exmid01  4282  ordtriexmidlem  4611  ordtriexmidlem2  4612  ordtri2or2exmidlem  4618  onsucelsucexmidlem  4621  sucprcreg  4641  preleq  4647  reg3exmidlemwe  4671  dcextest  4673  nn0eln0  4712  0nelelxp  4748  canth  5958  tfrlemisucaccv  6477  nnsucuniel  6649  nndceq  6653  nndcel  6654  2dom  6966  snnen2oprc  7029  snexxph  7128  elfi2  7150  djune  7256  updjudhcoinrg  7259  omp1eomlem  7272  nnnninfeq  7306  ismkvnex  7333  mkvprop  7336  omniwomnimkv  7345  nninfwlpoimlemginf  7354  exmidfodomrlemrALT  7392  exmidaclem  7401  netap  7451  2omotaplemap  7454  elni2  7512  ltsopi  7518  ltsonq  7596  renepnf  8205  renemnf  8206  lt0ne0d  8671  sup3exmid  9115  nnne0  9149  nn0ge2m1nn  9440  nn0nepnf  9451  xrltnr  9987  pnfnlt  9995  nltmnf  9996  xrltnsym  10001  xrlttri3  10005  nltpnft  10022  ngtmnft  10025  xrrebnd  10027  xrpnfdc  10050  xrmnfdc  10051  xsubge0  10089  xposdif  10090  xleaddadd  10095  fzpreddisj  10279  fzm1  10308  exfzdc  10458  xnn0nnen  10671  lsw0  11132  cats1un  11268  xrbdtri  11802  m1exp1  12427  bitsfzolem  12480  bitsfzo  12481  bitsinv1lem  12487  3prm  12665  prmdc  12667  pcgcd1  12866  pc2dvds  12868  pcmpt  12881  exmidunben  13012  unct  13028  fvprif  13391  blssioo  15242  pilem3  15472  perfectlem1  15688  lgsval2lem  15704  umgredgnlp  15965  bj-charfunbi  16229  bj-intexr  16326  bj-intnexr  16327  3dom  16411  2omap  16418  subctctexmid  16425  nninfsellemeq  16440  exmidsbthrlem  16450