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  1545  nonconne  2379  nemtbir  2456  ru  2988  noel  3454  iun0  3973  0iun  3974  br0  4081  vprc  4165  iin0r  4202  nlim0  4429  snnex  4483  onsucelsucexmid  4566  0nelxp  4691  dm0  4880  iprc  4934  co02  5183  0fv  5594  frec0g  6455  nnsucuniel  6553  1nen2  6922  fidcenumlemrk  7020  djulclb  7121  ismkvnex  7221  pw1ne3  7297  sucpw1nel3  7300  3nsssucpw1  7303  0nnq  7431  0npr  7550  nqprdisj  7611  0ncn  7898  axpre-ltirr  7949  pnfnre  8068  mnfnre  8069  inelr  8611  xrltnr  9854  fzo0  10244  fzouzdisj  10256  inftonninf  10534  hashinfom  10870  3prm  12296  sqrt2irr  12330  ennnfonelem1  12624  bj-nndcALT  15404  bj-vprc  15542  pwle2  15643  exmidsbthrlem  15666