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

Theorem mpbir3an 1134
Description: Detach a conjunction of truths in a biconditional. (Contributed by NM, 16-Sep-2011.)
Hypotheses
Ref Expression
mpbir3an.1  |-  ps
mpbir3an.2  |-  ch
mpbir3an.3  |-  th
mpbir3an.4  |-  ( ph  <->  ( ps  /\  ch  /\  th ) )
Assertion
Ref Expression
mpbir3an  |-  ph

Proof of Theorem mpbir3an
StepHypRef Expression
1 mpbir3an.1 . . 3  |-  ps
2 mpbir3an.2 . . 3  |-  ch
3 mpbir3an.3 . . 3  |-  th
41, 2, 33pm3.2i 1130 . 2  |-  ( ps 
/\  ch  /\  th )
5 mpbir3an.4 . 2  |-  ( ph  <->  ( ps  /\  ch  /\  th ) )
64, 5mpbir 200 1  |-  ph
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ w3a 934
This theorem is referenced by:  limon  4643  issmo  6381  xpider  6746  omina  8329  0elunit  10770  1elunit  10771  cats1fv  11525  sincos1sgn  12489  sincos2sgn  12490  divalglem7  12614  igz  12997  strlemor1  13251  strleun  13254  strle1  13255  letsr  14365  xrge0subm  16428  cnsubmlem  16435  cnsubglem  16436  cnsubrglem  16437  cnmsubglem  16450  cnngp  18305  cnfldtgp  18389  htpycc  18494  pco0  18528  pcocn  18531  pcohtpylem  18533  pcopt  18536  pcopt2  18537  pcoass  18538  pcorevlem  18540  sinhalfpilem  19850  sincos4thpi  19897  sincos6thpi  19899  argregt0  19980  argrege0  19981  asin1  20206  atanbnd  20238  atan1  20240  harmonicbnd3  20317  ppiublem1  20457  ex-opab  20835  isgrpoi  20881  issubgoi  20993  isvci  21154  isnvi  21185  adj1o  22490  bra11  22704  ballotth  23112  unitssxrge0  23299  iistmd  23301  mhmhmeotmd  23315  xrge0tmdALT  23342  empos  25345  fdc  26558  riscer  26722  jm2.27dlem2  27206  psgnunilem2  27521  lhe4.4ex1a  27649  fzo0to42pr  28211  4fvwrd4  28220  usgrcyclnl1  28386  usgrcyclnl2  28387  4cycl4v4e  28412  4cycl4dv  28413  4cycl4dv4e  28414  elogb  28513  isatliN  30114
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator