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 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  5518  limon  7855  issmo  8386  xpider  8826  omina  10728  5eluz3  12924  1eluzge0  12931  2eluzge1  12933  0elunit  13505  1elunit  13506  fz0to3un2pr  13665  fz0to4untppr  13666  fz0to5un2tp  13667  4fvwrd4  13684  fzo0to42pr  13788  fvf1tp  13825  tpf1ofv1  14532  tpf1ofv2  14533  tpfo  14535  ccat2s1p2  14664  cats1fv  14894  pfx2  14982  wwlktovf  14991  fprodge0  16025  fprodge1  16027  sincos1sgn  16225  sincos2sgn  16226  divalglem7  16432  igz  16967  strleun  17190  strle1  17191  letsr  18650  psgnunilem2  19527  cnfldfun  21395  cnfldfunOLD  21408  xrge0subm  21442  cnsubmlem  21449  cnsubglem  21450  cnsubrglem  21451  cnsubrglemOLD  21452  cnmsubglem  21465  nn0srg  21472  rge0srg  21473  pzriprnglem4  21512  ust0  24243  cnngp  24815  cnfldtgp  24906  htpycc  25025  pco0  25060  pcocn  25063  pcohtpylem  25065  pcopt  25068  pcopt2  25069  pcoass  25070  pcorevlem  25072  sinhalfpilem  26519  sincos4thpi  26569  sincos6thpi  26572  logi  26643  argregt0  26666  argrege0  26667  elogb  26827  2logb9irr  26852  2logb9irrALT  26855  sqrt2cxp2logb9e3  26856  asin1  26951  atanbnd  26983  atan1  26985  harmonicbnd3  27065  ppiublem1  27260  usgrexmplef  29290  usgr2pthlem  29795  uspgrn2crct  29837  upgr3v3e3cycl  30208  upgr4cycl4dv4e  30213  konigsbergiedgw  30276  konigsberglem1  30280  konigsberglem2  30281  konigsberglem3  30282  konigsberglem4  30283  ex-opab  30460  isgrpoi  30526  isvciOLD  30608  isnvi  30641  adj1o  31922  bra11  32136  xrge0omnd  33070  1fldgenq  33303  reofld  33351  xrge0slmod  33355  ccfldsrarelvec  33695  2sqr3minply  33752  unitssxrge0  33860  iistmd  33862  mhmhmeotmd  33887  xrge0tmdALT  33906  rerrext  33971  cnrrext  33972  volmeas  34211  ddemeas  34216  fib1  34381  ballotlem2  34469  ballotth  34518  prodfzo03  34596  bj-pinftyccb  37203  fdc  37731  riscer  37974  asin1half  42365  acos1half  42366  readvrec2  42369  jm2.27dlem2  42998  arearect  43203  areaquad  43204  onsucf1o  43261  lhe4.4ex1a  44324  wallispilem4  46023  fourierdlem20  46082  fourierdlem62  46123  fourierdlem104  46165  fourierdlem111  46172  sqwvfoura  46183  sqwvfourb  46184  fouriersw  46186  tworepnotupword  46839  fmtnoprmfac2lem1  47490  fmtno4prmfac  47496  31prm  47521  341fppr2  47658  4fppr1  47659  9fppr8  47661  nfermltl8rev  47666  nfermltl2rev  47667  sbgoldbo  47711  nnsum4primeseven  47724  nnsum4primesevenALTV  47725  wtgoldbnnsum4prm  47726  bgoldbnnsum3prm  47728  tgblthelfgott  47739  usgrexmpl1lem  47915  usgrexmpl2lem  47920  usgrexmpl2trifr  47931  gpg5nbgrvtx13starlem2  47962  gpg5nbgr3star  47971  gpg5grlic  47974  2zlidl  48083  2zrngALT  48097  nnpw2blen  48429