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

Step	Hyp	Ref	Expression
1		mtbii.min	. 2
2		mtbii.maj	. . 3
3	2	biimprd 223	. 2
4	1, 3	mtoi 178	1

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