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  4627  issmo  6365  xpider  6730  omina  8313  0elunit  10754  1elunit  10755  cats1fv  11509  sincos1sgn  12473  sincos2sgn  12474  divalglem7  12598  igz  12981  strlemor1  13235  strleun  13238  strle1  13239  letsr  14349  xrge0subm  16412  cnsubmlem  16419  cnsubglem  16420  cnsubrglem  16421  cnmsubglem  16434  cnngp  18289  cnfldtgp  18373  htpycc  18478  pco0  18512  pcocn  18515  pcohtpylem  18517  pcopt  18520  pcopt2  18521  pcoass  18522  pcorevlem  18524  sinhalfpilem  19834  sincos4thpi  19881  sincos6thpi  19883  argregt0  19964  argrege0  19965  asin1  20190  atanbnd  20222  atan1  20224  harmonicbnd3  20301  ppiublem1  20441  ex-opab  20819  isgrpoi  20865  issubgoi  20977  isvci  21138  isnvi  21169  adj1o  22474  bra11  22688  ballotth  23096  unitssxrge0  23284  iistmd  23286  mhmhmeotmd  23300  xrge0tmdALT  23327  empos  25242  fdc  26455  riscer  26619  jm2.27dlem2  27103  psgnunilem2  27418  lhe4.4ex1a  27546  isatliN  29492
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