Theorem mpbir3an 1340

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

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

This theorem is referenced by:  snopeqopsnid  5509  limon  7827  issmo  8351  xpider  8785  omina  10689  1eluzge0  12881  2eluzge1  12883  0elunit  13451  1elunit  13452  fz0to3un2pr  13608  4fvwrd4  13626  fzo0to42pr  13724  ccat2s1p2  14585  cats1fv  14815  pfx2  14903  wwlktovf  14912  fprodge0  15942  fprodge1  15944  sincos1sgn  16141  sincos2sgn  16142  divalglem7  16347  igz  16872  strleun  17095  strle1  17096  letsr  18551  psgnunilem2  19405  cnfldfun  21157  xrge0subm  21187  cnsubmlem  21194  cnsubglem  21195  cnsubrglem  21196  cnmsubglem  21209  nn0srg  21216  rge0srg  21217  pzriprnglem4  21254  ust0  23945  cnngp  24517  cnfldtgp  24608  htpycc  24727  pco0  24762  pcocn  24765  pcohtpylem  24767  pcopt  24770  pcopt2  24771  pcoass  24772  pcorevlem  24774  sinhalfpilem  26210  sincos4thpi  26260  sincos6thpi  26262  argregt0  26355  argrege0  26356  elogb  26512  2logb9irr  26537  2logb9irrALT  26540  sqrt2cxp2logb9e3  26541  asin1  26636  atanbnd  26668  atan1  26670  harmonicbnd3  26749  ppiublem1  26942  usgrexmplef  28784  usgr2pthlem  29288  uspgrn2crct  29330  upgr3v3e3cycl  29701  upgr4cycl4dv4e  29706  konigsbergiedgw  29769  konigsberglem1  29773  konigsberglem2  29774  konigsberglem3  29775  konigsberglem4  29776  ex-opab  29953  isgrpoi  30019  isvciOLD  30101  isnvi  30134  adj1o  31415  bra11  31629  xrge0omnd  32500  1fldgenq  32683  reofld  32730  xrge0slmod  32734  ccfldsrarelvec  33035  unitssxrge0  33179  iistmd  33181  mhmhmeotmd  33206  xrge0tmdALT  33225  rerrext  33288  cnrrext  33289  volmeas  33528  ddemeas  33533  fib1  33698  ballotlem2  33786  ballotth  33835  prodfzo03  33914  logi  35009  gg-cnfldfun  35484  bj-pinftyccb  36406  fdc  36917  riscer  37160  acos1half  41718  jm2.27dlem2  42052  arearect  42267  areaquad  42268  onsucf1o  42325  lhe4.4ex1a  43391  wallispilem4  45083  fourierdlem20  45142  fourierdlem62  45183  fourierdlem104  45225  fourierdlem111  45232  sqwvfoura  45243  sqwvfourb  45244  fouriersw  45246  tworepnotupword  45899  fmtnoprmfac2lem1  46533  fmtno4prmfac  46539  31prm  46564  341fppr2  46701  4fppr1  46702  9fppr8  46704  nfermltl8rev  46709  nfermltl2rev  46710  sbgoldbo  46754  nnsum4primeseven  46767  nnsum4primesevenALTV  46768  wtgoldbnnsum4prm  46769  bgoldbnnsum3prm  46771  tgblthelfgott  46782  2zlidl  46921  2zrngALT  46935  nnpw2blen  47354