Theorem mtbir 313

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

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

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 197

This theorem is referenced by:  fal  1490  nemtbir  2889  ru  3434  pssirr  3707  indifdir  3883  noel  3919  npss0OLD  4015  iun0  4576  0iun  4577  br0  4701  vprc  4796  iin0  4839  nfnid  4897  opelopabsb  4985  0nelxp  5143  0nelxpOLD  5144  0xp  5199  nrelv  5244  dm0  5339  cnv0  5535  co02  5649  nlim0  5783  snsn0non  5846  imadif  5973  0fv  6227  snnexOLD  6967  iprc  7101  tfr2b  7492  tz7.44lem1  7501  tz7.48-3  7539  canth2  8113  pwcdadom  9038  canthp1lem2  9475  pwxpndom2  9487  adderpq  9778  mulerpq  9779  0ncn  9954  ax1ne0  9981  pnfnre  10081  mnfnre  10082  inelr  11010  xrltnr  11953  fzouzdisj  12504  lsw0  13352  fprodn0f  14722  eirr  14933  ruc  14972  aleph1re  14974  sqrt2irr  14979  sadc0  15176  1nprm  15392  3prm  15406  prmrec  15626  meet0  17137  join0  17138  odhash  17989  00lsp  18981  cnfldfunALT  19759  zringndrg  19838  zfbas  21700  ustn0  22024  zclmncvs  22948  lhop  23779  dvrelog  24383  axlowdimlem13  25834  ntrl2v2e  27018  konigsberglem4  27117  avril1  27319  helloworld  27321  topnfbey  27325  vsfval  27488  dmadjrnb  28765  xrge00  29686  esumrnmpt2  30130  measvuni  30277  sibf0  30396  ballotlem4  30560  signswch  30638  bnj521  30805  3pm3.2ni  31594  elpotr  31686  dfon2lem7  31694  poseq  31750  nosgnn0  31811  sltsolem1  31826  linedegen  32250  mont  32408  subsym1  32426  limsucncmpi  32444  bj-ru1  32933  bj-0nel1  32940  bj-pinftynrr  33109  bj-minftynrr  33113  bj-pinftynminfty  33114  finxp0  33228  poimirlem30  33439  diophren  37377  eqneltri  39246  stoweidlem44  40261  fourierdlem62  40385  salexct2  40557  aisbnaxb  41078  dandysum2p2e4  41165  257prm  41473  fmtno4nprmfac193  41486  139prmALT  41511  31prm  41512  127prm  41515  nnsum4primeseven  41688  nnsum4primesevenALTV  41689  0nodd  41810  2nodd  41812  1neven  41932  2zrngnring  41952  ex-gt  42469  alsi-no-surprise  42542