Theorem mpbir3an 1339

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

Syntax hints:   ↔ wb 205   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  snopeqopsnid  5417  limon  7658  issmo  8150  xpider  8535  omina  10378  1eluzge0  12561  2eluzge1  12563  0elunit  13130  1elunit  13131  fz0to3un2pr  13287  4fvwrd4  13305  fzo0to42pr  13402  ccat2s1p2  14265  ccat2s1p2OLD  14267  cats1fv  14500  pfx2  14588  wwlktovf  14599  fprodge0  15631  fprodge1  15633  sincos1sgn  15830  sincos2sgn  15831  divalglem7  16036  igz  16563  strleun  16786  strle1  16787  letsr  18226  psgnunilem2  19018  cnfldfunALT  20523  xrge0subm  20551  cnsubmlem  20558  cnsubglem  20559  cnsubrglem  20560  cnmsubglem  20573  nn0srg  20580  rge0srg  20581  ust0  23279  cnngp  23849  cnfldtgp  23938  htpycc  24049  pco0  24083  pcocn  24086  pcohtpylem  24088  pcopt  24091  pcopt2  24092  pcoass  24093  pcorevlem  24095  sinhalfpilem  25525  sincos4thpi  25575  sincos6thpi  25577  argregt0  25670  argrege0  25671  elogb  25825  2logb9irr  25850  2logb9irrALT  25853  sqrt2cxp2logb9e3  25854  asin1  25949  atanbnd  25981  atan1  25983  harmonicbnd3  26062  ppiublem1  26255  usgrexmplef  27529  usgr2pthlem  28032  uspgrn2crct  28074  upgr3v3e3cycl  28445  upgr4cycl4dv4e  28450  konigsbergiedgw  28513  konigsberglem1  28517  konigsberglem2  28518  konigsberglem3  28519  konigsberglem4  28520  ex-opab  28697  isgrpoi  28761  isvciOLD  28843  isnvi  28876  adj1o  30157  bra11  30371  xrge0omnd  31239  reofld  31446  xrge0slmod  31450  ccfldsrarelvec  31643  unitssxrge0  31752  iistmd  31754  mhmhmeotmd  31779  xrge0tmdALT  31798  rerrext  31859  cnrrext  31860  volmeas  32099  ddemeas  32104  fib1  32267  ballotlem2  32355  ballotth  32404  prodfzo03  32483  logi  33606  bj-pinftyccb  35319  fdc  35830  riscer  36073  acos1half  40098  jm2.27dlem2  40748  arearect  40962  areaquad  40963  lhe4.4ex1a  41836  wallispilem4  43499  fourierdlem20  43558  fourierdlem62  43599  fourierdlem104  43641  fourierdlem111  43648  sqwvfoura  43659  sqwvfourb  43660  fouriersw  43662  fmtnoprmfac2lem1  44906  fmtno4prmfac  44912  31prm  44937  341fppr2  45074  4fppr1  45075  9fppr8  45077  nfermltl8rev  45082  nfermltl2rev  45083  sbgoldbo  45127  nnsum4primeseven  45140  nnsum4primesevenALTV  45141  wtgoldbnnsum4prm  45142  bgoldbnnsum3prm  45144  tgblthelfgott  45155  2zlidl  45380  2zrngALT  45394  nnpw2blen  45814