Theorem mtbir 299

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

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

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 185

This theorem is referenced by:  fal  1386  nonconneOLD  2676  nemtbir  2795  ru  3330  pssirr  3604  indifdir  3754  noel  3789  npss0  3865  iun0  4381  0iun  4382  br0  4493  sbcbr123  4498  vprc  4585  iin0  4621  nfnid  4676  opelopabsb  4757  nlim0  4936  snsn0non  4996  0nelxp  5027  dm0  5216  co02  5521  imadif  5663  0fv  5899  snnex  6590  iprc  6719  tfr2b  7065  tz7.44lem1  7071  tz7.48-3  7109  0we1  7156  canth2  7670  pwcdadom  8596  brdom3  8906  canthwe  9029  canthp1lem2  9031  pwxpndom2  9043  adderpq  9334  mulerpq  9335  0ncn  9510  ax1ne0  9537  pnfnre  9635  mnfnre  9636  inelr  10526  xrltnr  11330  fzouzdisj  11829  eirr  13799  ruc  13837  aleph1re  13839  sqrt2irr  13843  sadc0  13963  1nprm  14081  3prm  14093  prmrec  14299  meet0  15624  join0  15625  odhash  16400  00lsp  17427  zfbas  20160  ustn0  20486  lhop  22180  dvrelog  22774  axlowdimlem13  23961  uvtx01vtx  24196  avril1  24875  helloworld  24877  vsfval  25232  dmadjrnb  26529  xrge00  27364  measvuni  27853  sibf0  27944  ballotlem4  28105  signswch  28186  3pm3.2ni  28593  elpotr  28818  dfon2lem7  28826  poseq  28938  nosgnn0  29023  sltsolem1  29033  linedegen  29398  mont  29479  subsym1  29497  limsucncmpi  29515  diophren  30379  stoweidlem44  31372  fourierdlem62  31497  aisbnaxb  31601  dandysum2p2e4  31665  ex-gt  32221  alsi-no-surprise  32310  bnj521  32890  bj-ru1  33600  bj-0nel1  33608  bj-pinftynrr  33715  bj-minftynrr  33719  bj-pinftynminfty  33720