Theorem mtbir 673

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 672	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 615  ax-in2 616

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nnexmid  852  nndc  853  fal  1380  ax-9  1555  nonconne  2390  nemtbir  2467  ru  3004  noel  3472  iun0  3998  0iun  3999  br0  4108  vprc  4192  iin0r  4229  nlim0  4459  snnex  4513  onsucelsucexmid  4596  0nelxp  4721  dm0  4911  iprc  4966  co02  5215  0fv  5635  frec0g  6506  nnsucuniel  6604  1nen2  6983  1ndom2  6987  fidcenumlemrk  7082  djulclb  7183  ismkvnex  7283  pw1ne3  7376  sucpw1nel3  7379  3nsssucpw1  7382  0nnq  7512  0npr  7631  nqprdisj  7692  0ncn  7979  axpre-ltirr  8030  pnfnre  8149  mnfnre  8150  inelr  8692  xrltnr  9936  fzo0  10327  fzouzdisj  10339  inftonninf  10624  hashinfom  10960  lsw0  11078  3prm  12565  sqrt2irr  12599  ennnfonelem1  12893  bj-nndcALT  15894  bj-vprc  16031  pwle2  16137  exmidsbthrlem  16163