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

Theorem mtbird 302
Description: A deduction from a biconditional, similar to modus tollens. (Contributed by NM, 10-May-1994.)
Hypotheses
Ref Expression
mtbird.min  |-  ( ph  ->  -.  ch )
mtbird.maj  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
mtbird  |-  ( ph  ->  -.  ps )

Proof of Theorem mtbird
StepHypRef Expression
1 mtbird.min . 2  |-  ( ph  ->  -.  ch )
2 mtbird.maj . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
32biimpd 210 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41, 3mtod 180 1  |-  ( ph  ->  -.  ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187
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 188
This theorem is referenced by:  eqneltrd  2538  neleqtrrdOLD  2543  fvun1  5952  tz7.44-2  7133  oeeulem  7310  onomeneq  7768  supgtoreq  7992  inflb  8011  cantnfp1lem2  8183  cantnflem1  8193  rankxpsuc  8352  cardaleph  8518  cfsuc  8685  cflim2  8691  addnidpi  9325  genpnnp  9429  supaddc  10574  supmul1  10576  indstr2  11237  zbtwnre  11262  xrltnsym  11436  xrlttr  11439  xralrple  11498  supicclub2  11781  hashf1lem1  12613  swrdnd  12773  swrd0  12775  sqrtneglem  13309  rlimno1  13695  binomlem  13865  fprodn0f  14023  ruclem12  14271  dvdsle  14328  smu01lem  14433  rpexp  14643  oddprm  14728  pythagtriplem11  14738  pythagtriplem13  14740  pcpremul  14756  pczndvds  14777  pczndvds2  14779  pc2dvds  14791  pcadd  14797  pcmpt  14800  sgrp2nmndlem5  16614  pmtrdifellem4  17071  psgnunilem1  17085  psgnunilem2  17087  efgredlemc  17330  prmcyg  17463  ablfacrplem  17633  ablfac1eulem  17640  islbs2  18312  fidomndrng  18466  frlmssuvc2  19284  1stccnp  20408  fbasfip  20814  recld2  21743  metnrmlem1a  21786  xrhmeo  21870  bndth  21882  ioombl1lem4  22391  itg2seq  22577  itg2cnlem2  22597  dgrub  23056  dgrlb  23058  dgrnznn  23069  aaliou2  23161  taylthlem2  23194  dvlog2lem  23462  cxple2  23507  mumullem2  23970  chtub  24003  lgsval2lem  24097  lgsdir  24121  lgsne0  24124  lgsqr  24137  lgseisenlem1  24140  lgseisenlem2  24141  lgseisenlem4  24143  lgsquadlem1  24145  lgsquad2  24151  m1lgs  24153  2sqlem7  24161  2sqblem  24168  legso  24504  mirbtwnhl  24584  lmiopp  24700  axlowdimlem6  24823  usgra1v  24963  nbgranself  25007  cyclnspth  25204  eupath2lem3  25552  frgra2v  25572  frgrancvvdeqlem1  25603  2spotiundisj  25635  hmdmadj  27428  strlem1  27738  isoun  28122  archirng  28343  esumrnmpt2  28728  ballotlem4  29157  signswmnd  29234  signslema  29239  bnj1417  29638  tailfb  30818  topdifinffinlem  31484  icorempt2  31488  mblfinlem4  31684  3dimlem2  32733  3dimlem3a  32734  3dimlem3OLDN  32736  3dim2  32742  3dim3  32743  lplnnle2at  32815  lplnnlelln  32817  llncvrlpln  32832  lvolnle3at  32856  lvolnlelln  32858  lvolnlelpln  32859  4atlem3  32870  lplncvrlvol  32890  dalem30  32976  dalem35  32981  lhp2at0nle  33309  4atexlemswapqr  33337  ltrncnvel  33416  trlnle  33461  cdleme35sn3a  33735  cdleme46frvlpq  33780  cdlemeg46c  33789  cdlemeg46nlpq  33793  cdleme48gfv  33813  cdlemg7fvbwN  33883  cdlemg4d  33889  cdlemg10a  33916  cdlemg12d  33922  cdlemg27b  33972  cdlemg31d  33976  dihmeetlem6  34586  dochshpsat  34731  dochexmidlem1  34737  mapdindp  34948  lspindp5  35047  cmpfiiin  35248  fnwe2lem2  35615  relexpmulg  35941  relexp01min  35944  relexpxpmin  35948  cvgdvgrat  36299  nelsn  37042  flltnz  37125  gtnelioc  37172  ltnelicc  37179  gtnelicc  37182  limciccioolb  37273  limcrecl  37281  limcicciooub  37289  limclner  37304  reclimc  37306  sinaover2ne0  37315  icccncfext  37337  jumpncnp  37348  dvmptdiv  37361  itgsincmulx  37420  stoweidlem26  37455  stoweidlem35  37465  stirlinglem5  37509  dirker2re  37523  dirkerdenne0  37524  dirkertrigeqlem3  37531  dirkertrigeq  37532  dirkercncflem1  37534  dirkercncflem2  37535  dirkercncflem4  37537  fourierdlem10  37548  fourierdlem24  37562  fourierdlem25  37563  fourierdlem42  37580  fourierdlem44  37582  fourierdlem53  37591  fourierdlem58  37596  fourierdlem62  37600  fourierdlem76  37614  fourierdlem88  37626  fourierdlem104  37642  etransclem41  37707  etransclem44  37710  bits0eALTV  38199  oddprmALTV  38206  usgedgnlp  38480  0nodd  38568  2nodd  38570  lindslinindsimp1  39010
  Copyright terms: Public domain W3C validator