Theorem mtbir 672

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 671	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  851  nndc  852  fal  1371  ax-9  1542  nonconne  2376  nemtbir  2453  ru  2984  noel  3450  iun0  3969  0iun  3970  br0  4077  vprc  4161  iin0r  4198  nlim0  4425  snnex  4479  onsucelsucexmid  4562  0nelxp  4687  dm0  4876  iprc  4930  co02  5179  0fv  5590  frec0g  6450  nnsucuniel  6548  1nen2  6917  fidcenumlemrk  7013  djulclb  7114  ismkvnex  7214  pw1ne3  7290  sucpw1nel3  7293  3nsssucpw1  7296  0nnq  7424  0npr  7543  nqprdisj  7604  0ncn  7891  axpre-ltirr  7942  pnfnre  8061  mnfnre  8062  inelr  8603  xrltnr  9845  fzo0  10235  fzouzdisj  10247  inftonninf  10513  hashinfom  10849  3prm  12266  sqrt2irr  12300  ennnfonelem1  12564  bj-nndcALT  15250  bj-vprc  15388  pwle2  15489  exmidsbthrlem  15512