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

Theorem mtbiri 316
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  3841  n0i  4051  sbcel12  4114  sbcel2  4120  sbcbr123  4846  sbcbr  4847  axnul  4928  intex  4957  intnex  4958  iin0  4976  nfcvb  5035  opelopabsb  5123  0nelelxp  5290  elimasni  5638  0ellim  5936  onxpdisj  5996  ndmfvrcl  6368  canth  6759  fvmptopab  6850  brabv  6852  oprssdm  6968  ndmovrcl  6973  omelon2  7230  undefnel2  7560  tfr2b  7649  tz7.44-3  7661  omeulem1  7819  eceqoveq  8007  2dom  8182  omxpenlem  8214  domunsn  8263  disjen  8270  infensuc  8291  snnen2o  8302  elfi2  8473  en3lp  8670  preleqALT  8673  preleqOLD  8675  rankxpsuc  8906  sdomsdomcardi  8958  cardmin2  8985  pm54.43lem  8986  alephgeom  9066  alephval3  9094  pwcdadom  9201  cfsuc  9242  cflim2  9248  alephval2  9557  axunnd  9581  canthp1lem1  9637  pwxpndom2  9650  rankcf  9762  pinq  9912  adderpq  9941  mulerpq  9942  nqpr  9999  ltsopr  10017  ltapr  10030  renepnf  10250  renemnf  10251  lt0ne0d  10756  prodgt0  11031  nnne0  11216  nn0nepnf  11534  xrltnr  12117  pnfnlt  12126  nltmnf  12127  xrltnsym  12134  nltpnft  12159  ngtmnft  12161  xsubge0  12255  xmullem2  12259  xlemul1a  12282  xrsupsslem  12301  xrinfmsslem  12302  xrub  12306  fzpreddisj  12554  fzm1  12584  uzinf  12929  hashnemnf  13297  hashclb  13312  hasheq0  13317  hashnn0n0nn  13343  prprrab  13418  lsw0  13510  cats1un  13646  geolim  14771  geolim2  14772  georeclim  14773  geoisumr  14779  m1exp1  15266  bitsfzolem  15329  bitsfzo  15330  bitsinv1lem  15336  sadcp1  15350  saddisjlem  15359  smu01lem  15380  3prm  15579  pcgcd1  15754  pc2dvds  15756  pcmpt  15769  prmreclem5  15797  vdwap0  15853  setcepi  16910  oduclatb  17316  cntzrcl  17931  pmtrfrn  18049  pmtrprfval  18078  pmtrprfvalrn  18079  psgnunilem5  18085  odhash3  18162  gsumzaddlem  18492  gsumzsplit  18498  dprdcntz2  18608  0ringnnzr  19442  mplcoe1  19638  mplcoe5  19641  psrbagsn  19668  xrsdsreclblem  19965  dsmmbas2  20254  dsmmfi  20255  islindf4  20350  pmatcollpw3fi1lem1  20764  istps  20911  haust1  21329  hauspwdom  21477  kqcldsat  21709  csdfil  21870  tsmssplit  22127  dscopn  22550  htpycc  22951  pco1  22986  pcohtpylem  22990  pcopt  22993  pcopt2  22994  pcoass  22995  pcorevlem  22997  itg11  23628  bddmulibl  23775  lhop1  23947  deg1nn0clb  24020  plypf1  24138  vieta1lem2  24236  logdmn0  24556  logcnlem3  24560  fsumharmonic  24908  sqff1o  25078  perfectlem1  25124  bposlem5  25183  lgsval2lem  25202  ostth  25498  legso  25664  axlowdimlem13  26004  axlowdimlem16  26007  axlowdim1  26009  axlowdim  26011  upgrfi  26156  lfgrnloop  26190  umgredgnlp  26212  wlkp1lem3  26753  rusgrnumwwlkl1  27061  clwwlk  27077  clwwlkn0  27126  clwwlknon1sn  27219  trlsegvdeg  27350  konigsberg  27380  ex-res  27580  norm1exi  28387  dmadjrnb  29045  strlem1  29389  largei  29406  ifeqeqx  29639  ubico  29817  dya2iocuni  30625  eulerpartlemgh  30720  ballotlem4  30840  plymulx0  30904  signswch  30918  signstfvneq0  30929  signlem0  30944  subfacp1lem1  31439  bcneg1  31900  opelco3  31954  wsuclem  32047  sltval2  32086  sltintdifex  32091  sltres  32092  nolt02o  32122  dfrdg4  32335  linedegen  32527  rankeq1o  32555  hfninf  32570  ordcmp  32723  bj-projval  33261  bj-inftyexpidisj  33379  relowlpssretop  33494  finxpreclem2  33509  finxpreclem3  33512  finxpreclem5  33514  poimirlem18  33709  poimirlem19  33710  poimirlem20  33711  mblfinlem1  33728  nel02  34390  elpadd0  35567  diophin  37807  fiphp3d  37854  expdioph  38061  wepwsolem  38083  kelac1  38104  relintabex  38358  brnonrel  38366  relexp01min  38476  iooinlbub  40195  stoweidlem34  40723  fourierdlem60  40855  fourierdlem61  40856  fmtnoinf  41927  fmtno4prmfac193  41964  fmtno4prm  41966  31prm  41991  lighneallem3  42003  lighneallem4  42006  nnsum4primeseven  42167  nnsum4primesevenALTV  42168  spr0nelg  42205  sprsymrelfvlem  42219  dig2nn1st  42878
  Copyright terms: Public domain W3C validator