Theorem mtbir 661

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 131	. 2 |- ( ps <-> ph )
4	1, 3	mtbi 660	1 |- -. ph

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  nnexmid  840  nndc  841  fal  1350  ax-9  1519  nonconne  2348  nemtbir  2425  ru  2950  noel  3413  iun0  3922  0iun  3923  br0  4030  vprc  4114  iin0r  4148  nlim0  4372  snnex  4426  onsucelsucexmid  4507  0nelxp  4632  dm0  4818  iprc  4872  co02  5117  0fv  5521  frec0g  6365  nnsucuniel  6463  1nen2  6827  fidcenumlemrk  6919  djulclb  7020  ismkvnex  7119  pw1ne3  7186  sucpw1nel3  7189  3nsssucpw1  7192  0nnq  7305  0npr  7424  nqprdisj  7485  0ncn  7772  axpre-ltirr  7823  pnfnre  7940  mnfnre  7941  inelr  8482  xrltnr  9715  fzo0  10103  fzouzdisj  10115  inftonninf  10376  hashinfom  10691  3prm  12060  sqrt2irr  12094  ennnfonelem1  12340  bj-nndcALT  13639  bj-vprc  13778  pwle2  13878  exmidsbthrlem  13901