Theorem mpbir3an 1342

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

Syntax hints:   ↔ wb 206   ∧ w3a 1086

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 1088

This theorem is referenced by:  snopeqopsnid  5456  limon  7775  issmo  8278  xpider  8722  omina  10604  1eluzge0  12799  2eluzge1  12801  5eluz3  12802  0elunit  13390  1elunit  13391  fz0to3un2pr  13550  fz0to4untppr  13551  fz0to5un2tp  13552  4fvwrd4  13569  fzo0to42pr  13674  fvf1tp  13711  tpf1ofv1  14422  tpf1ofv2  14423  tpfo  14425  ccat2s1p2  14555  cats1fv  14784  pfx2  14872  wwlktovf  14881  fprodge0  15918  fprodge1  15920  sincos1sgn  16120  sincos2sgn  16121  divalglem7  16328  igz  16864  strleun  17086  strle1  17087  letsr  18517  psgnunilem2  19392  cnfldfun  21293  cnfldfunOLD  21306  cnsubmlem  21339  cnsubglem  21340  cnsubrglem  21341  cnsubrglemOLD  21342  cnmsubglem  21355  nn0srg  21362  rge0srg  21363  xrge0subm  21368  xrge0omnd  21370  pzriprnglem4  21409  ust0  24123  cnngp  24683  cnfldtgp  24776  htpycc  24895  pco0  24930  pcocn  24933  pcohtpylem  24935  pcopt  24938  pcopt2  24939  pcoass  24940  pcorevlem  24942  sinhalfpilem  26388  sincos4thpi  26438  sincos6thpi  26441  logi  26512  argregt0  26535  argrege0  26536  elogb  26696  2logb9irr  26721  2logb9irrALT  26724  sqrt2cxp2logb9e3  26725  asin1  26820  atanbnd  26852  atan1  26854  harmonicbnd3  26934  ppiublem1  27129  zsoring  28319  usgrexmplef  29222  usgr2pthlem  29726  uspgrn2crct  29771  upgr3v3e3cycl  30142  upgr4cycl4dv4e  30147  konigsbergiedgw  30210  konigsberglem1  30214  konigsberglem2  30215  konigsberglem3  30216  konigsberglem4  30217  ex-opab  30394  isgrpoi  30460  isvciOLD  30542  isnvi  30575  adj1o  31856  bra11  32070  1fldgenq  33271  reofld  33291  xrge0slmod  33295  ccfldsrarelvec  33642  constrextdg2  33715  constrext2chnlem  33716  constrcon  33740  2sqr3minply  33746  cos9thpiminply  33754  unitssxrge0  33866  iistmd  33868  mhmhmeotmd  33893  xrge0tmdALT  33912  rerrext  33975  cnrrext  33976  volmeas  34197  ddemeas  34202  fib1  34367  ballotlem2  34456  ballotth  34505  prodfzo03  34570  bj-pinftyccb  37194  fdc  37724  riscer  37967  asin1half  42330  acos1half  42331  readvrec2  42334  jm2.27dlem2  42983  arearect  43188  areaquad  43189  onsucf1o  43245  lhe4.4ex1a  44302  wallispilem4  46050  fourierdlem20  46109  fourierdlem62  46150  fourierdlem104  46192  fourierdlem111  46199  sqwvfoura  46210  sqwvfourb  46211  fouriersw  46213  tworepnotupword  46868  fmtnoprmfac2lem1  47551  fmtno4prmfac  47557  31prm  47582  341fppr2  47719  4fppr1  47720  9fppr8  47722  nfermltl8rev  47727  nfermltl2rev  47728  sbgoldbo  47772  nnsum4primeseven  47785  nnsum4primesevenALTV  47786  wtgoldbnnsum4prm  47787  bgoldbnnsum3prm  47789  tgblthelfgott  47800  cycl3grtri  47930  usgrexmpl1lem  47996  usgrexmpl2lem  48001  usgrexmpl2trifr  48012  gpg5nbgrvtx13starlem2  48047  gpg5nbgr3star  48056  2zlidl  48212  2zrngALT  48226  nnpw2blen  48553