Theorem mtbir 682

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 681	1 |- -. ph

This proof depends on syntax axioms:   -. wn 3   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624

This proof depends on definitions:  df-bi 117

This theorem is used by:  nnexmid  862  nndc  863  fal  1409  ax-9  1584  nonconne  2432  nemtbir  2509  ru  3050  noel  3525  iun0  4069  0iun  4070  br0  4180  vprc  4267  iin0r  4308  nlim0  4541  snnex  4596  onsucelsucexmid  4679  0nelxp  4804  dm0  4997  iprc  5053  co02  5304  0fv  5737  frec0g  6673  nnsucuniel  6773  1nen2  7168  1ndom2  7172  fidcenumlemrk  7278  djulclb  7401  ismkvnex  7501  pw1ne3  7595  sucpw1nel3  7598  3nsssucpw1  7601  0nnq  7737  0npr  7856  nqprdisj  7917  0ncn  8204  axpre-ltirr  8255  pnfnre  8373  mnfnre  8374  inelr  8920  xrltnr  10197  fzo0  10593  fzouzdisj  10605  inftonninf  10899  hashinfom  11238  lsw0  11373  3prm  12930  sqrt2irr  12965  ballotfilem4  13298  ennnfonelem1  13355  clwwlknnn  16875  konigsberglem4  16954  bj-nndcALT  17008  bj-vprc  17144  pwle2  17250  exmidsbthrlem  17290  rals-no-surprise  17372