Theorem mtbir 673

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 672	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  852  nndc  853  fal  1380  ax-9  1554  nonconne  2388  nemtbir  2465  ru  2997  noel  3464  iun0  3984  0iun  3985  br0  4093  vprc  4177  iin0r  4214  nlim0  4442  snnex  4496  onsucelsucexmid  4579  0nelxp  4704  dm0  4893  iprc  4948  co02  5197  0fv  5614  frec0g  6485  nnsucuniel  6583  1nen2  6960  fidcenumlemrk  7058  djulclb  7159  ismkvnex  7259  pw1ne3  7344  sucpw1nel3  7347  3nsssucpw1  7350  0nnq  7479  0npr  7598  nqprdisj  7659  0ncn  7946  axpre-ltirr  7997  pnfnre  8116  mnfnre  8117  inelr  8659  xrltnr  9903  fzo0  10294  fzouzdisj  10306  inftonninf  10589  hashinfom  10925  lsw0  11043  3prm  12483  sqrt2irr  12517  ennnfonelem1  12811  bj-nndcALT  15731  bj-vprc  15869  pwle2  15972  exmidsbthrlem  15998