Theorem mpbir3an 1337

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

Syntax hints:   ↔ wb 208   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  snopeqopsnid  5399  limon  7551  issmo  7985  xpider  8368  omina  10113  1eluzge0  12293  2eluzge1  12295  0elunit  12856  1elunit  12857  fz0to3un2pr  13010  4fvwrd4  13028  fzo0to42pr  13125  ccat2s1p2  13986  ccat2s1p2OLD  13988  cats1fv  14221  pfx2  14309  wwlktovf  14320  fprodge0  15347  fprodge1  15349  sincos1sgn  15546  sincos2sgn  15547  divalglem7  15750  igz  16270  strleun  16591  strle1  16592  letsr  17837  psgnunilem2  18623  cnfldfunALT  20558  xrge0subm  20586  cnsubmlem  20593  cnsubglem  20594  cnsubrglem  20595  cnmsubglem  20608  nn0srg  20615  rge0srg  20616  ust0  22828  cnngp  23388  cnfldtgp  23477  htpycc  23584  pco0  23618  pcocn  23621  pcohtpylem  23623  pcopt  23626  pcopt2  23627  pcoass  23628  pcorevlem  23630  sinhalfpilem  25049  sincos4thpi  25099  sincos6thpi  25101  argregt0  25193  argrege0  25194  elogb  25348  2logb9irr  25373  2logb9irrALT  25376  sqrt2cxp2logb9e3  25377  asin1  25472  atanbnd  25504  atan1  25506  harmonicbnd3  25585  ppiublem1  25778  usgrexmplef  27041  usgr2pthlem  27544  uspgrn2crct  27586  upgr3v3e3cycl  27959  upgr4cycl4dv4e  27964  konigsbergiedgw  28027  konigsberglem1  28031  konigsberglem2  28032  konigsberglem3  28033  konigsberglem4  28034  ex-opab  28211  isgrpoi  28275  isvciOLD  28357  isnvi  28390  adj1o  29671  bra11  29885  xrge0omnd  30712  reofld  30913  xrge0slmod  30917  ccfldsrarelvec  31056  unitssxrge0  31143  iistmd  31145  mhmhmeotmd  31170  xrge0tmdALT  31189  rerrext  31250  cnrrext  31251  volmeas  31490  ddemeas  31495  fib1  31658  ballotlem2  31746  ballotth  31795  prodfzo03  31874  logi  32966  bj-pinftyccb  34506  fdc  35035  riscer  35281  jm2.27dlem2  39627  arearect  39842  areaquad  39843  lhe4.4ex1a  40681  wallispilem4  42373  fourierdlem20  42432  fourierdlem62  42473  fourierdlem104  42515  fourierdlem111  42522  sqwvfoura  42533  sqwvfourb  42534  fouriersw  42536  fmtnoprmfac2lem1  43748  fmtno4prmfac  43754  31prm  43780  341fppr2  43919  4fppr1  43920  9fppr8  43922  nfermltl8rev  43927  nfermltl2rev  43928  sbgoldbo  43972  nnsum4primeseven  43985  nnsum4primesevenALTV  43986  wtgoldbnnsum4prm  43987  bgoldbnnsum3prm  43989  tgblthelfgott  44000  2zlidl  44225  2zrngALT  44239  nnpw2blen  44660