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

Theorem mtbii 315
Description: An inference from a biconditional, similar to modus tollens. (Contributed by NM, 27-Nov-1995.)
Hypotheses
Ref Expression
mtbii.min ¬ 𝜓
mtbii.maj (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
mtbii (𝜑 → ¬ 𝜒)

Proof of Theorem mtbii
StepHypRef Expression
1 mtbii.min . 2 ¬ 𝜓
2 mtbii.maj . . 3 (𝜑 → (𝜓𝜒))
32biimprd 237 . 2 (𝜑 → (𝜒𝜓))
41, 3mtoi 189 1 (𝜑 → ¬ 𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 195
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 196
This theorem is referenced by:  limom  6972  omopthlem2  7623  fineqv  8060  dfac2  8836  nd3  9290  axunndlem1  9296  axregndlem1  9303  axregndlem2  9304  axregnd  9305  axacndlem5  9312  canthp1lem2  9354  alephgch  9375  inatsk  9479  addnidpi  9602  indpi  9608  archnq  9681  fsumsplit  14318  sumsplit  14341  geoisum1c  14450  fprodm1  14536  m1dvdsndvds  15341  gexdvds  17822  chtub  24737  avril1  26711  ballotlemi1  29891  ballotlemii  29892  distel  30953  fvnobday  31081  onsucsuccmpi  31612  bj-inftyexpidisj  32274  poimirlem28  32607  poimirlem32  32611  nvelim  39849  1wlkp1lem6  40887  0nodd  41600  2nodd  41602
  Copyright terms: Public domain W3C validator