Theorem mtbir 675

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 674	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 617  ax-in2 618

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nnexmid  855  nndc  856  fal  1402  ax-9  1577  nonconne  2412  nemtbir  2489  ru  3027  noel  3495  iun0  4022  0iun  4023  br0  4132  vprc  4216  iin0r  4253  nlim0  4485  snnex  4539  onsucelsucexmid  4622  0nelxp  4747  dm0  4937  iprc  4993  co02  5242  0fv  5665  frec0g  6543  nnsucuniel  6641  1nen2  7022  1ndom2  7026  fidcenumlemrk  7121  djulclb  7222  ismkvnex  7322  pw1ne3  7415  sucpw1nel3  7418  3nsssucpw1  7421  0nnq  7551  0npr  7670  nqprdisj  7731  0ncn  8018  axpre-ltirr  8069  pnfnre  8188  mnfnre  8189  inelr  8731  xrltnr  9975  fzo0  10366  fzouzdisj  10378  inftonninf  10664  hashinfom  11000  lsw0  11119  3prm  12650  sqrt2irr  12684  ennnfonelem1  12978  bj-nndcALT  16122  bj-vprc  16259  pwle2  16364  exmidsbthrlem  16390