Theorem mtbir 682

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 132	. 2 |- ( ps <-> ph )
4	1, 3	mtbi 681	1 |- -. ph

This proof depends on syntax axioms:   -. wn 3   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624

This proof depends on definitions:  df-bi 117

This theorem is used by:  nnexmid  862  nndc  863  fal  1409  ax-9  1584  nonconne  2432  nemtbir  2509  ru  3050  noel  3525  iun0  4069  0iun  4070  br0  4179  vprc  4265  iin0r  4306  nlim0  4539  snnex  4594  onsucelsucexmid  4677  0nelxp  4802  dm0  4995  iprc  5051  co02  5301  0fv  5734  frec0g  6668  nnsucuniel  6768  1nen2  7162  1ndom2  7166  fidcenumlemrk  7271  djulclb  7395  ismkvnex  7495  pw1ne3  7589  sucpw1nel3  7592  3nsssucpw1  7595  0nnq  7731  0npr  7850  nqprdisj  7911  0ncn  8198  axpre-ltirr  8249  pnfnre  8367  mnfnre  8368  inelr  8912  xrltnr  10181  fzo0  10577  fzouzdisj  10589  inftonninf  10879  hashinfom  11217  lsw0  11352  3prm  12906  sqrt2irr  12940  ballotfilem4  13241  ennnfonelem1  13298  clwwlknnn  16653  konigsberglem4  16732  bj-nndcALT  16786  bj-vprc  16922  pwle2  17028  exmidsbthrlem  17067  rals-no-surprise  17148