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  2372  nemtbir  2449  ru  2976  noel  3441  iun0  3958  0iun  3959  br0  4066  vprc  4150  iin0r  4187  nlim0  4412  snnex  4466  onsucelsucexmid  4547  0nelxp  4672  dm0  4859  iprc  4913  co02  5160  0fv  5570  frec0g  6422  nnsucuniel  6520  1nen2  6889  fidcenumlemrk  6983  djulclb  7084  ismkvnex  7183  pw1ne3  7259  sucpw1nel3  7262  3nsssucpw1  7265  0nnq  7393  0npr  7512  nqprdisj  7573  0ncn  7860  axpre-ltirr  7911  pnfnre  8029  mnfnre  8030  inelr  8571  xrltnr  9809  fzo0  10198  fzouzdisj  10210  inftonninf  10472  hashinfom  10790  3prm  12160  sqrt2irr  12194  ennnfonelem1  12458  bj-nndcALT  14971  bj-vprc  15109  pwle2  15210  exmidsbthrlem  15232