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  1545  nonconne  2379  nemtbir  2456  ru  2988  noel  3455  iun0  3974  0iun  3975  br0  4082  vprc  4166  iin0r  4203  nlim0  4430  snnex  4484  onsucelsucexmid  4567  0nelxp  4692  dm0  4881  iprc  4935  co02  5184  0fv  5597  frec0g  6464  nnsucuniel  6562  1nen2  6931  fidcenumlemrk  7029  djulclb  7130  ismkvnex  7230  pw1ne3  7313  sucpw1nel3  7316  3nsssucpw1  7319  0nnq  7448  0npr  7567  nqprdisj  7628  0ncn  7915  axpre-ltirr  7966  pnfnre  8085  mnfnre  8086  inelr  8628  xrltnr  9871  fzo0  10261  fzouzdisj  10273  inftonninf  10551  hashinfom  10887  3prm  12321  sqrt2irr  12355  ennnfonelem1  12649  bj-nndcALT  15488  bj-vprc  15626  pwle2  15729  exmidsbthrlem  15753