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

Theorem mtbird 301
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 207 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41, 3mtod 177 1  |-  ( ph  ->  -.  ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184
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
This theorem is referenced by:  eqneltrd  2571  neleqtrrdOLD  2576  fvun1  5931  tz7.44-2  7065  oeeulem  7242  onomeneq  7699  supgtoreq  7919  cantnfp1lem2  8089  cantnflem1  8099  cantnfp1lem2OLD  8115  cantnflem1OLD  8122  rankxpsuc  8291  cardaleph  8461  cfsuc  8628  cflim2  8634  addnidpi  9270  genpnnp  9374  supmul1  10499  indstr2  11151  zbtwnre  11171  xrltnsym  11334  xrlttr  11337  xralrple  11395  hashf1lem1  12459  swrd0  12610  sqrneglem  13052  rlimno1  13427  binomlem  13595  ruclem12  13826  dvdsle  13881  smu01lem  13985  rpexp  14111  oddprm  14189  pythagtriplem11  14199  pythagtriplem13  14201  pcpremul  14217  pczndvds  14238  pczndvds2  14240  pc2dvds  14252  pcadd  14258  pcmpt  14261  pmtrdifellem4  16295  psgnunilem1  16309  psgnunilem2  16311  efgredlemc  16554  prmcyg  16682  ablfacrplem  16901  ablfac1eulem  16908  islbs2  17578  fidomndrng  17722  frlmssuvc2  18588  frlmssuvc2OLD  18590  1stccnp  19724  fbasfip  20099  recld2  21049  metnrmlem1a  21092  xrhmeo  21176  bndth  21188  ioombl1lem4  21701  itg2seq  21879  itg2cnlem2  21899  dgrub  22361  dgrlb  22363  aaliou2  22465  taylthlem2  22498  dvlog2lem  22756  cxple2  22801  mumullem2  23177  chtub  23210  lgsval2lem  23304  lgsdir  23328  lgsne0  23331  lgsqr  23344  lgseisenlem1  23347  lgseisenlem2  23348  lgseisenlem4  23350  lgsquadlem1  23352  lgsquad2  23358  m1lgs  23360  2sqlem7  23368  2sqblem  23375  legso  23707  axlowdimlem6  23921  usgra1v  24054  nbgranself  24098  cyclnspth  24295  eupath2lem3  24643  frgra2v  24663  frgrancvvdeqlem1  24695  2spotiundisj  24727  hmdmadj  26523  strlem1  26833  isoun  27180  archirng  27382  archiabllem2b  27390  ballotlem4  28065  signslema  28147  supaddc  29606  mblfinlem4  29620  tailfb  29787  cmpfiiin  30222  fnwe2lem2  30592  dgrnznn  30680  flltnz  31032  gtnelioc  31044  ltnelicc  31051  gtnelicc  31054  limciccioolb  31120  limcrecl  31128  limcicciooub  31136  limclner  31150  reclimc  31152  sinaover2ne0  31161  icccncfext  31183  cncfiooicclem1  31189  jumpncnp  31194  dvmptdiv  31204  itgsincmulx  31249  stoweidlem26  31283  stoweidlem35  31292  stirlinglem5  31335  dirker2re  31349  dirkerdenne0  31350  dirkerval2  31351  dirkertrigeqlem3  31357  dirkertrigeq  31358  dirkercncflem1  31360  dirkercncflem2  31361  dirkercncflem4  31363  fourierdlem10  31374  fourierdlem24  31388  fourierdlem25  31389  fourierdlem42  31406  fourierdlem44  31408  fourierdlem53  31417  fourierdlem58  31422  fourierdlem60  31424  fourierdlem61  31425  fourierdlem62  31426  fourierdlem76  31440  fourierdlem88  31452  fourierdlem104  31468  usgedgnlp  31814  lindslinindsimp1  32008  bnj1417  33053  3dimlem2  34132  3dimlem3a  34133  3dimlem3OLDN  34135  3dim2  34141  3dim3  34142  lplnnle2at  34214  lplnnlelln  34216  llncvrlpln  34231  lvolnle3at  34255  lvolnlelln  34257  lvolnlelpln  34258  4atlem3  34269  lplncvrlvol  34289  dalem30  34375  dalem35  34380  lhp2at0nle  34708  4atexlemswapqr  34736  ltrncnvel  34815  trlnle  34859  cdleme35sn3a  35132  cdleme46frvlpq  35177  cdlemeg46c  35186  cdlemeg46nlpq  35190  cdleme48gfv  35210  cdlemg7fvbwN  35280  cdlemg4d  35286  cdlemg10a  35313  cdlemg12d  35319  cdlemg27b  35369  cdlemg31d  35373  dihmeetlem6  35983  dochshpsat  36128  dochexmidlem1  36134  mapdindp  36345  lspindp5  36444
  Copyright terms: Public domain W3C validator