Theorem mtbiri 326

Description: An inference from a biconditional, similar to modus tollens. (Contributed by NM, 24-Aug-1995.)

Hypotheses

Ref	Expression
mtbiri.min	⊢ ¬ 𝜒
mtbiri.maj	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
mtbiri	⊢ (𝜑 → ¬ 𝜓)

Proof of Theorem mtbiri

Step	Hyp	Ref	Expression
1		mtbiri.min	. 2 ⊢ ¬ 𝜒
2		mtbiri.maj	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	2	biimpd 228	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1, 3	mtoi 198	1 ⊢ (𝜑 → ¬ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ↔ 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:  psstr  4035  nel02  4263  n0i  4264  sbcel12  4339  sbcel2  4346  sbcbr123  5124  sbcbr  5125  axnul  5224  intex  5256  intnex  5257  iin0  5279  notzfaus  5280  nfcvb  5294  eunex  5308  opelopabsb  5436  brabv  5473  epelg  5487  0nelelxp  5615  elimasni  5988  0ellim  6313  onxpdisj  6371  ndmfvrcl  6787  canth  7209  fvmptopab  7308  oprssdm  7431  ndmovrcl  7436  omelon2  7700  undefnel2  8064  tfr2b  8198  tz7.44-3  8210  eceqoveq  8569  2dom  8774  omxpenlem  8813  domunsn  8863  disjen  8870  infensuc  8891  snnen2o  8903  elfi2  9103  en3lp  9302  preleqALT  9305  rankxpsuc  9571  updjudhcoinrg  9622  sdomsdomcardi  9660  cardmin2  9688  pm54.43lem  9689  alephgeom  9769  alephval3  9797  cfsuc  9944  cflim2  9950  alephval2  10259  axunnd  10283  canthp1lem1  10339  pwxpndom2  10352  rankcf  10464  pinq  10614  adderpq  10643  mulerpq  10644  nqpr  10701  ltsopr  10719  ltapr  10732  renepnf  10954  renemnf  10955  lt0ne0d  11470  prodgt0  11752  nnne0ALT  11941  nn0nepnf  12243  xrltnr  12784  pnfnlt  12793  nltmnf  12794  xrltnsym  12800  nltpnft  12827  ngtmnft  12829  xsubge0  12924  xmullem2  12928  xlemul1a  12951  xrsupsslem  12970  xrinfmsslem  12971  xrub  12975  fzpreddisj  13234  fzm1  13265  uzinf  13613  hashnemnf  13986  hashclb  14001  hasheq0  14006  hashnn0n0nn  14034  prprrab  14115  lsw0  14196  cats1un  14362  geolim  15510  geolim2  15511  georeclim  15512  geoisumr  15518  m1exp1  16013  bitsfzolem  16069  bitsfzo  16070  bitsinv1lem  16076  sadcp1  16090  saddisjlem  16099  smu01lem  16120  3prm  16327  pcgcd1  16506  pc2dvds  16508  pcmpt  16521  prmreclem5  16549  vdwap0  16605  prmo1  16666  fvprif  17189  setcepi  17719  oduclatb  18140  smndex1n0mnd  18466  cntzrcl  18848  pmtrfrn  18981  pmtrprfval  19010  pmtrprfvalrn  19011  psgnunilem5  19017  odhash3  19096  gsumzaddlem  19437  gsumzsplit  19443  dprdcntz2  19556  trivnsimpgd  19615  0ringnnzr  20453  xrsdsreclblem  20556  dsmmfi  20855  islindf4  20955  mplcoe1  21148  mplcoe5  21151  psrbagsn  21181  pmatcollpw3fi1lem1  21843  istps  21991  haust1  22411  hauspwdom  22560  kqcldsat  22792  csdfil  22953  tsmssplit  23211  dscopn  23635  htpycc  24049  pco1  24084  pcohtpylem  24088  pcopt  24091  pcopt2  24092  pcoass  24093  pcorevlem  24095  itg11  24760  bddmulibl  24908  lhop1  25083  deg1nn0clb  25160  plypf1  25278  vieta1lem2  25376  logdmn0  25700  logcnlem3  25704  fsumharmonic  26066  sqff1o  26236  perfectlem1  26282  bposlem5  26341  lgsval2lem  26360  addsqrexnreu  26495  addsqnreup  26496  ostth  26692  legso  26864  axlowdimlem13  27225  axlowdimlem16  27228  axlowdim1  27230  axlowdim  27232  upgrfi  27364  lfgrnloop  27398  umgredgnlp  27420  wlkp1lem3  27945  rusgrnumwwlkl1  28234  clwwlk  28248  clwwlkn0  28293  clwwlknon1sn  28365  trlsegvdeg  28492  konigsberg  28522  ex-res  28706  norm1exi  29513  dmadjrnb  30169  strlem1  30513  largei  30530  ifeqeqx  30786  ubico  30998  dya2iocuni  32150  eulerpartlemgh  32245  ballotlem4  32365  plymulx0  32426  signswch  32440  signstfvneq0  32451  signlem0  32466  subfacp1lem1  33041  fmlaomn0  33252  gonan0  33254  goaln0  33255  fmla0disjsuc  33260  ex-sategoelelomsuc  33288  ex-sategoelel12  33289  prv1n  33293  bcneg1  33608  opelco3  33655  poxp2  33717  xpord2ind  33721  poxp3  33723  xpord3ind  33727  wsuclem  33746  sltval2  33786  sltintdifex  33791  sltres  33792  nolt02o  33825  nogt01o  33826  bday1s  33952  lrold  34004  lrrecpo  34025  dfrdg4  34180  linedegen  34372  rankeq1o  34400  hfninf  34415  ordcmp  34563  curryset  35062  currysetlem3  35065  bj-projval  35113  bj-inftyexpitaudisj  35303  bj-inftyexpidisj  35308  irrdiff  35424  relowlpssretop  35462  finxpreclem2  35488  finxpreclem3  35491  finxpreclem5  35493  nlpineqsn  35506  poimirlem18  35722  poimirlem19  35723  poimirlem20  35724  mblfinlem1  35741  elpadd0  37750  pssn0  40128  oexpreposd  40242  diophin  40510  fiphp3d  40557  expdioph  40761  wepwsolem  40783  kelac1  40804  ensucne0  41034  relintabex  41078  brnonrel  41086  relexp01min  41210  iooinlbub  42929  stoweidlem34  43465  fourierdlem60  43597  fourierdlem61  43598  afv20defat  44611  spr0nelg  44816  sprsymrelfvlem  44830  fmtnoinf  44876  fmtno4prmfac193  44913  fmtno4prm  44915  31prm  44937  lighneallem3  44947  lighneallem4  44950  nnsum4primeseven  45140  nnsum4primesevenALTV  45141  dig2nn1st  45839  itcoval1  45897  line2ylem  45985  ipolub00  46167