Theorem mpbir3an 1339

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

Syntax hints:   ↔ wb 205   ∧ w3a 1085

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

This theorem is referenced by:  snopeqopsnid  5505  limon  7833  issmo  8362  xpider  8800  omina  10708  1eluzge0  12900  2eluzge1  12902  0elunit  13472  1elunit  13473  fz0to3un2pr  13629  4fvwrd4  13647  fzo0to42pr  13745  ccat2s1p2  14606  cats1fv  14836  pfx2  14924  wwlktovf  14933  fprodge0  15963  fprodge1  15965  sincos1sgn  16163  sincos2sgn  16164  divalglem7  16369  igz  16896  strleun  17119  strle1  17120  letsr  18578  psgnunilem2  19443  cnfldfun  21286  cnfldfunOLD  21299  xrge0subm  21333  cnsubmlem  21340  cnsubglem  21341  cnsubrglem  21342  cnsubrglemOLD  21343  cnmsubglem  21356  nn0srg  21363  rge0srg  21364  pzriprnglem4  21403  ust0  24117  cnngp  24689  cnfldtgp  24780  htpycc  24899  pco0  24934  pcocn  24937  pcohtpylem  24939  pcopt  24942  pcopt2  24943  pcoass  24944  pcorevlem  24946  sinhalfpilem  26391  sincos4thpi  26441  sincos6thpi  26443  logi  26514  argregt0  26537  argrege0  26538  elogb  26695  2logb9irr  26720  2logb9irrALT  26723  sqrt2cxp2logb9e3  26724  asin1  26819  atanbnd  26851  atan1  26853  harmonicbnd3  26933  ppiublem1  27128  usgrexmplef  29065  usgr2pthlem  29570  uspgrn2crct  29612  upgr3v3e3cycl  29983  upgr4cycl4dv4e  29988  konigsbergiedgw  30051  konigsberglem1  30055  konigsberglem2  30056  konigsberglem3  30057  konigsberglem4  30058  ex-opab  30235  isgrpoi  30301  isvciOLD  30383  isnvi  30416  adj1o  31697  bra11  31911  xrge0omnd  32785  1fldgenq  33003  reofld  33050  xrge0slmod  33054  ccfldsrarelvec  33349  unitssxrge0  33495  iistmd  33497  mhmhmeotmd  33522  xrge0tmdALT  33541  rerrext  33604  cnrrext  33605  volmeas  33844  ddemeas  33849  fib1  34014  ballotlem2  34102  ballotth  34151  prodfzo03  34229  bj-pinftyccb  36694  fdc  37212  riscer  37455  acos1half  42091  jm2.27dlem2  42425  arearect  42637  areaquad  42638  onsucf1o  42695  lhe4.4ex1a  43760  wallispilem4  45450  fourierdlem20  45509  fourierdlem62  45550  fourierdlem104  45592  fourierdlem111  45599  sqwvfoura  45610  sqwvfourb  45611  fouriersw  45613  tworepnotupword  46266  fmtnoprmfac2lem1  46900  fmtno4prmfac  46906  31prm  46931  341fppr2  47068  4fppr1  47069  9fppr8  47071  nfermltl8rev  47076  nfermltl2rev  47077  sbgoldbo  47121  nnsum4primeseven  47134  nnsum4primesevenALTV  47135  wtgoldbnnsum4prm  47136  bgoldbnnsum3prm  47138  tgblthelfgott  47149  2zlidl  47296  2zrngALT  47310  nnpw2blen  47647