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  8914  xrltnr  10191  fzo0  10587  fzouzdisj  10599  inftonninf  10892  hashinfom  11231  lsw0  11366  3prm  12922  sqrt2irr  12957  ballotfilem4  13290  ennnfonelem1  13347  clwwlknnn  16751  konigsberglem4  16830  bj-nndcALT  16884  bj-vprc  17020  pwle2  17126  exmidsbthrlem  17165  rals-no-surprise  17246