Theorem mtbiri 676

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 665	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 615  ax-in2 616

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nel02  3456  n0i  3457  axnul  4159  intexr  4184  intnexr  4185  iin0r  4203  exmid01  4232  ordtriexmidlem  4556  ordtriexmidlem2  4557  ordtri2or2exmidlem  4563  onsucelsucexmidlem  4566  sucprcreg  4586  preleq  4592  reg3exmidlemwe  4616  dcextest  4618  nn0eln0  4657  0nelelxp  4693  canth  5878  tfrlemisucaccv  6392  nnsucuniel  6562  nndceq  6566  nndcel  6567  2dom  6873  snnen2oprc  6930  snexxph  7025  elfi2  7047  djune  7153  updjudhcoinrg  7156  omp1eomlem  7169  nnnninfeq  7203  ismkvnex  7230  mkvprop  7233  omniwomnimkv  7242  nninfwlpoimlemginf  7251  exmidfodomrlemrALT  7282  exmidaclem  7291  netap  7337  2omotaplemap  7340  elni2  7398  ltsopi  7404  ltsonq  7482  renepnf  8091  renemnf  8092  lt0ne0d  8557  sup3exmid  9001  nnne0  9035  nn0ge2m1nn  9326  nn0nepnf  9337  xrltnr  9871  pnfnlt  9879  nltmnf  9880  xrltnsym  9885  xrlttri3  9889  nltpnft  9906  ngtmnft  9909  xrrebnd  9911  xrpnfdc  9934  xrmnfdc  9935  xsubge0  9973  xposdif  9974  xleaddadd  9979  fzpreddisj  10163  fzm1  10192  exfzdc  10333  xnn0nnen  10546  xrbdtri  11458  m1exp1  12083  bitsfzolem  12136  bitsfzo  12137  bitsinv1lem  12143  3prm  12321  prmdc  12323  pcgcd1  12522  pc2dvds  12524  pcmpt  12537  exmidunben  12668  unct  12684  fvprif  13045  blssioo  14873  pilem3  15103  perfectlem1  15319  lgsval2lem  15335  bj-charfunbi  15541  bj-intexr  15638  bj-intnexr  15639  2omap  15726  subctctexmid  15731  nninfsellemeq  15745  exmidsbthrlem  15753