Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  mtbiri Structured version   Visualization version   GIF version

Theorem mtbiri 330
 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
StepHypRef Expression
1 mtbiri.min . 2 ¬ 𝜒
2 mtbiri.maj . . 3 (𝜑 → (𝜓𝜒))
32biimpd 232 . 2 (𝜑 → (𝜓𝜒))
41, 3mtoi 202 1 (𝜑 → ¬ 𝜓)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209 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 210 This theorem is referenced by:  psstr  4035  nel02  4251  n0i  4252  sbcel12  4319  sbcel2  4326  sbcbr123  5087  sbcbr  5088  axnul  5176  intex  5207  intnex  5208  iin0  5229  notzfaus  5230  nfcvb  5245  eunex  5259  opelopabsb  5385  brabv  5421  epelg  5434  0nelelxp  5558  elimasni  5927  0ellim  6225  onxpdisj  6282  ndmfvrcl  6680  canth  7094  fvmptopab  7192  oprssdm  7313  ndmovrcl  7318  omelon2  7576  undefnel2  7930  tfr2b  8019  tz7.44-3  8031  eceqoveq  8389  2dom  8569  omxpenlem  8605  domunsn  8655  disjen  8662  infensuc  8683  snnen2o  8695  elfi2  8866  en3lp  9065  preleqALT  9068  rankxpsuc  9299  updjudhcoinrg  9350  sdomsdomcardi  9388  cardmin2  9416  pm54.43lem  9417  alephgeom  9497  alephval3  9525  cfsuc  9672  cflim2  9678  alephval2  9987  axunnd  10011  canthp1lem1  10067  pwxpndom2  10080  rankcf  10192  pinq  10342  adderpq  10371  mulerpq  10372  nqpr  10429  ltsopr  10447  ltapr  10460  renepnf  10682  renemnf  10683  lt0ne0d  11198  prodgt0  11480  nnne0ALT  11667  nn0nepnf  11967  xrltnr  12506  pnfnlt  12515  nltmnf  12516  xrltnsym  12522  nltpnft  12549  ngtmnft  12551  xsubge0  12646  xmullem2  12650  xlemul1a  12673  xrsupsslem  12692  xrinfmsslem  12693  xrub  12697  fzpreddisj  12955  fzm1  12986  uzinf  13332  hashnemnf  13704  hashclb  13719  hasheq0  13724  hashnn0n0nn  13752  prprrab  13831  lsw0  13912  cats1un  14078  geolim  15221  geolim2  15222  georeclim  15223  geoisumr  15229  m1exp1  15720  bitsfzolem  15776  bitsfzo  15777  bitsinv1lem  15783  sadcp1  15797  saddisjlem  15806  smu01lem  15827  3prm  16031  pcgcd1  16206  pc2dvds  16208  pcmpt  16221  prmreclem5  16249  vdwap0  16305  prmo1  16366  fvprif  16829  setcepi  17343  oduclatb  17749  smndex1n0mnd  18072  cntzrcl  18452  pmtrfrn  18581  pmtrprfval  18610  pmtrprfvalrn  18611  psgnunilem5  18617  odhash3  18696  gsumzaddlem  19037  gsumzsplit  19043  dprdcntz2  19156  trivnsimpgd  19215  0ringnnzr  20038  xrsdsreclblem  20140  dsmmfi  20430  islindf4  20530  mplcoe1  20708  mplcoe5  20711  psrbagsn  20737  pmatcollpw3fi1lem1  21394  istps  21542  haust1  21960  hauspwdom  22109  kqcldsat  22341  csdfil  22502  tsmssplit  22760  dscopn  23183  htpycc  23588  pco1  23623  pcohtpylem  23627  pcopt  23630  pcopt2  23631  pcoass  23632  pcorevlem  23634  itg11  24298  bddmulibl  24445  lhop1  24620  deg1nn0clb  24694  plypf1  24812  vieta1lem2  24910  logdmn0  25234  logcnlem3  25238  fsumharmonic  25600  sqff1o  25770  perfectlem1  25816  bposlem5  25875  lgsval2lem  25894  addsqrexnreu  26029  addsqnreup  26030  ostth  26226  legso  26396  axlowdimlem13  26751  axlowdimlem16  26754  axlowdim1  26756  axlowdim  26758  upgrfi  26887  lfgrnloop  26921  umgredgnlp  26943  wlkp1lem3  27468  rusgrnumwwlkl1  27757  clwwlk  27771  clwwlkn0  27816  clwwlknon1sn  27888  trlsegvdeg  28015  konigsberg  28045  ex-res  28229  norm1exi  29036  dmadjrnb  29692  strlem1  30036  largei  30053  ifeqeqx  30312  ubico  30527  dya2iocuni  31649  eulerpartlemgh  31744  ballotlem4  31864  plymulx0  31925  signswch  31939  signstfvneq0  31950  signlem0  31965  subfacp1lem1  32534  fmlaomn0  32745  gonan0  32747  goaln0  32748  fmla0disjsuc  32753  ex-sategoelelomsuc  32781  ex-sategoelel12  32782  prv1n  32786  bcneg1  33076  opelco3  33126  wsuclem  33220  sltval2  33271  sltintdifex  33276  sltres  33277  nolt02o  33307  dfrdg4  33520  linedegen  33712  rankeq1o  33740  hfninf  33755  ordcmp  33903  curryset  34376  currysetlem3  34379  bj-projval  34427  bj-inftyexpitaudisj  34615  bj-inftyexpidisj  34620  irrdiff  34735  relowlpssretop  34776  finxpreclem2  34802  finxpreclem3  34805  finxpreclem5  34807  nlpineqsn  34820  poimirlem18  35068  poimirlem19  35069  poimirlem20  35070  mblfinlem1  35087  elpadd0  37098  pssn0  39394  oexpreposd  39474  diophin  39700  fiphp3d  39747  expdioph  39951  wepwsolem  39973  kelac1  39994  ensucne0  40224  relintabex  40268  brnonrel  40276  relexp01min  40401  iooinlbub  42125  stoweidlem34  42663  fourierdlem60  42795  fourierdlem61  42796  afv20defat  43775  spr0nelg  43980  sprsymrelfvlem  43994  fmtnoinf  44040  fmtno4prmfac193  44077  fmtno4prm  44079  31prm  44101  lighneallem3  44112  lighneallem4  44115  nnsum4primeseven  44305  nnsum4primesevenALTV  44306  dig2nn1st  45006  itcoval1  45064  line2ylem  45152
 Copyright terms: Public domain W3C validator