Theorem mpbir3an 1244

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

Step	Hyp	Ref	Expression
1		mpbir3an.1	. . 3 |- ps
2		mpbir3an.2	. . 3 |- ch
3		mpbir3an.3	. . 3 |- th
4	1, 2, 3	3pm3.2i 1239	. 2 |- ( ps /\ ch /\ th )
5		mpbir3an.4	. 2 |- ( ph <-> ( ps /\ ch /\ th ) )
6	4, 5	mpbir 221	1 |- ph

Syntax hints:   <-> wb 196   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  limon  7036  issmo  7445  xpider  7818  omina  9513  1eluzge0  11732  2eluzge1  11734  0elunit  12290  1elunit  12291  fz0to3un2pr  12441  4fvwrd4  12459  fzo0to42pr  12555  ccat2s1p2  13406  cats1fv  13604  wwlktovf  13699  sincos1sgn  14923  sincos2sgn  14924  divalglem7  15122  igz  15638  strlemor1OLD  15969  strleun  15972  strle1  15973  letsr  17227  psgnunilem2  17915  cnfldfunALT  19759  xrge0subm  19787  cnsubmlem  19794  cnsubglem  19795  cnsubrglem  19796  cnmsubglem  19809  nn0srg  19816  rge0srg  19817  ust0  22023  cnngp  22583  cnfldtgp  22672  htpycc  22779  pco0  22814  pcocn  22817  pcohtpylem  22819  pcopt  22822  pcopt2  22823  pcoass  22824  pcorevlem  22826  sinhalfpilem  24215  sincos4thpi  24265  sincos6thpi  24267  argregt0  24356  argrege0  24357  elogb  24508  asin1  24621  atanbnd  24653  atan1  24655  harmonicbnd3  24734  ppiublem1  24927  usgrexmplef  26151  usgr2pthlem  26659  uspgrn2crct  26700  upgr3v3e3cycl  27040  upgr4cycl4dv4e  27045  konigsbergiedgw  27108  konigsbergiedgwOLD  27109  konigsberglem1  27114  konigsberglem2  27115  konigsberglem3  27116  konigsberglem4  27117  ex-opab  27289  isgrpoi  27352  isvciOLD  27435  isnvi  27468  adj1o  28753  bra11  28967  xrge0omnd  29711  reofld  29840  xrge0slmod  29844  unitssxrge0  29946  iistmd  29948  mhmhmeotmd  29973  xrge0tmdOLD  29991  rerrext  30053  cnrrext  30054  volmeas  30294  ddemeas  30299  fib1  30462  ballotlem2  30550  ballotth  30599  prodfzo03  30681  logi  31620  bj-pinftyccb  33108  fdc  33541  riscer  33787  jm2.27dlem2  37577  arearect  37801  areaquad  37802  lhe4.4ex1a  38528  wallispilem4  40285  fourierdlem20  40344  fourierdlem62  40385  fourierdlem104  40427  fourierdlem111  40434  sqwvfoura  40445  sqwvfourb  40446  fouriersw  40448  pfx2  41412  fmtnoprmfac2lem1  41478  fmtno4prmfac  41484  31prm  41512  sbgoldbo  41675  nnsum4primeseven  41688  nnsum4primesevenALTV  41689  wtgoldbnnsum4prm  41690  bgoldbnnsum3prm  41692  tgblthelfgott  41703  tgblthelfgottOLD  41709  2zlidl  41934  2zrngALT  41948  nnpw2blen  42374