Theorem mtbir 671

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 670	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 614  ax-in2 615

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nnexmid  850  nndc  851  fal  1360  ax-9  1531  nonconne  2359  nemtbir  2436  ru  2961  noel  3426  iun0  3943  0iun  3944  br0  4051  vprc  4135  iin0r  4169  nlim0  4394  snnex  4448  onsucelsucexmid  4529  0nelxp  4654  dm0  4841  iprc  4895  co02  5142  0fv  5550  frec0g  6397  nnsucuniel  6495  1nen2  6860  fidcenumlemrk  6952  djulclb  7053  ismkvnex  7152  pw1ne3  7228  sucpw1nel3  7231  3nsssucpw1  7234  0nnq  7362  0npr  7481  nqprdisj  7542  0ncn  7829  axpre-ltirr  7880  pnfnre  7998  mnfnre  7999  inelr  8540  xrltnr  9778  fzo0  10167  fzouzdisj  10179  inftonninf  10440  hashinfom  10757  3prm  12127  sqrt2irr  12161  ennnfonelem1  12407  bj-nndcALT  14480  bj-vprc  14618  pwle2  14718  exmidsbthrlem  14740