Theorem mtbiri 327

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 229	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1, 3	mtoi 199	1 ⊢ (𝜑 → ¬ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  psstr  4060  nel02  4292  n0i  4293  sbcel12  4364  sbcel2  4371  sbcbr123  5149  sbcbr  5150  axnul  5247  intex  5286  intnex  5287  iin0  5304  notzfaus  5305  nfcvb  5318  eunex  5332  opelopabsb  5477  brabv  5513  epelg  5524  0nelelxp  5658  elimasni  6046  onxpdisj  6438  ndmfvrcl  6860  canth  7307  oprssdm  7534  ndmovrcl  7539  omelon2  7819  poxp2  8083  xpord2indlem  8087  poxp3  8090  undefnel2  8217  tfr2b  8325  tz7.44-3  8337  nlim2  8415  ord1eln01  8421  ord2eln012  8422  1ellim  8423  2ellim  8424  eceqoveq  8756  2dom  8962  omxpenlem  9002  domunsn  9051  disjen  9058  infensuc  9079  0sdom1dom  9145  1sdom2dom  9153  infn0  9209  elfi2  9323  en3lp  9529  preleqALT  9532  rankxpsuc  9797  updjudhcoinrg  9848  sdomsdomcardi  9886  cardmin2  9914  pm54.43lem  9915  pr2ne  9918  alephgeom  9995  alephval3  10023  cfsuc  10170  cflim2  10176  alephval2  10485  axunnd  10509  canthp1lem1  10565  pwxpndom2  10578  rankcf  10690  pinq  10840  adderpq  10869  mulerpq  10870  nqpr  10927  ltsopr  10945  ltapr  10958  renepnf  11182  renemnf  11183  lt0ne0d  11703  prodgt0  11989  nnne0ALT  12184  nn0nepnf  12483  xrltnr  13039  pnfnlt  13048  nltmnf  13049  xrltnsym  13057  nltpnft  13084  ngtmnft  13086  xsubge0  13181  xmullem2  13185  xlemul1a  13208  xrsupsslem  13227  xrinfmsslem  13228  xrub  13232  fzpreddisj  13494  fzm1  13528  uzinf  13890  hashnemnf  14269  hashclb  14283  hasheq0  14288  hashnn0n0nn  14316  prprrab  14398  tpf1ofv1  14422  tpf1ofv2  14423  lsw0  14490  cats1un  14645  geolim  15795  geolim2  15796  georeclim  15797  geoisumr  15803  m1exp1  16305  bitsfzolem  16363  bitsfzo  16364  bitsinv1lem  16370  sadcp1  16384  saddisjlem  16393  smu01lem  16414  3prm  16623  pcgcd1  16807  pc2dvds  16809  pcmpt  16822  prmreclem5  16850  vdwap0  16906  prmo1  16967  fvprif  17483  setcepi  18013  oduclatb  18431  smndex1n0mnd  18804  cntzrcl  19224  pmtrfrn  19355  pmtrprfval  19384  pmtrprfvalrn  19385  psgnunilem5  19391  odhash3  19473  gsumzaddlem  19818  gsumzsplit  19824  dprdcntz2  19937  trivnsimpgd  19996  0ringnnzr  20428  xrsdsreclblem  21337  dsmmfi  21663  islindf4  21763  mplcoe1  21960  mplcoe5  21963  psrbagsn  21986  pmatcollpw3fi1lem1  22689  istps  22837  haust1  23255  hauspwdom  23404  kqcldsat  23636  csdfil  23797  tsmssplit  24055  dscopn  24477  htpycc  24895  pco1  24931  pcohtpylem  24935  pcopt  24938  pcopt2  24939  pcoass  24940  pcorevlem  24942  itg11  25608  bddmulibl  25756  lhop1  25935  deg1nn0clb  26011  plypf1  26133  vieta1lem2  26235  logdmn0  26565  logcnlem3  26569  fsumharmonic  26938  sqff1o  27108  perfectlem1  27156  bposlem5  27215  lgsval2lem  27234  addsqrexnreu  27369  addsqnreup  27370  ostth  27566  sltval2  27584  sltintdifex  27589  sltres  27590  nolt02o  27623  nogt01o  27624  bday1s  27763  lrold  27829  lrrecpo  27871  mulsval  28035  legso  28562  axlowdimlem13  28917  axlowdimlem16  28920  axlowdim1  28922  axlowdim  28924  upgrfi  29054  lfgrnloop  29088  umgredgnlp  29110  wlkp1lem3  29637  rusgrnumwwlkl1  29931  clwwlk  29945  clwwlkn0  29990  clwwlknon1sn  30062  trlsegvdeg  30189  konigsberg  30219  ex-res  30403  norm1exi  31212  dmadjrnb  31868  strlem1  32212  largei  32229  ifeqeqx  32504  ubico  32731  expgt0b  32774  chnccats1  32970  0ringirng  33660  rtelextdg2lem  33692  2sqr3minply  33746  dya2iocuni  34250  eulerpartlemgh  34345  ballotlem4  34466  plymulx0  34514  signswch  34528  signstfvneq0  34539  signlem0  34554  subfacp1lem1  35151  fmlaomn0  35362  gonan0  35364  goaln0  35365  fmla0disjsuc  35370  ex-sategoelelomsuc  35398  ex-sategoelel12  35399  prv1n  35403  bcneg1  35708  opelco3  35747  wsuclem  35798  dfrdg4  35924  linedegen  36116  rankeq1o  36144  hfninf  36159  ordcmp  36420  curryset  36919  currysetlem3  36922  bj-projval  36969  bj-inftyexpitaudisj  37178  bj-inftyexpidisj  37183  irrdiff  37299  relowlpssretop  37337  finxpreclem2  37363  finxpreclem3  37366  finxpreclem5  37368  nlpineqsn  37381  poimirlem18  37617  poimirlem19  37618  poimirlem20  37619  mblfinlem1  37636  elpadd0  39788  pssn0  42200  oexpreposd  42295  diophin  42745  fiphp3d  42792  expdioph  42996  wepwsolem  43015  kelac1  43036  onov0suclim  43247  tfsconcatb0  43317  ensucne0  43502  relintabex  43554  brnonrel  43562  relexp01min  43686  iooinlbub  45483  stoweidlem34  46016  fourierdlem60  46148  fourierdlem61  46149  tworepnotupword  46868  afv20defat  47217  minusmodnep2tmod  47338  spr0nelg  47461  sprsymrelfvlem  47475  fmtnoinf  47521  fmtno4prmfac193  47558  fmtno4prm  47560  31prm  47582  lighneallem3  47592  lighneallem4  47595  nnsum4primeseven  47785  nnsum4primesevenALTV  47786  dig2nn1st  48591  itcoval1  48649  line2ylem  48737  ipolub00  48978  fucofvalne  49311