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  5484  limon  7828  issmo  8360  xpider  8800  omina  10703  5eluz3  12899  1eluzge0  12906  2eluzge1  12908  0elunit  13484  1elunit  13485  fz0to3un2pr  13644  fz0to4untppr  13645  fz0to5un2tp  13646  4fvwrd4  13663  fzo0to42pr  13767  fvf1tp  13804  tpf1ofv1  14513  tpf1ofv2  14514  tpfo  14516  ccat2s1p2  14646  cats1fv  14876  pfx2  14964  wwlktovf  14973  fprodge0  16007  fprodge1  16009  sincos1sgn  16209  sincos2sgn  16210  divalglem7  16416  igz  16952  strleun  17174  strle1  17175  letsr  18601  psgnunilem2  19474  cnfldfun  21327  cnfldfunOLD  21340  xrge0subm  21373  cnsubmlem  21380  cnsubglem  21381  cnsubrglem  21382  cnsubrglemOLD  21383  cnmsubglem  21396  nn0srg  21403  rge0srg  21404  pzriprnglem4  21443  ust0  24156  cnngp  24716  cnfldtgp  24809  htpycc  24928  pco0  24963  pcocn  24966  pcohtpylem  24968  pcopt  24971  pcopt2  24972  pcoass  24973  pcorevlem  24975  sinhalfpilem  26422  sincos4thpi  26472  sincos6thpi  26475  logi  26546  argregt0  26569  argrege0  26570  elogb  26730  2logb9irr  26755  2logb9irrALT  26758  sqrt2cxp2logb9e3  26759  asin1  26854  atanbnd  26886  atan1  26888  harmonicbnd3  26968  ppiublem1  27163  usgrexmplef  29184  usgr2pthlem  29691  uspgrn2crct  29736  upgr3v3e3cycl  30107  upgr4cycl4dv4e  30112  konigsbergiedgw  30175  konigsberglem1  30179  konigsberglem2  30180  konigsberglem3  30181  konigsberglem4  30182  ex-opab  30359  isgrpoi  30425  isvciOLD  30507  isnvi  30540  adj1o  31821  bra11  32035  xrge0omnd  33025  1fldgenq  33262  reofld  33305  xrge0slmod  33309  ccfldsrarelvec  33658  constrextdg2  33729  constrext2chnlem  33730  constrcon  33754  2sqr3minply  33760  cos9thpiminply  33768  unitssxrge0  33877  iistmd  33879  mhmhmeotmd  33904  xrge0tmdALT  33923  rerrext  33986  cnrrext  33987  volmeas  34208  ddemeas  34213  fib1  34378  ballotlem2  34467  ballotth  34516  prodfzo03  34581  bj-pinftyccb  37185  fdc  37715  riscer  37958  asin1half  42347  acos1half  42348  readvrec2  42351  jm2.27dlem2  42981  arearect  43186  areaquad  43187  onsucf1o  43243  lhe4.4ex1a  44301  wallispilem4  46045  fourierdlem20  46104  fourierdlem62  46145  fourierdlem104  46187  fourierdlem111  46194  sqwvfoura  46205  sqwvfourb  46206  fouriersw  46208  tworepnotupword  46863  fmtnoprmfac2lem1  47528  fmtno4prmfac  47534  31prm  47559  341fppr2  47696  4fppr1  47697  9fppr8  47699  nfermltl8rev  47704  nfermltl2rev  47705  sbgoldbo  47749  nnsum4primeseven  47762  nnsum4primesevenALTV  47763  wtgoldbnnsum4prm  47764  bgoldbnnsum3prm  47766  tgblthelfgott  47777  cycl3grtri  47907  usgrexmpl1lem  47973  usgrexmpl2lem  47978  usgrexmpl2trifr  47989  gpg5nbgrvtx13starlem2  48022  gpg5nbgr3star  48031  gpg5grlic  48041  2zlidl  48163  2zrngALT  48177  nnpw2blen  48508