Theorem mtbiri 677

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 666	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 615  ax-in2 616

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nel02  3469  n0i  3470  axnul  4180  intexr  4205  intnexr  4206  iin0r  4224  exmid01  4253  ordtriexmidlem  4580  ordtriexmidlem2  4581  ordtri2or2exmidlem  4587  onsucelsucexmidlem  4590  sucprcreg  4610  preleq  4616  reg3exmidlemwe  4640  dcextest  4642  nn0eln0  4681  0nelelxp  4717  canth  5915  tfrlemisucaccv  6429  nnsucuniel  6599  nndceq  6603  nndcel  6604  2dom  6916  snnen2oprc  6977  snexxph  7073  elfi2  7095  djune  7201  updjudhcoinrg  7204  omp1eomlem  7217  nnnninfeq  7251  ismkvnex  7278  mkvprop  7281  omniwomnimkv  7290  nninfwlpoimlemginf  7299  exmidfodomrlemrALT  7337  exmidaclem  7346  netap  7396  2omotaplemap  7399  elni2  7457  ltsopi  7463  ltsonq  7541  renepnf  8150  renemnf  8151  lt0ne0d  8616  sup3exmid  9060  nnne0  9094  nn0ge2m1nn  9385  nn0nepnf  9396  xrltnr  9931  pnfnlt  9939  nltmnf  9940  xrltnsym  9945  xrlttri3  9949  nltpnft  9966  ngtmnft  9969  xrrebnd  9971  xrpnfdc  9994  xrmnfdc  9995  xsubge0  10033  xposdif  10034  xleaddadd  10039  fzpreddisj  10223  fzm1  10252  exfzdc  10401  xnn0nnen  10614  lsw0  11073  cats1un  11207  xrbdtri  11672  m1exp1  12297  bitsfzolem  12350  bitsfzo  12351  bitsinv1lem  12357  3prm  12535  prmdc  12537  pcgcd1  12736  pc2dvds  12738  pcmpt  12751  exmidunben  12882  unct  12898  fvprif  13260  blssioo  15110  pilem3  15340  perfectlem1  15556  lgsval2lem  15572  umgredgnlp  15826  bj-charfunbi  15916  bj-intexr  16013  bj-intnexr  16014  2omap  16102  subctctexmid  16109  nninfsellemeq  16123  exmidsbthrlem  16133