MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpbir3an Structured version   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  4808  issmo  6602  xpider  6967  omina  8558  0elunit  11007  1elunit  11008  4fvwrd4  11113  fzo0to42pr  11178  cats1fv  11815  sincos1sgn  12786  sincos2sgn  12787  divalglem7  12911  igz  13294  strlemor1  13548  strleun  13551  strle1  13552  letsr  14664  xrge0subm  16731  cnsubmlem  16738  cnsubglem  16739  cnsubrglem  16740  cnmsubglem  16753  ust0  18241  cnngp  18806  cnfldtgp  18891  htpycc  18997  pco0  19031  pcocn  19034  pcohtpylem  19036  pcopt  19039  pcopt2  19040  pcoass  19041  pcorevlem  19043  sinhalfpilem  20366  sincos4thpi  20413  sincos6thpi  20415  argregt0  20497  argrege0  20498  asin1  20726  atanbnd  20758  atan1  20760  harmonicbnd3  20838  ppiublem1  20978  usgraex0elv  21407  usgraex1elv  21408  usgraex2elv  21409  usgraex3elv  21410  usgrcyclnl1  21619  usgrcyclnl2  21620  4cycl4v4e  21645  4cycl4dv  21646  4cycl4dv4e  21647  ex-opab  21732  isgrpoi  21778  issubgoi  21890  isvci  22053  isnvi  22084  adj1o  23389  bra11  23603  reofld  24272  unitssxrge0  24290  iistmd  24292  mhmhmeotmd  24305  xrge0tmdOLD  24323  volmeas  24579  ballotth  24787  fdc  26440  riscer  26595  jm2.27dlem2  27072  psgnunilem2  27386  lhe4.4ex1a  27514  wallispilem4  27784  1eluzge0  28085  2eluzge0  28086  2eluzge1  28087  usgra2pthlem1  28263  elogb  28469  isatliN  30037
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