Theorem mpbir3an 1343

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 1341	. 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  5464  f1oi  6819  limon  7787  issmo  8288  xpider  8735  omina  10614  1eluzge0  12830  2eluzge1  12832  5eluz3  12833  0elunit  13422  1elunit  13423  fz0to3un2pr  13583  fz0to4untppr  13584  fz0to5un2tp  13585  4fvwrd4  13602  fzo0to42pr  13708  fvf1tp  13748  tpf1ofv1  14459  tpf1ofv2  14460  tpfo  14462  ccat2s1p2  14593  cats1fv  14821  pfx2  14909  wwlktovf  14918  fprodge0  15958  fprodge1  15960  sincos1sgn  16160  sincos2sgn  16161  divalglem7  16368  igz  16905  strleun  17127  strle1  17128  letsr  18559  psgnunilem2  19470  cnfldfun  21366  cnsubmlem  21395  cnsubglem  21396  cnsubrglem  21397  cnmsubglem  21410  nn0srg  21417  rge0srg  21418  xrge0subm  21423  xrge0omnd  21425  pzriprnglem4  21464  ust0  24185  cnngp  24744  cnfldtgp  24836  htpycc  24947  pco0  24981  pcocn  24984  pcohtpylem  24986  pcopt  24989  pcopt2  24990  pcoass  24991  pcorevlem  24993  sinhalfpilem  26427  sincos4thpi  26477  sincos6thpi  26480  logi  26551  argregt0  26574  argrege0  26575  elogb  26734  2logb9irr  26759  2logb9irrALT  26762  sqrt2cxp2logb9e3  26763  asin1  26858  atanbnd  26890  atan1  26892  harmonicbnd3  26971  ppiublem1  27165  zsoring  28401  usgrexmplef  29328  usgr2pthlem  29831  uspgrn2crct  29876  upgr3v3e3cycl  30250  upgr4cycl4dv4e  30255  konigsbergiedgw  30318  konigsberglem1  30322  konigsberglem2  30323  konigsberglem3  30324  konigsberglem4  30325  ex-opab  30502  isgrpoi  30569  isvciOLD  30651  isnvi  30684  adj1o  31965  bra11  32179  1fldgenq  33383  reofld  33403  xrge0slmod  33408  ccfldsrarelvec  33815  constrextdg2  33893  constrext2chnlem  33894  constrcon  33918  2sqr3minply  33924  cos9thpiminply  33932  unitssxrge0  34044  iistmd  34046  mhmhmeotmd  34071  xrge0tmdALT  34090  rerrext  34153  cnrrext  34154  volmeas  34375  ddemeas  34380  fib1  34544  ballotlem2  34633  ballotth  34682  prodfzo03  34747  bj-pinftyccb  37535  fdc  38066  riscer  38309  asin1half  42789  acos1half  42790  readvrec2  42793  jm2.27dlem2  43438  arearect  43643  areaquad  43644  onsucf1o  43700  lhe4.4ex1a  44756  wallispilem4  46496  fourierdlem20  46555  fourierdlem62  46596  fourierdlem104  46638  fourierdlem111  46645  sqwvfoura  46656  sqwvfourb  46657  fouriersw  46659  goldrapos  47327  fmtnoprmfac2lem1  48023  fmtno4prmfac  48029  31prm  48054  nprmdvdsfacm1lem4  48080  nprmdvdsfacm1  48081  ppivalnnnprmge6  48083  341fppr2  48204  4fppr1  48205  9fppr8  48207  nfermltl8rev  48212  nfermltl2rev  48213  sbgoldbo  48257  nnsum4primeseven  48270  nnsum4primesevenALTV  48271  wtgoldbnnsum4prm  48272  bgoldbnnsum3prm  48274  tgblthelfgott  48285  cycl3grtri  48417  usgrexmpl1lem  48491  usgrexmpl2lem  48496  usgrexmpl2trifr  48507  gpg5nbgrvtx13starlem2  48542  gpg5nbgr3star  48551  gpg5edgnedg  48600  grlimedgnedg  48601  2zlidl  48710  2zrngALT  48724  nnpw2blen  49050