Theorem mtbid 300

Description: A deduction from a biconditional, similar to modus tollens. (Contributed by NM, 26-Nov-1995.)

Hypotheses

Ref	Expression
mtbid.min
mtbid.maj

Assertion

Ref	Expression
mtbid

Proof of Theorem mtbid

Step	Hyp	Ref	Expression
1		mtbid.min	. 2
2		mtbid.maj	. . 3
3	2	biimprd 223	. 2
4	1, 3	mtod 177	1

Syntax hints:  -.wn 3  ->wi 4  <->wb 184

This theorem is referenced by:  sylnib  304  eqneltrrdOLD  2568  neleqtrd  2569  eueq3  3274  efrirr  4865  efrn2lp  4866  epne3  6616  ordtypelem9  7972  cantnfp1lem3  8120  cantnflem1b  8126  cantnflem1  8129  cantnfp1lem3OLD  8146  cantnflem1bOLD  8149  cantnflem1OLD  8152  cnfcom3lem  8168  cnfcom3lemOLD  8176  cflim2  8664  fin23lem30  8743  isf32lem5  8758  axdc3lem4  8854  axpownd  8999  pwfseqlem3  9059  grur1  9219  genpnnp  9404  xrlttri  11374  infmxrlb  11554  expneg  12174  bcval5  12396  seqcoll  12512  seqcoll2  12513  hashge2el2dif  12521  lswccatn0lsw  12607  fsumss  13547  fprodss  13755  rpdvds  14265  pcmpt  14411  prmreclem2  14435  prmreclem5  14438  prmlem0  14591  sylow1lem3  16620  sylow2blem3  16642  efgredlema  16758  gsum2d2lem  17001  lindsind2  18854  1stccnp  19963  kqdisj  20233  alexsubALTlem4  20550  xrhmeo  21446  minveclem3b  21843  ovolgelb  21891  volsup  21966  volsup2  22014  itg1val2  22091  itg2seq  22149  itg2cn  22170  limcnlp  22282  itgsubstlem  22449  ply1termlem  22600  radcnvlt1  22813  fsumharmonic  23341  ftalem3  23348  chpub  23495  lgsqr  23621  lgseisenlem1  23624  lgsquadlem3  23631  2sqlem8a  23646  2sqlem8  23647  2sqblem  23652  tgdim01  23898  lnoppnhpg  24133  axcontlem2  24268  usgraedgrnv  24377  minvecolem5  25797  divnumden2  27609  oddpwdc  28293  eulerpartlemsv2  28297  eulerpartlemv  28303  eulerpartlemgh  28317  signslema  28519  erdszelem7  28641  erdszelem8  28642  wfrlem10  29352  wsuclem  29381  wsuclb  29384  ftc1anclem5  30094  cntotbnd  30292  irrapxlem1  30758  elpell14qr2  30798  elpell1qr2  30808  wepwsolem  30987  fnwe2lem2  30997  oddfl  31459  dstregt0  31463  xrlttri5d  31465  divlt0gt0d  31469  iccdifprioo  31556  stoweidlem34  31816  stirlinglem5  31860  dirker2re  31874  dirkerdenne0  31875  dirkertrigeq  31883  dirkercncflem2  31886  dirkercncflem4  31888  fourierdlem54  31943  elaa2lem  32016  etransclem9  32026  0nodd  32498  2nodd  32500  1neven  32738  lshpdisj  34712  lcv1  34766  atlatmstc  35044  hlatcon2  35176  4noncolr3  35177  3atlem6  35212  lplnnleat  35266  lplnexllnN  35288  lvolnleat  35307  4atlem11  35333  dalem1  35383  dalemswapyzps  35414  dalemrotps  35415  2llnma1  35511  dalawlem15  35609  4atexlemcnd  35796  ltrnel  35863  cdleme15c  36001  cdleme0nex  36015  cdleme20yOLD  36028  cdleme20m  36049  cdleme43bN  36216  cdleme43dN  36218  cdlemeg46nlpq  36243  cdlemg12  36376  dihmeetcN  37029  dihjatc1  37038  dihjatcclem1  37145  lclkrlem2a  37234  lcfrlem20  37289  mapdh6aN  37462  mapdh8ab  37504  hdmap1l6a  37537

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