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  7396  ismkvnex  7496  pw1ne3  7590  sucpw1nel3  7593  3nsssucpw1  7596  0nnq  7732  0npr  7851  nqprdisj  7912  0ncn  8199  axpre-ltirr  8250  pnfnre  8368  mnfnre  8369  inelr  8915  xrltnr  10192  fzo0  10588  fzouzdisj  10600  inftonninf  10894  hashinfom  11233  lsw0  11368  3prm  12925  sqrt2irr  12960  ballotfilem4  13293  ennnfonelem1  13350  clwwlknnn  16819  konigsberglem4  16898  bj-nndcALT  16952  bj-vprc  17088  pwle2  17194  exmidsbthrlem  17233  rals-no-surprise  17315