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  4757  issmo  6547  xpider  6912  omina  8500  0elunit  10948  1elunit  10949  4fvwrd4  11052  fzo0to42pr  11114  cats1fv  11751  sincos1sgn  12722  sincos2sgn  12723  divalglem7  12847  igz  13230  strlemor1  13484  strleun  13487  strle1  13488  letsr  14600  xrge0subm  16663  cnsubmlem  16670  cnsubglem  16671  cnsubrglem  16672  cnmsubglem  16685  ust0  18171  cnngp  18686  cnfldtgp  18771  htpycc  18877  pco0  18911  pcocn  18914  pcohtpylem  18916  pcopt  18919  pcopt2  18920  pcoass  18921  pcorevlem  18923  sinhalfpilem  20242  sincos4thpi  20289  sincos6thpi  20291  argregt0  20373  argrege0  20374  asin1  20602  atanbnd  20634  atan1  20636  harmonicbnd3  20714  ppiublem1  20854  usgraex0elv  21282  usgraex1elv  21283  usgraex2elv  21284  usgraex3elv  21285  usgrcyclnl1  21476  usgrcyclnl2  21477  4cycl4v4e  21502  4cycl4dv  21503  4cycl4dv4e  21504  ex-opab  21589  isgrpoi  21635  issubgoi  21747  isvci  21910  isnvi  21941  adj1o  23246  bra11  23460  reofld  24097  unitssxrge0  24103  iistmd  24105  mhmhmeotmd  24118  xrge0tmdOLD  24136  volmeas  24382  ballotth  24575  fdc  26141  riscer  26296  jm2.27dlem2  26773  psgnunilem2  27088  lhe4.4ex1a  27216  wallispilem4  27486  elogb  27879  isatliN  29418
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