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

Theorem mpbir3an 1136
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 1132 . 2  |-  ( ps 
/\  ch  /\  th )
5 mpbir3an.4 . 2  |-  ( ph  <->  ( ps  /\  ch  /\  th ) )
64, 5mpbir 201 1  |-  ph
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ w3a 936
This theorem is referenced by:  limon  4775  issmo  6569  xpider  6934  omina  8522  0elunit  10971  1elunit  10972  4fvwrd4  11076  fzo0to42pr  11141  cats1fv  11778  sincos1sgn  12749  sincos2sgn  12750  divalglem7  12874  igz  13257  strlemor1  13511  strleun  13514  strle1  13515  letsr  14627  xrge0subm  16694  cnsubmlem  16701  cnsubglem  16702  cnsubrglem  16703  cnmsubglem  16716  ust0  18202  cnngp  18767  cnfldtgp  18852  htpycc  18958  pco0  18992  pcocn  18995  pcohtpylem  18997  pcopt  19000  pcopt2  19001  pcoass  19002  pcorevlem  19004  sinhalfpilem  20327  sincos4thpi  20374  sincos6thpi  20376  argregt0  20458  argrege0  20459  asin1  20687  atanbnd  20719  atan1  20721  harmonicbnd3  20799  ppiublem1  20939  usgraex0elv  21368  usgraex1elv  21369  usgraex2elv  21370  usgraex3elv  21371  usgrcyclnl1  21580  usgrcyclnl2  21581  4cycl4v4e  21606  4cycl4dv  21607  4cycl4dv4e  21608  ex-opab  21693  isgrpoi  21739  issubgoi  21851  isvci  22014  isnvi  22045  adj1o  23350  bra11  23564  reofld  24233  unitssxrge0  24251  iistmd  24253  mhmhmeotmd  24266  xrge0tmdOLD  24284  volmeas  24540  ballotth  24748  fdc  26339  riscer  26494  jm2.27dlem2  26971  psgnunilem2  27286  lhe4.4ex1a  27414  wallispilem4  27684  usgra2pthlem1  28040  elogb  28246  isatliN  29785
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  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator