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  2415  nemtbir  2492  ru  3031  noel  3500  iun0  4032  0iun  4033  br0  4142  vprc  4226  iin0r  4265  nlim0  4497  snnex  4551  onsucelsucexmid  4634  0nelxp  4759  dm0  4951  iprc  5007  co02  5257  0fv  5686  frec0g  6606  nnsucuniel  6706  1nen2  7090  1ndom2  7094  fidcenumlemrk  7196  djulclb  7314  ismkvnex  7414  pw1ne3  7508  sucpw1nel3  7511  3nsssucpw1  7514  0nnq  7644  0npr  7763  nqprdisj  7824  0ncn  8111  axpre-ltirr  8162  pnfnre  8280  mnfnre  8281  inelr  8823  xrltnr  10075  fzo0  10467  fzouzdisj  10479  inftonninf  10767  hashinfom  11103  lsw0  11227  3prm  12780  sqrt2irr  12814  ennnfonelem1  13108  clwwlknnn  16353  konigsberglem4  16432  bj-nndcALT  16476  bj-vprc  16612  pwle2  16720  exmidsbthrlem  16750