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 1087

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 1089

This theorem is referenced by:  snopeqopsnid  5514  limon  7856  issmo  8388  xpider  8828  omina  10731  5eluz3  12927  1eluzge0  12934  2eluzge1  12936  0elunit  13509  1elunit  13510  fz0to3un2pr  13669  fz0to4untppr  13670  fz0to5un2tp  13671  4fvwrd4  13688  fzo0to42pr  13792  fvf1tp  13829  tpf1ofv1  14536  tpf1ofv2  14537  tpfo  14539  ccat2s1p2  14668  cats1fv  14898  pfx2  14986  wwlktovf  14995  fprodge0  16029  fprodge1  16031  sincos1sgn  16229  sincos2sgn  16230  divalglem7  16436  igz  16972  strleun  17194  strle1  17195  letsr  18638  psgnunilem2  19513  cnfldfun  21378  cnfldfunOLD  21391  xrge0subm  21425  cnsubmlem  21432  cnsubglem  21433  cnsubrglem  21434  cnsubrglemOLD  21435  cnmsubglem  21448  nn0srg  21455  rge0srg  21456  pzriprnglem4  21495  ust0  24228  cnngp  24800  cnfldtgp  24893  htpycc  25012  pco0  25047  pcocn  25050  pcohtpylem  25052  pcopt  25055  pcopt2  25056  pcoass  25057  pcorevlem  25059  sinhalfpilem  26505  sincos4thpi  26555  sincos6thpi  26558  logi  26629  argregt0  26652  argrege0  26653  elogb  26813  2logb9irr  26838  2logb9irrALT  26841  sqrt2cxp2logb9e3  26842  asin1  26937  atanbnd  26969  atan1  26971  harmonicbnd3  27051  ppiublem1  27246  usgrexmplef  29276  usgr2pthlem  29783  uspgrn2crct  29828  upgr3v3e3cycl  30199  upgr4cycl4dv4e  30204  konigsbergiedgw  30267  konigsberglem1  30271  konigsberglem2  30272  konigsberglem3  30273  konigsberglem4  30274  ex-opab  30451  isgrpoi  30517  isvciOLD  30599  isnvi  30632  adj1o  31913  bra11  32127  xrge0omnd  33088  1fldgenq  33324  reofld  33372  xrge0slmod  33376  ccfldsrarelvec  33721  constrextdg2  33790  2sqr3minply  33791  unitssxrge0  33899  iistmd  33901  mhmhmeotmd  33926  xrge0tmdALT  33945  rerrext  34010  cnrrext  34011  volmeas  34232  ddemeas  34237  fib1  34402  ballotlem2  34491  ballotth  34540  prodfzo03  34618  bj-pinftyccb  37222  fdc  37752  riscer  37995  asin1half  42387  acos1half  42388  readvrec2  42391  jm2.27dlem2  43022  arearect  43227  areaquad  43228  onsucf1o  43285  lhe4.4ex1a  44348  wallispilem4  46083  fourierdlem20  46142  fourierdlem62  46183  fourierdlem104  46225  fourierdlem111  46232  sqwvfoura  46243  sqwvfourb  46244  fouriersw  46246  tworepnotupword  46901  fmtnoprmfac2lem1  47553  fmtno4prmfac  47559  31prm  47584  341fppr2  47721  4fppr1  47722  9fppr8  47724  nfermltl8rev  47729  nfermltl2rev  47730  sbgoldbo  47774  nnsum4primeseven  47787  nnsum4primesevenALTV  47788  wtgoldbnnsum4prm  47789  bgoldbnnsum3prm  47791  tgblthelfgott  47802  cycl3grtri  47914  usgrexmpl1lem  47980  usgrexmpl2lem  47985  usgrexmpl2trifr  47996  gpg5nbgrvtx13starlem2  48028  gpg5nbgr3star  48037  gpg5grlic  48047  2zlidl  48156  2zrngALT  48170  nnpw2blen  48501