Theorem mpbir3an 1340

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

Syntax hints:   ↔ wb 205   ∧ w3a 1086

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

This theorem is referenced by:  snopeqopsnid  5424  limon  7692  issmo  8188  xpider  8586  omina  10456  1eluzge0  12641  2eluzge1  12643  0elunit  13210  1elunit  13211  fz0to3un2pr  13367  4fvwrd4  13385  fzo0to42pr  13483  ccat2s1p2  14346  ccat2s1p2OLD  14348  cats1fv  14581  pfx2  14669  wwlktovf  14680  fprodge0  15712  fprodge1  15714  sincos1sgn  15911  sincos2sgn  15912  divalglem7  16117  igz  16644  strleun  16867  strle1  16868  letsr  18320  psgnunilem2  19112  cnfldfun  20618  xrge0subm  20648  cnsubmlem  20655  cnsubglem  20656  cnsubrglem  20657  cnmsubglem  20670  nn0srg  20677  rge0srg  20678  ust0  23380  cnngp  23952  cnfldtgp  24041  htpycc  24152  pco0  24186  pcocn  24189  pcohtpylem  24191  pcopt  24194  pcopt2  24195  pcoass  24196  pcorevlem  24198  sinhalfpilem  25629  sincos4thpi  25679  sincos6thpi  25681  argregt0  25774  argrege0  25775  elogb  25929  2logb9irr  25954  2logb9irrALT  25957  sqrt2cxp2logb9e3  25958  asin1  26053  atanbnd  26085  atan1  26087  harmonicbnd3  26166  ppiublem1  26359  usgrexmplef  27635  usgr2pthlem  28140  uspgrn2crct  28182  upgr3v3e3cycl  28553  upgr4cycl4dv4e  28558  konigsbergiedgw  28621  konigsberglem1  28625  konigsberglem2  28626  konigsberglem3  28627  konigsberglem4  28628  ex-opab  28805  isgrpoi  28869  isvciOLD  28951  isnvi  28984  adj1o  30265  bra11  30479  xrge0omnd  31346  reofld  31553  xrge0slmod  31557  ccfldsrarelvec  31750  unitssxrge0  31859  iistmd  31861  mhmhmeotmd  31886  xrge0tmdALT  31905  rerrext  31968  cnrrext  31969  volmeas  32208  ddemeas  32213  fib1  32376  ballotlem2  32464  ballotth  32513  prodfzo03  32592  logi  33709  bj-pinftyccb  35401  fdc  35912  riscer  36155  acos1half  40177  jm2.27dlem2  40839  arearect  41053  areaquad  41054  lhe4.4ex1a  41954  wallispilem4  43616  fourierdlem20  43675  fourierdlem62  43716  fourierdlem104  43758  fourierdlem111  43765  sqwvfoura  43776  sqwvfourb  43777  fouriersw  43779  fmtnoprmfac2lem1  45029  fmtno4prmfac  45035  31prm  45060  341fppr2  45197  4fppr1  45198  9fppr8  45200  nfermltl8rev  45205  nfermltl2rev  45206  sbgoldbo  45250  nnsum4primeseven  45263  nnsum4primesevenALTV  45264  wtgoldbnnsum4prm  45265  bgoldbnnsum3prm  45267  tgblthelfgott  45278  2zlidl  45503  2zrngALT  45517  nnpw2blen  45937  tworepnotupword  46532