Theorem mtbiri 676

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 665	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  3455  n0i  3456  axnul  4158  intexr  4183  intnexr  4184  iin0r  4202  exmid01  4231  ordtriexmidlem  4555  ordtriexmidlem2  4556  ordtri2or2exmidlem  4562  onsucelsucexmidlem  4565  sucprcreg  4585  preleq  4591  reg3exmidlemwe  4615  dcextest  4617  nn0eln0  4656  0nelelxp  4692  canth  5875  tfrlemisucaccv  6383  nnsucuniel  6553  nndceq  6557  nndcel  6558  2dom  6864  snnen2oprc  6921  snexxph  7016  elfi2  7038  djune  7144  updjudhcoinrg  7147  omp1eomlem  7160  nnnninfeq  7194  ismkvnex  7221  mkvprop  7224  omniwomnimkv  7233  nninfwlpoimlemginf  7242  exmidfodomrlemrALT  7270  exmidaclem  7275  netap  7321  2omotaplemap  7324  elni2  7381  ltsopi  7387  ltsonq  7465  renepnf  8074  renemnf  8075  lt0ne0d  8540  sup3exmid  8984  nnne0  9018  nn0ge2m1nn  9309  nn0nepnf  9320  xrltnr  9854  pnfnlt  9862  nltmnf  9863  xrltnsym  9868  xrlttri3  9872  nltpnft  9889  ngtmnft  9892  xrrebnd  9894  xrpnfdc  9917  xrmnfdc  9918  xsubge0  9956  xposdif  9957  xleaddadd  9962  fzpreddisj  10146  fzm1  10175  exfzdc  10316  xnn0nnen  10529  xrbdtri  11441  m1exp1  12066  bitsfzolem  12118  bitsfzo  12119  3prm  12296  prmdc  12298  pcgcd1  12497  pc2dvds  12499  pcmpt  12512  exmidunben  12643  unct  12659  fvprif  12986  blssioo  14789  pilem3  15019  perfectlem1  15235  lgsval2lem  15251  bj-charfunbi  15457  bj-intexr  15554  bj-intnexr  15555  subctctexmid  15645  nninfsellemeq  15658  exmidsbthrlem  15666