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

Theorem mpbir3an 1191
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 1187 . 2  |-  ( ps 
/\  ch  /\  th )
5 mpbir3an.4 . 2  |-  ( ph  <->  ( ps  /\  ch  /\  th ) )
64, 5mpbir 214 1  |-  ph
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189    /\ w3a 986
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 190  df-an 377  df-3an 988
This theorem is referenced by:  limon  6651  issmo  7054  xpider  7421  omina  9103  1eluzge0  11192  2eluzge0OLD  11194  2eluzge1  11195  0elunit  11741  1elunit  11742  fz0to3un2pr  11885  4fvwrd4  11902  fzo0to42pr  11993  ccat2s1p2  12761  cats1fv  12954  wwlktovf  13042  sincos1sgn  14258  sincos2sgn  14259  divalglem7  14390  igz  14889  strlemor1  15228  strleun  15231  strle1  15232  letsr  16484  psgnunilem2  17147  xrge0subm  19020  cnsubmlem  19027  cnsubglem  19028  cnsubrglem  19029  cnmsubglem  19041  nn0srg  19048  rge0srg  19049  ust0  21245  cnngp  21811  cnfldtgp  21912  htpycc  22022  pco0  22056  pcocn  22059  pcohtpylem  22061  pcopt  22064  pcopt2  22065  pcoass  22066  pcorevlem  22068  sinhalfpilem  23430  sincos4thpi  23480  sincos6thpi  23482  argregt0  23571  argrege0  23572  elogb  23719  asin1  23832  atanbnd  23864  atan1  23866  harmonicbnd3  23945  ppiublem1  24142  usgraex0elv  25135  usgraex1elv  25136  usgraex2elv  25137  usgraex3elv  25138  usgrcyclnl1  25380  usgrcyclnl2  25381  4cycl4v4e  25406  4cycl4dv  25407  4cycl4dv4e  25408  ex-opab  25894  isgrpoi  25938  issubgoi  26050  isvci  26213  isnvi  26244  adj1o  27559  bra11  27773  xrge0omnd  28481  reofld  28610  xrge0slmod  28614  unitssxrge0  28713  iistmd  28715  mhmhmeotmd  28740  xrge0tmdOLD  28758  rerrext  28820  cnrrext  28821  volmeas  29060  ddemeas  29065  fib1  29239  ballotlem2  29327  ballotth  29376  ballotthOLD  29414  logi  30376  bj-pinftyccb  31665  fdc  32076  riscer  32229  jm2.27dlem2  35867  arearect  36102  areaquad  36103  lhe4.4ex1a  36679  wallispilem4  37987  fourierdlem20  38046  fourierdlem62  38089  fourierdlem104  38131  fourierdlem111  38138  sqwvfoura  38149  sqwvfourb  38150  fouriersw  38152  nnsum4primeseven  38986  nnsum4primesevenALTV  38987  wtgoldbnnsum4prm  38988  bgoldbnnsum3prm  38990  tgblthelfgott  38999  pfx2  39046  uspgrn2crct  39878  upgr3v3e3cycl  39973  upgr4cycl4dv4e  39978  usgra2pthlem1  39992  2zlidl  40259  2zrngALT  40273  nnpw2blen  40716
  Copyright terms: Public domain W3C validator