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

Theorem mpbir3an 1173
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 1169 . 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 968
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 970
This theorem is referenced by:  limon  6642  issmo  7009  xpider  7372  omina  9058  1eluzge0  11114  2eluzge0  11115  2eluzge1  11116  0elunit  11627  1elunit  11628  4fvwrd4  11779  fzo0to42pr  11858  ccat2s1p2  12583  cats1fv  12774  wwlktovf  12844  sincos1sgn  13778  sincos2sgn  13779  divalglem7  13905  igz  14300  strlemor1  14571  strleun  14574  strle1  14575  letsr  15703  psgnunilem2  16309  xrge0subm  18220  cnsubmlem  18227  cnsubglem  18228  cnsubrglem  18229  cnmsubglem  18241  nn0srg  18247  rge0srg  18248  ust0  20450  cnngp  21015  cnfldtgp  21101  htpycc  21208  pco0  21242  pcocn  21245  pcohtpylem  21247  pcopt  21250  pcopt2  21251  pcoass  21252  pcorevlem  21254  sinhalfpilem  22582  sincos4thpi  22632  sincos6thpi  22634  argregt0  22716  argrege0  22717  asin1  22946  atanbnd  22978  atan1  22980  harmonicbnd3  23058  ppiublem1  23198  usgraex0elv  24058  usgraex1elv  24059  usgraex2elv  24060  usgraex3elv  24061  usgrcyclnl1  24302  usgrcyclnl2  24303  4cycl4v4e  24328  4cycl4dv  24329  4cycl4dv4e  24330  ex-opab  24816  isgrpoi  24862  issubgoi  24974  isvci  25137  isnvi  25168  adj1o  26475  bra11  26689  xrge0omnd  27349  xrge0slmod  27483  unitssxrge0  27504  iistmd  27506  mhmhmeotmd  27531  xrge0tmdOLD  27549  rerrext  27612  cnrrext  27613  volmeas  27829  ddemeas  27834  fib1  27965  ballotth  28102  fdc  29828  riscer  29981  jm2.27dlem2  30545  arearect  30777  areaquad  30778  lhe4.4ex1a  30789  wallispilem4  31323  fourierdlem20  31382  fourierdlem62  31424  fourierdlem104  31466  fourierdlem111  31473  fouriersw  31487  usgra2pthlem1  31777  elogb  32125  bj-pinftyccb  33571
  Copyright terms: Public domain W3C validator