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 397  df-3an 1088

This theorem is referenced by:  snopeqopsnid  5426  limon  7675  issmo  8168  xpider  8558  omina  10446  1eluzge0  12629  2eluzge1  12631  0elunit  13198  1elunit  13199  fz0to3un2pr  13355  4fvwrd4  13373  fzo0to42pr  13470  ccat2s1p2  14333  ccat2s1p2OLD  14335  cats1fv  14568  pfx2  14656  wwlktovf  14667  fprodge0  15699  fprodge1  15701  sincos1sgn  15898  sincos2sgn  15899  divalglem7  16104  igz  16631  strleun  16854  strle1  16855  letsr  18307  psgnunilem2  19099  cnfldfunALT  20607  xrge0subm  20635  cnsubmlem  20642  cnsubglem  20643  cnsubrglem  20644  cnmsubglem  20657  nn0srg  20664  rge0srg  20665  ust0  23367  cnngp  23939  cnfldtgp  24028  htpycc  24139  pco0  24173  pcocn  24176  pcohtpylem  24178  pcopt  24181  pcopt2  24182  pcoass  24183  pcorevlem  24185  sinhalfpilem  25616  sincos4thpi  25666  sincos6thpi  25668  argregt0  25761  argrege0  25762  elogb  25916  2logb9irr  25941  2logb9irrALT  25944  sqrt2cxp2logb9e3  25945  asin1  26040  atanbnd  26072  atan1  26074  harmonicbnd3  26153  ppiublem1  26346  usgrexmplef  27622  usgr2pthlem  28125  uspgrn2crct  28167  upgr3v3e3cycl  28538  upgr4cycl4dv4e  28543  konigsbergiedgw  28606  konigsberglem1  28610  konigsberglem2  28611  konigsberglem3  28612  konigsberglem4  28613  ex-opab  28790  isgrpoi  28854  isvciOLD  28936  isnvi  28969  adj1o  30250  bra11  30464  xrge0omnd  31331  reofld  31538  xrge0slmod  31542  ccfldsrarelvec  31735  unitssxrge0  31844  iistmd  31846  mhmhmeotmd  31871  xrge0tmdALT  31890  rerrext  31953  cnrrext  31954  volmeas  32193  ddemeas  32198  fib1  32361  ballotlem2  32449  ballotth  32498  prodfzo03  32577  logi  33694  bj-pinftyccb  35386  fdc  35897  riscer  36140  acos1half  40165  jm2.27dlem2  40827  arearect  41041  areaquad  41042  lhe4.4ex1a  41915  wallispilem4  43578  fourierdlem20  43637  fourierdlem62  43678  fourierdlem104  43720  fourierdlem111  43727  sqwvfoura  43738  sqwvfourb  43739  fouriersw  43741  fmtnoprmfac2lem1  44985  fmtno4prmfac  44991  31prm  45016  341fppr2  45153  4fppr1  45154  9fppr8  45156  nfermltl8rev  45161  nfermltl2rev  45162  sbgoldbo  45206  nnsum4primeseven  45219  nnsum4primesevenALTV  45220  wtgoldbnnsum4prm  45221  bgoldbnnsum3prm  45223  tgblthelfgott  45234  2zlidl  45459  2zrngALT  45473  nnpw2blen  45893