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  3497  n0i  3498  axnul  4212  intexr  4238  intnexr  4239  iin0r  4257  exmid01  4286  ordtriexmidlem  4615  ordtriexmidlem2  4616  ordtri2or2exmidlem  4622  onsucelsucexmidlem  4625  sucprcreg  4645  preleq  4651  reg3exmidlemwe  4675  dcextest  4677  nn0eln0  4716  0nelelxp  4752  canth  5964  tfrlemisucaccv  6486  nnsucuniel  6658  nndceq  6662  nndcel  6663  2dom  6975  snnen2oprc  7041  snexxph  7140  elfi2  7162  djune  7268  updjudhcoinrg  7271  omp1eomlem  7284  nnnninfeq  7318  ismkvnex  7345  mkvprop  7348  omniwomnimkv  7357  nninfwlpoimlemginf  7366  exmidfodomrlemrALT  7404  exmidaclem  7413  netap  7463  2omotaplemap  7466  elni2  7524  ltsopi  7530  ltsonq  7608  renepnf  8217  renemnf  8218  lt0ne0d  8683  sup3exmid  9127  nnne0  9161  nn0ge2m1nn  9452  nn0nepnf  9463  xrltnr  10004  pnfnlt  10012  nltmnf  10013  xrltnsym  10018  xrlttri3  10022  nltpnft  10039  ngtmnft  10042  xrrebnd  10044  xrpnfdc  10067  xrmnfdc  10068  xsubge0  10106  xposdif  10107  xleaddadd  10112  fzpreddisj  10296  fzm1  10325  exfzdc  10476  xnn0nnen  10689  lsw0  11151  cats1un  11292  xrbdtri  11827  m1exp1  12452  bitsfzolem  12505  bitsfzo  12506  bitsinv1lem  12512  3prm  12690  prmdc  12692  pcgcd1  12891  pc2dvds  12893  pcmpt  12906  exmidunben  13037  unct  13053  fvprif  13416  blssioo  15267  pilem3  15497  perfectlem1  15713  lgsval2lem  15729  umgredgnlp  15991  clwwlkn0  16203  clwwlknnn  16207  bj-charfunbi  16342  bj-intexr  16439  bj-intnexr  16440  3dom  16523  2omap  16530  subctctexmid  16537  nninfsellemeq  16552  exmidsbthrlem  16562