Theorem mpbir3an 1348

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 1346	. 2 ⊢ (𝜓 ∧ 𝜒 ∧ 𝜃)
5		mpbir3an.4	. 2 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))
6	4, 5	mpbir 232	1 ⊢ 𝜑

Syntax hints:   ↔ wb 207   ∧ w3a 1092

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

This theorem is referenced by:  snopeqopsnid  5457  f1oi  6812  limon  7783  issmo  8285  xpider  8732  omina  10612  1eluzge0  12828  2eluzge1  12830  5eluz3  12831  0elunit  13420  1elunit  13421  fz0to3un2pr  13581  fz0to4untppr  13582  fz0to5un2tp  13583  4fvwrd4  13600  fzo0to42pr  13706  fvf1tp  13746  tpf1ofv1  14457  tpf1ofv2  14458  tpfo  14460  ccat2s1p2  14591  cats1fv  14819  pfx2  14907  wwlktovf  14916  fprodge0  15956  fprodge1  15958  sincos1sgn  16158  sincos2sgn  16159  divalglem7  16366  igz  16903  strleun  17125  strle1  17126  letsr  18557  psgnunilem2  19468  cnfldfun  21368  cnsubmlem  21397  cnsubglem  21398  cnsubrglem  21399  cnmsubglem  21412  nn0srg  21419  rge0srg  21420  xrge0subm  21425  xrge0omnd  21427  pzriprnglem4  21466  ust0  24210  cnngp  24769  cnfldtgp  24861  htpycc  24972  pco0  25006  pcocn  25009  pcohtpylem  25011  pcopt  25014  pcopt2  25015  pcoass  25016  pcorevlem  25018  sinhalfpilem  26452  sincos4thpi  26502  sincos6thpi  26505  logi  26576  argregt0  26599  argrege0  26600  elogb  26759  2logb9irr  26784  2logb9irrALT  26787  sqrt2cxp2logb9e3  26788  asin1  26883  atanbnd  26915  atan1  26917  harmonicbnd3  26996  ppiublem1  27190  zsoring  28426  usgrexmplef  29353  usgr2pthlem  29856  uspgrn2crct  29901  upgr3v3e3cycl  30275  upgr4cycl4dv4e  30280  konigsbergiedgw  30343  konigsberglem1  30347  konigsberglem2  30348  konigsberglem3  30349  konigsberglem4  30350  ex-opab  30527  isgrpoi  30594  isvciOLD  30676  isnvi  30709  adj1o  31990  bra11  32204  1fldgenq  33413  reofld  33433  xrge0slmod  33438  ccfldsrarelvec  33862  constrextdg2  33940  constrext2chnlem  33941  constrcon  33965  2sqr3minply  33971  cos9thpiminply  33979  unitssxrge0  34091  iistmd  34093  mhmhmeotmd  34118  xrge0tmdALT  34137  rerrext  34200  cnrrext  34201  volmeas  34422  ddemeas  34427  fib1  34591  ballotlem2  34680  ballotth  34729  prodfzo03  34794  bj-pinftyccb  37582  fdc  38113  riscer  38356  asin1half  42835  acos1half  42836  readvrec2  42839  jm2.27dlem2  43456  arearect  43661  areaquad  43662  onsucf1o  43718  lhe4.4ex1a  44774  wallispilem4  46512  fourierdlem20  46571  fourierdlem62  46612  fourierdlem104  46654  fourierdlem111  46661  sqwvfoura  46672  sqwvfourb  46673  fouriersw  46675  goldrapos  47347  fmtnoprmfac2lem1  48045  fmtno4prmfac  48051  31prm  48076  nprmdvdsfacm1lem4  48102  nprmdvdsfacm1  48103  ppivalnnnprmge6  48105  341fppr2  48226  4fppr1  48227  9fppr8  48229  nfermltl8rev  48234  nfermltl2rev  48235  sbgoldbo  48279  nnsum4primeseven  48292  nnsum4primesevenALTV  48293  wtgoldbnnsum4prm  48294  bgoldbnnsum3prm  48296  tgblthelfgott  48307  cycl3grtri  48439  usgrexmpl1lem  48513  usgrexmpl2lem  48518  usgrexmpl2trifr  48529  gpg5nbgrvtx13starlem2  48564  gpg5nbgr3star  48573  gpg5edgnedg  48622  grlimedgnedg  48623  2zlidl  48732  2zrngALT  48746  nnpw2blen  49072