Theorem mtbir 672

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 671	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 615  ax-in2 616

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nnexmid  851  nndc  852  fal  1371  ax-9  1542  nonconne  2376  nemtbir  2453  ru  2985  noel  3451  iun0  3970  0iun  3971  br0  4078  vprc  4162  iin0r  4199  nlim0  4426  snnex  4480  onsucelsucexmid  4563  0nelxp  4688  dm0  4877  iprc  4931  co02  5180  0fv  5591  frec0g  6452  nnsucuniel  6550  1nen2  6919  fidcenumlemrk  7015  djulclb  7116  ismkvnex  7216  pw1ne3  7292  sucpw1nel3  7295  3nsssucpw1  7298  0nnq  7426  0npr  7545  nqprdisj  7606  0ncn  7893  axpre-ltirr  7944  pnfnre  8063  mnfnre  8064  inelr  8605  xrltnr  9848  fzo0  10238  fzouzdisj  10250  inftonninf  10516  hashinfom  10852  3prm  12269  sqrt2irr  12303  ennnfonelem1  12567  bj-nndcALT  15320  bj-vprc  15458  pwle2  15559  exmidsbthrlem  15582