Theorem mtbir 323

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	⊢ ¬ 𝜓
mtbir.2	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
mtbir	⊢ ¬ 𝜑

Proof of Theorem mtbir

Step	Hyp	Ref	Expression
1		mtbir.1	. 2 ⊢ ¬ 𝜓
2		mtbir.2	. . 3 ⊢ (𝜑 ↔ 𝜓)
3	2	bicomi 223	. 2 ⊢ (𝜓 ↔ 𝜑)
4	1, 3	mtbi 322	1 ⊢ ¬ 𝜑

Syntax hints:  ¬ wn 3   ↔ wb 205

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 206

This theorem is referenced by:  3pm3.2ni  1489  fal  1556  eqneltri  2853  nemtbir  3039  ru  3777  pssirr  4101  indifdirOLD  4286  noel  4331  noelOLD  4332  iun0  5066  0iun  5067  br0  5198  vprc  5316  iin0  5361  nfnid  5374  opelopabsb  5531  0nelopab  5568  0nelxp  5711  0xp  5775  nrelv  5801  dm0  5921  cnv0  6141  co02  6260  nlim0  6424  snsn0non  6490  imadif  6633  0fv  6936  poxp2  8129  poseq  8144  tz7.44lem1  8405  nlim1  8489  nlim2  8490  sdom0  9108  canth2  9130  snnen2o  9237  1sdom2  9240  canthp1lem2  10648  pwxpndom2  10660  adderpq  10951  mulerpq  10952  0ncn  11128  ax1ne0  11155  inelr  12202  xrltnr  13099  fzouzdisj  13668  lsw0  14515  eirr  16148  ruc  16186  aleph1re  16188  sqrt2irr  16192  n2dvds1  16311  n2dvds3  16314  sadc0  16395  1nprm  16616  join0  18358  meet0  18359  smndex1n0mnd  18793  nsmndex1  18794  smndex2dnrinv  18796  odhash  19442  cnfldfun  20956  zringndrg  21038  zfbas  23400  ustn0  23725  zclmncvs  24665  lhop  25533  dvrelog  26145  nosgnn0  27161  sltsolem1  27178  addsrid  27448  muls01  27568  mulsrid  27569  axlowdimlem13  28212  ntrl2v2e  29411  konigsberglem4  29508  avril1  29716  helloworld  29718  topnfbey  29722  vsfval  29886  dmadjrnb  31159  xrge00  32187  esumrnmpt2  33066  measvuni  33212  sibf0  33333  ballotlem4  33497  signswch  33572  satf0n0  34369  fmlaomn0  34381  gonan0  34383  goaln0  34384  fmla0disjsuc  34389  elpotr  34753  dfon2lem7  34761  linedegen  35115  nmotru  35293  limsucncmpi  35330  bj-ru1  35824  bj-0nel1  35834  bj-inftyexpitaudisj  36086  bj-pinftynminfty  36108  finxp0  36272  poimirlem30  36518  coss0  37349  epnsymrel  37432  diophren  41551  notbicom  43860  rexanuz2nf  44203  stoweidlem44  44760  fourierdlem62  44884  salexct2  45055  aisbnaxb  45621  dandysum2p2e4  45708  iota0ndef  45749  aiota0ndef  45805  257prm  46229  fmtno4nprmfac193  46242  139prmALT  46264  31prm  46265  127prm  46267  nnsum4primeseven  46468  nnsum4primesevenALTV  46469  0nodd  46580  2nodd  46582  1neven  46830  2zrngnring  46850  ex-gt  47773  alsi-no-surprise  47843