Theorem mtbir 678

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 677	1 |- -. ph

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nnexmid  858  nndc  859  fal  1405  ax-9  1580  nonconne  2424  nemtbir  2501  ru  3041  noel  3512  iun0  4048  0iun  4049  br0  4158  vprc  4242  iin0r  4282  nlim0  4515  snnex  4569  onsucelsucexmid  4652  0nelxp  4777  dm0  4970  iprc  5026  co02  5276  0fv  5708  frec0g  6628  nnsucuniel  6728  1nen2  7115  1ndom2  7119  fidcenumlemrk  7224  djulclb  7346  ismkvnex  7446  pw1ne3  7540  sucpw1nel3  7543  3nsssucpw1  7546  0nnq  7679  0npr  7798  nqprdisj  7859  0ncn  8146  axpre-ltirr  8197  pnfnre  8315  mnfnre  8316  inelr  8858  xrltnr  10112  fzo0  10504  fzouzdisj  10516  inftonninf  10804  hashinfom  11141  lsw0  11272  3prm  12825  sqrt2irr  12859  ennnfonelem1  13158  clwwlknnn  16407  konigsberglem4  16486  bj-nndcALT  16530  bj-vprc  16666  pwle2  16772  exmidsbthrlem  16802