Theorem mpbir3an 1341

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

Syntax hints:   ↔ wb 205   ∧ 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  snopeqopsnid  5509  limon  7823  issmo  8347  xpider  8781  omina  10685  1eluzge0  12875  2eluzge1  12877  0elunit  13445  1elunit  13446  fz0to3un2pr  13602  4fvwrd4  13620  fzo0to42pr  13718  ccat2s1p2  14579  cats1fv  14809  pfx2  14897  wwlktovf  14906  fprodge0  15936  fprodge1  15938  sincos1sgn  16135  sincos2sgn  16136  divalglem7  16341  igz  16866  strleun  17089  strle1  17090  letsr  18545  psgnunilem2  19362  cnfldfun  20955  xrge0subm  20985  cnsubmlem  20992  cnsubglem  20993  cnsubrglem  20994  cnmsubglem  21007  nn0srg  21014  rge0srg  21015  ust0  23723  cnngp  24295  cnfldtgp  24384  htpycc  24495  pco0  24529  pcocn  24532  pcohtpylem  24534  pcopt  24537  pcopt2  24538  pcoass  24539  pcorevlem  24541  sinhalfpilem  25972  sincos4thpi  26022  sincos6thpi  26024  argregt0  26117  argrege0  26118  elogb  26272  2logb9irr  26297  2logb9irrALT  26300  sqrt2cxp2logb9e3  26301  asin1  26396  atanbnd  26428  atan1  26430  harmonicbnd3  26509  ppiublem1  26702  usgrexmplef  28513  usgr2pthlem  29017  uspgrn2crct  29059  upgr3v3e3cycl  29430  upgr4cycl4dv4e  29435  konigsbergiedgw  29498  konigsberglem1  29502  konigsberglem2  29503  konigsberglem3  29504  konigsberglem4  29505  ex-opab  29682  isgrpoi  29746  isvciOLD  29828  isnvi  29861  adj1o  31142  bra11  31356  xrge0omnd  32224  1fldgenq  32407  reofld  32454  xrge0slmod  32458  ccfldsrarelvec  32740  unitssxrge0  32875  iistmd  32877  mhmhmeotmd  32902  xrge0tmdALT  32921  rerrext  32984  cnrrext  32985  volmeas  33224  ddemeas  33229  fib1  33394  ballotlem2  33482  ballotth  33531  prodfzo03  33610  logi  34699  bj-pinftyccb  36097  fdc  36608  riscer  36851  acos1half  41025  jm2.27dlem2  41739  arearect  41954  areaquad  41955  onsucf1o  42012  lhe4.4ex1a  43078  wallispilem4  44774  fourierdlem20  44833  fourierdlem62  44874  fourierdlem104  44916  fourierdlem111  44923  sqwvfoura  44934  sqwvfourb  44935  fouriersw  44937  tworepnotupword  45590  fmtnoprmfac2lem1  46224  fmtno4prmfac  46230  31prm  46255  341fppr2  46392  4fppr1  46393  9fppr8  46395  nfermltl8rev  46400  nfermltl2rev  46401  sbgoldbo  46445  nnsum4primeseven  46458  nnsum4primesevenALTV  46459  wtgoldbnnsum4prm  46460  bgoldbnnsum3prm  46462  tgblthelfgott  46473  pzriprnglem4  46798  2zlidl  46822  2zrngALT  46836  nnpw2blen  47256