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

Theorem mtbird 293
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 199 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41, 3mtod 170 1  |-  ( ph  ->  -.  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177
This theorem is referenced by:  eqneltrd  2482  neleqtrrd  2485  fvun1  5735  tz7.44-2  6603  oeeulem  6782  onomeneq  7234  cantnfp1lem2  7570  cantnflem1  7580  rankxpsuc  7741  cardaleph  7905  cfsuc  8072  cflim2  8078  addnidpi  8713  genpnnp  8817  supmul1  9907  indstr2  10488  zbtwnre  10506  xrltnsym  10664  xrlttr  10667  xralrple  10725  hashf1lem1  11633  sqrneglem  12001  rlimno1  12376  binomlem  12537  ruclem12  12769  dvdsle  12824  smu01lem  12926  rpexp  13049  oddprm  13118  pythagtriplem11  13128  pythagtriplem13  13130  pcpremul  13146  pczndvds  13167  pczndvds2  13169  pc2dvds  13181  pcadd  13187  pcmpt  13190  efgredlemc  15306  prmcyg  15432  ablfacrplem  15552  ablfac1eulem  15559  islbs2  16155  fidomndrng  16296  1stccnp  17448  fbasfip  17823  recld2  18718  metnrmlem1a  18761  xrhmeo  18844  bndth  18856  ioombl1lem4  19324  itg2seq  19503  itg2cnlem2  19523  dgrub  20022  dgrlb  20024  aaliou2  20126  taylthlem2  20159  dvlog2lem  20412  cxple2  20457  mumullem2  20832  chtub  20865  lgsval2lem  20959  lgsdir  20983  lgsne0  20986  lgsqr  20999  lgseisenlem1  21002  lgseisenlem2  21003  lgseisenlem4  21005  lgsquadlem1  21007  lgsquad2  21013  m1lgs  21015  2sqlem7  21023  2sqblem  21030  usgra1v  21277  nbgranself  21314  cyclnspth  21468  eupath2lem3  21551  hmdmadj  23293  strlem1  23603  isoun  23932  ballotlem4  24537  axlowdimlem6  25602  supaddc  25949  tailfb  26099  cmpfiiin  26444  fnwe2lem2  26819  frlmssuvc2  26918  dgrnznn  27011  psgnunilem1  27087  psgnunilem2  27089  stoweidlem26  27445  stoweidlem35  27454  stirlinglem5  27497  frgra2v  27754  frgrancvvdeqlem1  27784  bnj1417  28750  3dimlem2  29575  3dimlem3a  29576  3dimlem3OLDN  29578  3dim2  29584  3dim3  29585  lplnnle2at  29657  lplnnlelln  29659  llncvrlpln  29674  lvolnle3at  29698  lvolnlelln  29700  lvolnlelpln  29701  4atlem3  29712  lplncvrlvol  29732  dalem30  29818  dalem35  29823  lhp2at0nle  30151  4atexlemswapqr  30179  ltrncnvel  30258  trlnle  30302  cdleme35sn3a  30575  cdleme46frvlpq  30620  cdlemeg46c  30629  cdlemeg46nlpq  30633  cdleme48gfv  30653  cdlemg7fvbwN  30723  cdlemg4d  30729  cdlemg10a  30756  cdlemg12d  30762  cdlemg27b  30812  cdlemg31d  30816  dihmeetlem6  31426  dochshpsat  31571  dochexmidlem1  31577  mapdindp  31788  lspindp5  31887
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator