Theorem mtbir 632

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 631	1 |- -. ph

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  fal  1297  ax-9  1470  nonconne  2268  nemtbir  2345  ru  2840  noel  3291  iun0  3792  0iun  3793  vprc  3977  iin0r  4010  nlim0  4230  snnex  4283  onsucelsucexmid  4359  0nelxp  4479  dm0  4663  iprc  4714  co02  4957  0fv  5352  frec0g  6176  nnsucuniel  6270  1nen2  6631  fidcenumlemrk  6717  djulclb  6801  0nnq  6984  0npr  7103  nqprdisj  7164  0ncn  7430  axpre-ltirr  7478  pnfnre  7590  mnfnre  7591  inelr  8122  xrltnr  9311  fzo0  9640  fzouzdisj  9652  inftonninf  9908  hashinfom  10247  3prm  11449  sqrt2irr  11480  nnexmid  11933  nndc  11934  bj-vprc  12060  exmidsbthrlem  12184