Theorem mtbir 595

Description: An inference from a biconditional, related to modus tollens. (Contributed by NM, 15-Nov-1994.) (Proof shortened by Wolf Lammen, 14-Oct-2012.)

Hypotheses

Ref	Expression
mtbir.1	|- -. ps
mtbir.2	|- (ph <-> ps)

Assertion

Ref	Expression
mtbir	|- -. ph

Proof of Theorem mtbir

Step	Hyp	Ref	Expression
1		mtbir.1	. 2 |- -. ps
2		mtbir.2	. . 3 |- (ph <-> ps)
3	2	bicomi 123	. 2 |- (ps <-> ph)
4	1, 3	mtbi 594	1 |- -. ph

Syntax hints:  -. wn 3   <-> wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  fal  1249  ax-9  1421  nonconne  2212  nemtbir  2288  ru  2757  pssirr  3038  noel  3222  npss0  3260  iun0  3704  0iun  3705  vprc  3879  iin0r  3913  nlim0  4097  snnex  4147  onsucelsucexmid  4215  0nelxp  4315  dm0  4492  iprc  4543  co02  4777  0fv  5151  frec0g  5922  0nnq  6348  0npr  6466  nqprdisj  6527  0ncn  6729  axpre-ltirr  6766  pnfnre  6864  mnfnre  6865  inelr  7368  xrltnr  8471  fzo0  8794  fzouzdisj  8806  nnexmid  9234  nndc  9235  bj-vprc  9351