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  6672  nnsucuniel  6772  1nen2  7166  1ndom2  7170  fidcenumlemrk  7276  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  10198  fzo0  10594  fzouzdisj  10606  inftonninf  10900  hashinfom  11239  lsw0  11374  3prm  12931  sqrt2irr  12966  ballotfilem4  13299  ennnfonelem1  13356  clwwlknnn  16858  konigsberglem4  16937  bj-nndcALT  16991  bj-vprc  17127  pwle2  17233  exmidsbthrlem  17273  rals-no-surprise  17355