Theorem mtbir 305

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 207	. 2 |- ( ps <-> ph )
4	1, 3	mtbi 304	1 |- -. ph

Syntax hints:   -. wn 3   <-> wb 189

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 190

This theorem is referenced by:  fal  1461  nonconneOLD  2647  nemtbir  2730  ru  3277  pssirr  3544  indifdir  3710  noel  3746  npss0  3814  iun0  4347  0iun  4348  br0  4462  vprc  4554  iin0  4590  nfnid  4642  opelopabsb  4724  0nelxp  4880  dm0  5066  co02  5367  nlim0  5499  snsn0non  5559  imadif  5679  0fv  5920  snnex  6623  iprc  6754  tfr2b  7139  tz7.44lem1  7148  tz7.48-3  7186  canth2  7750  pwcdadom  8671  canthp1lem2  9103  pwxpndom2  9115  adderpq  9406  mulerpq  9407  0ncn  9582  ax1ne0  9609  pnfnre  9707  mnfnre  9708  inelr  10626  xrltnr  11449  fzouzdisj  11984  lsw0  12747  fprodn0f  14093  eirr  14305  ruc  14343  aleph1re  14345  sqrt2irr  14349  sadc0  14476  1nprm  14677  3prm  14689  prmrec  14914  meet0  16431  join0  16432  odhash  17271  00lsp  18252  zfbas  20959  ustn0  21283  lhop  23016  dvrelog  23630  axlowdimlem13  25032  uvtx01vtx  25268  avril1  25948  helloworld  25950  topnfbey  25954  vsfval  26302  dmadjrnb  27607  xrge00  28496  esumrnmpt2  28937  measvuni  29084  sibf0  29215  ballotlem4  29379  signswch  29498  bnj521  29593  3pm3.2ni  30393  elpotr  30475  dfon2lem7  30483  poseq  30539  nosgnn0  30593  sltsolem1  30605  linedegen  30958  mont  31117  subsym1  31135  limsucncmpi  31153  bj-ru1  31582  bj-0nel1  31590  bj-pinftynrr  31708  bj-minftynrr  31712  bj-pinftynminfty  31713  finxp0  31827  poimirlem30  32014  diophren  35700  eqneltri  37458  stoweidlem44  37942  fourierdlem62  38069  salexct2  38235  aisbnaxb  38535  dandysum2p2e4  38623  nnsum4primeseven  38932  nnsum4primesevenALTV  38933  ntrl2v2e  39872  0nodd  40082  2nodd  40084  1neven  40204  2zrngnring  40224  ex-gt  40720  alsi-no-surprise  40807