Theorem mpbir3an 1178

Description: Detach a conjunction of truths in a biconditional. (Contributed by NM, 16-Sep-2011.)

Hypotheses

Ref	Expression
mpbir3an.1
mpbir3an.2
mpbir3an.3
mpbir3an.4

Assertion

Ref	Expression
mpbir3an

Proof of Theorem mpbir3an

Step	Hyp	Ref	Expression
1		mpbir3an.1	. . 3
2		mpbir3an.2	. . 3
3		mpbir3an.3	. . 3
4	1, 2, 3	3pm3.2i 1174	. 2
5		mpbir3an.4	. 2
6	4, 5	mpbir 209	1

Syntax hints:  <->wb 184  /\w3a 973

This theorem is referenced by:  limon  6671  issmo  7038  xpider  7401  omina  9090  1eluzge0  11153  2eluzge0OLD  11155  2eluzge1  11156  0elunit  11667  1elunit  11668  4fvwrd4  11822  fzo0to42pr  11901  ccat2s1p2  12633  cats1fv  12824  wwlktovf  12894  sincos1sgn  13928  sincos2sgn  13929  divalglem7  14057  igz  14452  strlemor1  14724  strleun  14727  strle1  14728  letsr  15857  psgnunilem2  16520  xrge0subm  18459  cnsubmlem  18466  cnsubglem  18467  cnsubrglem  18468  cnmsubglem  18480  nn0srg  18486  rge0srg  18487  ust0  20722  cnngp  21287  cnfldtgp  21373  htpycc  21480  pco0  21514  pcocn  21517  pcohtpylem  21519  pcopt  21522  pcopt2  21523  pcoass  21524  pcorevlem  21526  sinhalfpilem  22856  sincos4thpi  22906  sincos6thpi  22908  argregt0  22995  argrege0  22996  asin1  23225  atanbnd  23257  atan1  23259  harmonicbnd3  23337  ppiublem1  23477  usgraex0elv  24396  usgraex1elv  24397  usgraex2elv  24398  usgraex3elv  24399  usgrcyclnl1  24640  usgrcyclnl2  24641  4cycl4v4e  24666  4cycl4dv  24667  4cycl4dv4e  24668  ex-opab  25153  isgrpoi  25200  issubgoi  25312  isvci  25475  isnvi  25506  adj1o  26813  bra11  27027  xrge0omnd  27701  reofld  27830  xrge0slmod  27834  unitssxrge0  27882  iistmd  27884  mhmhmeotmd  27909  xrge0tmdOLD  27927  rerrext  27990  cnrrext  27991  volmeas  28203  ddemeas  28208  fib1  28339  ballotlem2  28427  ballotth  28476  logi  29121  fdc  30238  riscer  30391  jm2.27dlem2  30952  arearect  31183  areaquad  31184  lhe4.4ex1a  31234  wallispilem4  31850  fourierdlem20  31909  fourierdlem62  31951  fourierdlem104  31993  fourierdlem111  32000  sqwvfoura  32011  sqwvfourb  32012  fouriersw  32014  usgra2pthlem1  32353  2zlidl  32740  2zrngALT  32754  elogb  33169  bj-pinftyccb  34624

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 975