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  3496  n0i  3497  axnul  4208  intexr  4233  intnexr  4234  iin0r  4252  exmid01  4281  ordtriexmidlem  4610  ordtriexmidlem2  4611  ordtri2or2exmidlem  4617  onsucelsucexmidlem  4620  sucprcreg  4640  preleq  4646  reg3exmidlemwe  4670  dcextest  4672  nn0eln0  4711  0nelelxp  4747  canth  5951  tfrlemisucaccv  6469  nnsucuniel  6639  nndceq  6643  nndcel  6644  2dom  6956  snnen2oprc  7017  snexxph  7113  elfi2  7135  djune  7241  updjudhcoinrg  7244  omp1eomlem  7257  nnnninfeq  7291  ismkvnex  7318  mkvprop  7321  omniwomnimkv  7330  nninfwlpoimlemginf  7339  exmidfodomrlemrALT  7377  exmidaclem  7386  netap  7436  2omotaplemap  7439  elni2  7497  ltsopi  7503  ltsonq  7581  renepnf  8190  renemnf  8191  lt0ne0d  8656  sup3exmid  9100  nnne0  9134  nn0ge2m1nn  9425  nn0nepnf  9436  xrltnr  9971  pnfnlt  9979  nltmnf  9980  xrltnsym  9985  xrlttri3  9989  nltpnft  10006  ngtmnft  10009  xrrebnd  10011  xrpnfdc  10034  xrmnfdc  10035  xsubge0  10073  xposdif  10074  xleaddadd  10079  fzpreddisj  10263  fzm1  10292  exfzdc  10441  xnn0nnen  10654  lsw0  11114  cats1un  11248  xrbdtri  11782  m1exp1  12407  bitsfzolem  12460  bitsfzo  12461  bitsinv1lem  12467  3prm  12645  prmdc  12647  pcgcd1  12846  pc2dvds  12848  pcmpt  12861  exmidunben  12992  unct  13008  fvprif  13371  blssioo  15221  pilem3  15451  perfectlem1  15667  lgsval2lem  15683  umgredgnlp  15944  bj-charfunbi  16132  bj-intexr  16229  bj-intnexr  16230  2omap  16318  subctctexmid  16325  nninfsellemeq  16339  exmidsbthrlem  16349