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

Theorem mpbir3an 1170
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 1166 . 2  |-  ( ps 
/\  ch  /\  th )
5 mpbir3an.4 . 2  |-  ( ph  <->  ( ps  /\  ch  /\  th ) )
64, 5mpbir 209 1  |-  ph
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ w3a 965
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967
This theorem is referenced by:  limon  6445  issmo  6807  xpider  7169  omina  8856  1eluzge0  10897  2eluzge0  10898  2eluzge1  10899  0elunit  11401  1elunit  11402  4fvwrd4  11531  fzo0to42pr  11614  cats1fv  12484  sincos1sgn  13475  sincos2sgn  13476  divalglem7  13601  igz  13993  strlemor1  14263  strleun  14266  strle1  14267  letsr  15395  psgnunilem2  15999  xrge0subm  17852  cnsubmlem  17859  cnsubglem  17860  cnsubrglem  17861  cnmsubglem  17873  nn0srg  17879  rge0srg  17880  ust0  19792  cnngp  20357  cnfldtgp  20443  htpycc  20550  pco0  20584  pcocn  20587  pcohtpylem  20589  pcopt  20592  pcopt2  20593  pcoass  20594  pcorevlem  20596  sinhalfpilem  21923  sincos4thpi  21973  sincos6thpi  21975  argregt0  22057  argrege0  22058  asin1  22287  atanbnd  22319  atan1  22321  harmonicbnd3  22399  ppiublem1  22539  usgraex0elv  23312  usgraex1elv  23313  usgraex2elv  23314  usgraex3elv  23315  usgrcyclnl1  23524  usgrcyclnl2  23525  4cycl4v4e  23550  4cycl4dv  23551  4cycl4dv4e  23552  ex-opab  23637  isgrpoi  23683  issubgoi  23795  isvci  23958  isnvi  23989  adj1o  25296  bra11  25510  xrge0omnd  26172  xrge0slmod  26310  unitssxrge0  26328  iistmd  26330  mhmhmeotmd  26355  xrge0tmdOLD  26373  rerrext  26436  cnrrext  26437  volmeas  26645  ddemeas  26650  fib1  26781  ballotth  26918  fdc  28638  riscer  28791  jm2.27dlem2  29356  arearect  29588  areaquad  29589  lhe4.4ex1a  29600  wallispilem4  29860  wwlktovf  30248  ccat2s1p2  30263  usgra2pthlem1  30297  elogb  31107  bj-pinftyccb  32541
  Copyright terms: Public domain W3C validator