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

Theorem mtbii 302
 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 223 . 2
41, 3mtoi 178 1
 Colors of variables: wff setvar class Syntax hints:  -.wn 3  ->wi 4  <->wb 184 This theorem is referenced by:  limom  6715  omopthlem2  7324  fineqv  7755  dfac2  8532  nd3  8985  axunndlem1  8991  axregndlem1  9000  axregndlem2  9001  axregnd  9002  axregndOLD  9003  axacndlem5  9010  canthp1lem2  9052  alephgch  9073  inatsk  9177  addnidpi  9300  indpi  9306  archnq  9379  fsumsplit  13562  sumsplit  13583  geoisum1c  13689  fprodm1  13771  m1dvdsndvds  14325  gexdvds  16604  chtub  23487  avril1  25171  vcoprne  25472  ballotlemi1  28441  ballotlemii  28442  distel  29236  fvnobday  29442  onsucsuccmpi  29908  nvelim  32205  0nodd  32498  2nodd  32500  bj-inftyexpidisj  34613 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 185
 Copyright terms: Public domain W3C validator