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  5465  f1oi  6820  limon  7788  issmo  8290  xpider  8737  omina  10614  1eluzge0  12805  2eluzge1  12807  5eluz3  12808  0elunit  13397  1elunit  13398  fz0to3un2pr  13557  fz0to4untppr  13558  fz0to5un2tp  13559  4fvwrd4  13576  fzo0to42pr  13681  fvf1tp  13721  tpf1ofv1  14432  tpf1ofv2  14433  tpfo  14435  ccat2s1p2  14566  cats1fv  14794  pfx2  14882  wwlktovf  14891  fprodge0  15928  fprodge1  15930  sincos1sgn  16130  sincos2sgn  16131  divalglem7  16338  igz  16874  strleun  17096  strle1  17097  letsr  18528  psgnunilem2  19436  cnfldfun  21335  cnfldfunOLD  21348  cnsubmlem  21381  cnsubglem  21382  cnsubrglem  21383  cnsubrglemOLD  21384  cnmsubglem  21397  nn0srg  21404  rge0srg  21405  xrge0subm  21410  xrge0omnd  21412  pzriprnglem4  21451  ust0  24176  cnngp  24735  cnfldtgp  24828  htpycc  24947  pco0  24982  pcocn  24985  pcohtpylem  24987  pcopt  24990  pcopt2  24991  pcoass  24992  pcorevlem  24994  sinhalfpilem  26440  sincos4thpi  26490  sincos6thpi  26493  logi  26564  argregt0  26587  argrege0  26588  elogb  26748  2logb9irr  26773  2logb9irrALT  26776  sqrt2cxp2logb9e3  26777  asin1  26872  atanbnd  26904  atan1  26906  harmonicbnd3  26986  ppiublem1  27181  zsoring  28417  usgrexmplef  29344  usgr2pthlem  29848  uspgrn2crct  29893  upgr3v3e3cycl  30267  upgr4cycl4dv4e  30272  konigsbergiedgw  30335  konigsberglem1  30339  konigsberglem2  30340  konigsberglem3  30341  konigsberglem4  30342  ex-opab  30519  isgrpoi  30585  isvciOLD  30667  isnvi  30700  adj1o  31981  bra11  32195  1fldgenq  33415  reofld  33435  xrge0slmod  33440  ccfldsrarelvec  33848  constrextdg2  33926  constrext2chnlem  33927  constrcon  33951  2sqr3minply  33957  cos9thpiminply  33965  unitssxrge0  34077  iistmd  34079  mhmhmeotmd  34104  xrge0tmdALT  34123  rerrext  34186  cnrrext  34187  volmeas  34408  ddemeas  34413  fib1  34577  ballotlem2  34666  ballotth  34715  prodfzo03  34780  bj-pinftyccb  37465  fdc  37985  riscer  38228  asin1half  42716  acos1half  42717  readvrec2  42720  jm2.27dlem2  43356  arearect  43561  areaquad  43562  onsucf1o  43618  lhe4.4ex1a  44674  wallispilem4  46415  fourierdlem20  46474  fourierdlem62  46515  fourierdlem104  46557  fourierdlem111  46564  sqwvfoura  46575  sqwvfourb  46576  fouriersw  46578  fmtnoprmfac2lem1  47915  fmtno4prmfac  47921  31prm  47946  341fppr2  48083  4fppr1  48084  9fppr8  48086  nfermltl8rev  48091  nfermltl2rev  48092  sbgoldbo  48136  nnsum4primeseven  48149  nnsum4primesevenALTV  48150  wtgoldbnnsum4prm  48151  bgoldbnnsum3prm  48153  tgblthelfgott  48164  cycl3grtri  48296  usgrexmpl1lem  48370  usgrexmpl2lem  48375  usgrexmpl2trifr  48386  gpg5nbgrvtx13starlem2  48421  gpg5nbgr3star  48430  gpg5edgnedg  48479  grlimedgnedg  48480  2zlidl  48589  2zrngALT  48603  nnpw2blen  48929