Theorem mtbir 666

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 665	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 609  ax-in2 610

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  nnexmid  845  nndc  846  fal  1355  ax-9  1524  nonconne  2352  nemtbir  2429  ru  2954  noel  3418  iun0  3927  0iun  3928  br0  4035  vprc  4119  iin0r  4153  nlim0  4377  snnex  4431  onsucelsucexmid  4512  0nelxp  4637  dm0  4823  iprc  4877  co02  5122  0fv  5529  frec0g  6373  nnsucuniel  6471  1nen2  6835  fidcenumlemrk  6927  djulclb  7028  ismkvnex  7127  pw1ne3  7194  sucpw1nel3  7197  3nsssucpw1  7200  0nnq  7313  0npr  7432  nqprdisj  7493  0ncn  7780  axpre-ltirr  7831  pnfnre  7948  mnfnre  7949  inelr  8490  xrltnr  9723  fzo0  10111  fzouzdisj  10123  inftonninf  10384  hashinfom  10699  3prm  12069  sqrt2irr  12103  ennnfonelem1  12349  bj-nndcALT  13752  bj-vprc  13891  pwle2  13991  exmidsbthrlem  14014