Theorem mpbir3an 1341

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 1339	. 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  5528  limon  7872  issmo  8404  xpider  8846  omina  10760  1eluzge0  12957  2eluzge1  12959  0elunit  13529  1elunit  13530  fz0to3un2pr  13686  fz0to4untppr  13687  fz0to5un2tp  13688  4fvwrd4  13705  fzo0to42pr  13803  fvf1tp  13840  tpf1ofv1  14546  tpf1ofv2  14547  tpfo  14549  ccat2s1p2  14678  cats1fv  14908  pfx2  14996  wwlktovf  15005  fprodge0  16041  fprodge1  16043  sincos1sgn  16241  sincos2sgn  16242  divalglem7  16447  igz  16981  strleun  17204  strle1  17205  letsr  18663  psgnunilem2  19537  cnfldfun  21401  cnfldfunOLD  21414  xrge0subm  21448  cnsubmlem  21455  cnsubglem  21456  cnsubrglem  21457  cnsubrglemOLD  21458  cnmsubglem  21471  nn0srg  21478  rge0srg  21479  pzriprnglem4  21518  ust0  24249  cnngp  24821  cnfldtgp  24912  htpycc  25031  pco0  25066  pcocn  25069  pcohtpylem  25071  pcopt  25074  pcopt2  25075  pcoass  25076  pcorevlem  25078  sinhalfpilem  26523  sincos4thpi  26573  sincos6thpi  26576  logi  26647  argregt0  26670  argrege0  26671  elogb  26831  2logb9irr  26856  2logb9irrALT  26859  sqrt2cxp2logb9e3  26860  asin1  26955  atanbnd  26987  atan1  26989  harmonicbnd3  27069  ppiublem1  27264  usgrexmplef  29294  usgr2pthlem  29799  uspgrn2crct  29841  upgr3v3e3cycl  30212  upgr4cycl4dv4e  30217  konigsbergiedgw  30280  konigsberglem1  30284  konigsberglem2  30285  konigsberglem3  30286  konigsberglem4  30287  ex-opab  30464  isgrpoi  30530  isvciOLD  30612  isnvi  30645  adj1o  31926  bra11  32140  xrge0omnd  33061  1fldgenq  33289  reofld  33337  xrge0slmod  33341  ccfldsrarelvec  33681  2sqr3minply  33738  unitssxrge0  33846  iistmd  33848  mhmhmeotmd  33873  xrge0tmdALT  33892  rerrext  33955  cnrrext  33956  volmeas  34195  ddemeas  34200  fib1  34365  ballotlem2  34453  ballotth  34502  prodfzo03  34580  bj-pinftyccb  37187  fdc  37705  riscer  37948  asin1half  42339  acos1half  42340  jm2.27dlem2  42967  arearect  43176  areaquad  43177  onsucf1o  43234  lhe4.4ex1a  44298  wallispilem4  45989  fourierdlem20  46048  fourierdlem62  46089  fourierdlem104  46131  fourierdlem111  46138  sqwvfoura  46149  sqwvfourb  46150  fouriersw  46152  tworepnotupword  46805  fmtnoprmfac2lem1  47440  fmtno4prmfac  47446  31prm  47471  341fppr2  47608  4fppr1  47609  9fppr8  47611  nfermltl8rev  47616  nfermltl2rev  47617  sbgoldbo  47661  nnsum4primeseven  47674  nnsum4primesevenALTV  47675  wtgoldbnnsum4prm  47676  bgoldbnnsum3prm  47678  tgblthelfgott  47689  usgrexmpl1lem  47836  usgrexmpl2lem  47841  usgrexmpl2trifr  47852  2zlidl  47963  2zrngALT  47977  nnpw2blen  48314