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  836  nndc  837  fal  1339  ax-9  1512  nonconne  2321  nemtbir  2398  ru  2912  noel  3372  iun0  3877  0iun  3878  br0  3984  vprc  4068  iin0r  4101  nlim0  4324  snnex  4377  onsucelsucexmid  4453  0nelxp  4575  dm0  4761  iprc  4815  co02  5060  0fv  5464  frec0g  6302  nnsucuniel  6399  1nen2  6763  fidcenumlemrk  6850  djulclb  6948  ismkvnex  7037  0nnq  7196  0npr  7315  nqprdisj  7376  0ncn  7663  axpre-ltirr  7714  pnfnre  7831  mnfnre  7832  inelr  8370  xrltnr  9596  fzo0  9976  fzouzdisj  9988  inftonninf  10245  hashinfom  10556  3prm  11845  sqrt2irr  11876  ennnfonelem1  11956  bj-nndcALT  13134  bj-vprc  13265  pwle2  13366  exmidsbthrlem  13392