Theorem mtbir 678

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 677	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 619  ax-in2 620

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nnexmid  858  nndc  859  fal  1405  ax-9  1580  nonconne  2426  nemtbir  2503  ru  3044  noel  3516  iun0  4053  0iun  4054  br0  4163  vprc  4247  iin0r  4287  nlim0  4520  snnex  4574  onsucelsucexmid  4657  0nelxp  4782  dm0  4975  iprc  5031  co02  5281  0fv  5713  frec0g  6641  nnsucuniel  6741  1nen2  7128  1ndom2  7132  fidcenumlemrk  7237  djulclb  7359  ismkvnex  7459  pw1ne3  7553  sucpw1nel3  7556  3nsssucpw1  7559  0nnq  7695  0npr  7814  nqprdisj  7875  0ncn  8162  axpre-ltirr  8213  pnfnre  8331  mnfnre  8332  inelr  8875  xrltnr  10131  fzo0  10526  fzouzdisj  10538  inftonninf  10828  hashinfom  11166  lsw0  11297  3prm  12850  sqrt2irr  12884  ballotfilem4  13185  ennnfonelem1  13242  clwwlknnn  16533  konigsberglem4  16612  bj-nndcALT  16656  bj-vprc  16792  pwle2  16898  exmidsbthrlem  16928