Theorem mtbiri 682

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  3517  n0i  3518  ifeqeqxdc  3673  axnul  4240  intexr  4267  intnexr  4268  iin0r  4287  exmid01  4316  ordtriexmidlem  4646  ordtriexmidlem2  4647  ordtri2or2exmidlem  4653  onsucelsucexmidlem  4656  sucprcreg  4676  preleq  4682  reg3exmidlemwe  4706  dcextest  4708  nn0eln0  4747  0nelelxp  4783  canth  6009  tfrlemisucaccv  6569  nnsucuniel  6741  nndceq  6745  nndcel  6746  2dom  7059  snnen2oprc  7127  snexxph  7233  elfi2  7272  2omap  7282  djune  7382  updjudhcoinrg  7385  omp1eomlem  7398  nnnninfeq  7432  ismkvnex  7459  mkvprop  7462  omniwomnimkv  7471  nninfwlpoimlemginf  7480  exmidfodomrlemrALT  7519  exmidaclem  7528  netap  7584  2omotaplemap  7587  elni2  7645  ltsopi  7651  ltsonq  7729  renepnf  8337  renemnf  8338  lt0ne0d  8804  sup3exmid  9248  nnne0  9282  nn0ge2m1nn  9577  nn0nepnf  9588  xrltnr  10131  pnfnlt  10139  nltmnf  10140  xrltnsym  10145  xrlttri3  10149  nltpnft  10166  ngtmnft  10169  xrrebnd  10171  xrpnfdc  10194  xrmnfdc  10195  xsubge0  10233  xposdif  10234  xleaddadd  10239  fzpreddisj  10427  fzm1  10456  exfzdc  10608  xnn0nnen  10823  hashtpglem  11243  lsw0  11297  cats1un  11438  xrbdtri  11986  m1exp1  12612  bitsfzolem  12665  bitsfzo  12666  bitsinv1lem  12672  3prm  12850  prmdc  12852  pcgcd1  13051  pc2dvds  13053  pcmpt  13066  ballotfilem4  13185  exmidunben  13261  unct  13277  fvprif  13607  blssioo  15544  pilem3  15774  perfectlem1  15993  lgsval2lem  16009  umgredgnlp  16273  clwwlkn0  16529  clwwlknnn  16533  trlsegvdegfi  16588  eupth2lem3lem4fi  16594  konigsberg  16614  bj-charfunbi  16707  bj-intexr  16804  bj-intnexr  16805  3dom  16888  subctctexmid  16900  nninfsellemeq  16918  exmidsbthrlem  16928