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  3513  n0i  3514  axnul  4235  intexr  4262  intnexr  4263  iin0r  4282  exmid01  4311  ordtriexmidlem  4641  ordtriexmidlem2  4642  ordtri2or2exmidlem  4648  onsucelsucexmidlem  4651  sucprcreg  4671  preleq  4677  reg3exmidlemwe  4701  dcextest  4703  nn0eln0  4742  0nelelxp  4778  canth  6001  tfrlemisucaccv  6556  nnsucuniel  6728  nndceq  6732  nndcel  6733  2dom  7046  snnen2oprc  7114  snexxph  7220  elfi2  7259  2omap  7269  djune  7369  updjudhcoinrg  7372  omp1eomlem  7385  nnnninfeq  7419  ismkvnex  7446  mkvprop  7449  omniwomnimkv  7458  nninfwlpoimlemginf  7467  exmidfodomrlemrALT  7506  exmidaclem  7515  netap  7568  2omotaplemap  7571  elni2  7629  ltsopi  7635  ltsonq  7713  renepnf  8321  renemnf  8322  lt0ne0d  8787  sup3exmid  9231  nnne0  9265  nn0ge2m1nn  9560  nn0nepnf  9571  xrltnr  10112  pnfnlt  10120  nltmnf  10121  xrltnsym  10126  xrlttri3  10130  nltpnft  10147  ngtmnft  10150  xrrebnd  10152  xrpnfdc  10175  xrmnfdc  10176  xsubge0  10214  xposdif  10215  xleaddadd  10220  fzpreddisj  10405  fzm1  10434  exfzdc  10586  xnn0nnen  10799  hashtpglem  11218  lsw0  11272  cats1un  11413  xrbdtri  11961  m1exp1  12587  bitsfzolem  12640  bitsfzo  12641  bitsinv1lem  12647  3prm  12825  prmdc  12827  pcgcd1  13026  pc2dvds  13028  pcmpt  13041  exmidunben  13177  unct  13193  fvprif  13556  blssioo  15418  pilem3  15648  perfectlem1  15867  lgsval2lem  15883  umgredgnlp  16147  clwwlkn0  16403  clwwlknnn  16407  trlsegvdegfi  16462  eupth2lem3lem4fi  16468  konigsberg  16488  bj-charfunbi  16581  bj-intexr  16678  bj-intnexr  16679  3dom  16762  subctctexmid  16774  nninfsellemeq  16792  exmidsbthrlem  16802