Theorem mpbir3an 1343

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 1341	. 2 ⊢ (𝜓 ∧ 𝜒 ∧ 𝜃)
5		mpbir3an.4	. 2 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))
6	4, 5	mpbir 231	1 ⊢ 𝜑

Syntax hints:   ↔ wb 206   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  snopeqopsnid  5455  f1oi  6810  limon  7778  issmo  8279  xpider  8726  omina  10603  1eluzge0  12819  2eluzge1  12821  5eluz3  12822  0elunit  13411  1elunit  13412  fz0to3un2pr  13572  fz0to4untppr  13573  fz0to5un2tp  13574  4fvwrd4  13591  fzo0to42pr  13697  fvf1tp  13737  tpf1ofv1  14448  tpf1ofv2  14449  tpfo  14451  ccat2s1p2  14582  cats1fv  14810  pfx2  14898  wwlktovf  14907  fprodge0  15947  fprodge1  15949  sincos1sgn  16149  sincos2sgn  16150  divalglem7  16357  igz  16894  strleun  17116  strle1  17117  letsr  18548  psgnunilem2  19459  cnfldfun  21356  cnfldfunOLD  21369  cnsubmlem  21402  cnsubglem  21403  cnsubrglem  21404  cnsubrglemOLD  21405  cnmsubglem  21418  nn0srg  21425  rge0srg  21426  xrge0subm  21431  xrge0omnd  21433  pzriprnglem4  21472  ust0  24194  cnngp  24753  cnfldtgp  24845  htpycc  24956  pco0  24990  pcocn  24993  pcohtpylem  24995  pcopt  24998  pcopt2  24999  pcoass  25000  pcorevlem  25002  sinhalfpilem  26443  sincos4thpi  26493  sincos6thpi  26496  logi  26567  argregt0  26590  argrege0  26591  elogb  26751  2logb9irr  26776  2logb9irrALT  26779  sqrt2cxp2logb9e3  26780  asin1  26875  atanbnd  26907  atan1  26909  harmonicbnd3  26989  ppiublem1  27184  zsoring  28420  usgrexmplef  29347  usgr2pthlem  29851  uspgrn2crct  29896  upgr3v3e3cycl  30270  upgr4cycl4dv4e  30275  konigsbergiedgw  30338  konigsberglem1  30342  konigsberglem2  30343  konigsberglem3  30344  konigsberglem4  30345  ex-opab  30522  isgrpoi  30589  isvciOLD  30671  isnvi  30704  adj1o  31985  bra11  32199  1fldgenq  33403  reofld  33423  xrge0slmod  33428  ccfldsrarelvec  33836  constrextdg2  33914  constrext2chnlem  33915  constrcon  33939  2sqr3minply  33945  cos9thpiminply  33953  unitssxrge0  34065  iistmd  34067  mhmhmeotmd  34092  xrge0tmdALT  34111  rerrext  34174  cnrrext  34175  volmeas  34396  ddemeas  34401  fib1  34565  ballotlem2  34654  ballotth  34703  prodfzo03  34768  bj-pinftyccb  37548  fdc  38077  riscer  38320  asin1half  42800  acos1half  42801  readvrec2  42804  jm2.27dlem2  43453  arearect  43658  areaquad  43659  onsucf1o  43715  lhe4.4ex1a  44771  wallispilem4  46511  fourierdlem20  46570  fourierdlem62  46611  fourierdlem104  46653  fourierdlem111  46660  sqwvfoura  46671  sqwvfourb  46672  fouriersw  46674  fmtnoprmfac2lem1  48026  fmtno4prmfac  48032  31prm  48057  nprmdvdsfacm1lem4  48083  nprmdvdsfacm1  48084  ppivalnnnprmge6  48086  341fppr2  48207  4fppr1  48208  9fppr8  48210  nfermltl8rev  48215  nfermltl2rev  48216  sbgoldbo  48260  nnsum4primeseven  48273  nnsum4primesevenALTV  48274  wtgoldbnnsum4prm  48275  bgoldbnnsum3prm  48277  tgblthelfgott  48288  cycl3grtri  48420  usgrexmpl1lem  48494  usgrexmpl2lem  48499  usgrexmpl2trifr  48510  gpg5nbgrvtx13starlem2  48545  gpg5nbgr3star  48554  gpg5edgnedg  48603  grlimedgnedg  48604  2zlidl  48713  2zrngALT  48727  nnpw2blen  49053