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

Theorem mtbiri 317
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 219 . 2 (𝜑 → (𝜓𝜒))
41, 3mtoi 190 1 (𝜑 → ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196
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 197
This theorem is referenced by:  psstr  3703  n0i  3912  sbcel12  3974  sbcel2  3980  sbcbr123  4697  sbcbr  4698  axnul  4779  intex  4811  intnex  4812  iin0  4830  nfcvb  4889  opelopabsb  4975  0nelelxp  5135  elimasni  5480  0ellim  5775  onxpdisj  5835  ndmfvrcl  6206  canth  6593  fvmptopab  6682  brabv  6684  oprssdm  6800  ndmovrcl  6805  omelon2  7062  undefnel2  7388  tfr2b  7477  tz7.44-3  7489  omeulem1  7647  eceqoveq  7838  2dom  8014  omxpenlem  8046  domunsn  8095  disjen  8102  infensuc  8123  snnen2o  8134  elfi2  8305  en3lp  8498  preleq  8499  rankxpsuc  8730  sdomsdomcardi  8782  cardmin2  8809  pm54.43lem  8810  alephgeom  8890  alephval3  8918  pwcdadom  9023  cfsuc  9064  cflim2  9070  alephval2  9379  axunnd  9403  canthp1lem1  9459  pwxpndom2  9472  rankcf  9584  pinq  9734  adderpq  9763  mulerpq  9764  nqpr  9821  ltsopr  9839  ltapr  9852  renepnf  10072  renemnf  10073  lt0ne0d  10578  prodgt0  10853  nnne0  11038  nn0nepnf  11356  xrltnr  11938  pnfnlt  11947  nltmnf  11948  xrltnsym  11955  nltpnft  11980  ngtmnft  11982  xsubge0  12076  xmullem2  12080  xlemul1a  12103  xrsupsslem  12122  xrinfmsslem  12123  xrub  12127  fzpreddisj  12375  fzm1  12404  uzinf  12747  hashnemnf  13115  hashclb  13132  hasheq0  13137  hashnn0n0nn  13163  prprrab  13238  lsw0  13335  cats1un  13457  geolim  14582  geolim2  14583  georeclim  14584  geoisumr  14590  m1exp1  15074  bitsfzolem  15137  bitsfzo  15138  bitsinv1lem  15144  sadcp1  15158  saddisjlem  15167  smu01lem  15188  3prm  15387  pcgcd1  15562  pc2dvds  15564  pcmpt  15577  prmreclem5  15605  vdwap0  15661  setcepi  16719  oduclatb  17125  cntzrcl  17741  pmtrfrn  17859  pmtrprfval  17888  pmtrprfvalrn  17889  psgnunilem5  17895  odhash3  17972  gsumzaddlem  18302  gsumzsplit  18308  dprdcntz2  18418  0ringnnzr  19250  mplcoe1  19446  mplcoe5  19449  psrbagsn  19476  xrsdsreclblem  19773  dsmmbas2  20062  dsmmfi  20063  islindf4  20158  pmatcollpw3fi1lem1  20572  istps  20719  haust1  21137  hauspwdom  21285  kqcldsat  21517  csdfil  21679  tsmssplit  21936  dscopn  22359  htpycc  22760  pco1  22796  pcohtpylem  22800  pcopt  22803  pcopt2  22804  pcoass  22805  pcorevlem  22807  itg11  23439  bddmulibl  23586  lhop1  23758  deg1nn0clb  23831  plypf1  23949  vieta1lem2  24047  logdmn0  24367  logcnlem3  24371  fsumharmonic  24719  sqff1o  24889  perfectlem1  24935  bposlem5  24994  lgsval2lem  25013  ostth  25309  legso  25475  axlowdimlem13  25815  axlowdimlem16  25818  axlowdim1  25820  axlowdim  25822  upgrfi  25967  lfgrnloop  26001  umgredgnlp  26023  uvtxa01vtx  26279  wlkp1lem3  26553  rusgrnumwwlkl1  26844  clwwlks  26860  trlsegvdeg  27067  konigsberg  27099  ex-res  27268  norm1exi  28077  dmadjrnb  28735  strlem1  29079  largei  29096  ifeqeqx  29333  ubico  29511  dya2iocuni  30319  eulerpartlemgh  30414  ballotlem4  30534  plymulx0  30598  signswch  30612  signstfvneq0  30623  signlem0  30638  subfacp1lem1  31135  bcneg1  31597  opelco3  31652  wsuclem  31747  wsuclemOLD  31748  sltval2  31783  sltintdifex  31788  sltres  31789  nolt02o  31819  dfrdg4  32033  linedegen  32225  rankeq1o  32253  hfninf  32268  ordcmp  32421  bj-projval  32959  bj-inftyexpidisj  33068  relowlpssretop  33183  finxpreclem2  33198  finxpreclem3  33201  finxpreclem5  33203  poimirlem18  33398  poimirlem19  33399  poimirlem20  33400  mblfinlem1  33417  elpadd0  34914  diophin  37155  fiphp3d  37202  expdioph  37409  wepwsolem  37431  kelac1  37452  relintabex  37706  brnonrel  37714  relexp01min  37824  iooinlbub  39526  stoweidlem34  40014  fourierdlem60  40146  fourierdlem61  40147  fmtnoinf  41213  fmtno4prmfac193  41250  fmtno4prm  41252  31prm  41277  lighneallem3  41289  lighneallem4  41292  nnsum4primeseven  41453  nnsum4primesevenALTV  41454  spr0nelg  41491  sprsymrelfvlem  41505  dig2nn1st  42164
  Copyright terms: Public domain W3C validator