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  5969  tfrlemisucaccv  6491  nnsucuniel  6663  nndceq  6667  nndcel  6668  2dom  6980  snnen2oprc  7046  snexxph  7149  elfi2  7171  djune  7277  updjudhcoinrg  7280  omp1eomlem  7293  nnnninfeq  7327  ismkvnex  7354  mkvprop  7357  omniwomnimkv  7366  nninfwlpoimlemginf  7375  exmidfodomrlemrALT  7414  exmidaclem  7423  netap  7473  2omotaplemap  7476  elni2  7534  ltsopi  7540  ltsonq  7618  renepnf  8227  renemnf  8228  lt0ne0d  8693  sup3exmid  9137  nnne0  9171  nn0ge2m1nn  9462  nn0nepnf  9473  xrltnr  10014  pnfnlt  10022  nltmnf  10023  xrltnsym  10028  xrlttri3  10032  nltpnft  10049  ngtmnft  10052  xrrebnd  10054  xrpnfdc  10077  xrmnfdc  10078  xsubge0  10116  xposdif  10117  xleaddadd  10122  fzpreddisj  10306  fzm1  10335  exfzdc  10487  xnn0nnen  10700  hashtpglem  11111  lsw0  11165  cats1un  11306  xrbdtri  11854  m1exp1  12480  bitsfzolem  12533  bitsfzo  12534  bitsinv1lem  12540  3prm  12718  prmdc  12720  pcgcd1  12919  pc2dvds  12921  pcmpt  12934  exmidunben  13065  unct  13081  fvprif  13444  blssioo  15296  pilem3  15526  perfectlem1  15742  lgsval2lem  15758  umgredgnlp  16022  clwwlkn0  16278  clwwlknnn  16282  trlsegvdegfi  16337  eupth2lem3lem4fi  16343  konigsberg  16363  bj-charfunbi  16457  bj-intexr  16554  bj-intnexr  16555  3dom  16638  2omap  16645  subctctexmid  16652  nninfsellemeq  16667  exmidsbthrlem  16677