Theorem mpbir3an 1321

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

Syntax hints:   ↔ wb 198   ∧ w3a 1068

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 199  df-an 388  df-3an 1070

This theorem is referenced by:  snopeqopsnid  5251  limon  7365  issmo  7787  xpider  8166  omina  9909  1eluzge0  12104  2eluzge1  12106  0elunit  12669  1elunit  12670  fz0to3un2pr  12823  4fvwrd4  12841  fzo0to42pr  12937  ccat2s1p2  13791  cats1fv  14081  pfx2  14169  wwlktovf  14179  fprodge0  15205  fprodge1  15207  sincos1sgn  15404  sincos2sgn  15405  divalglem7  15608  igz  16124  strleun  16445  strle1  16446  letsr  17707  psgnunilem2  18397  cnfldfunALT  20272  xrge0subm  20300  cnsubmlem  20307  cnsubglem  20308  cnsubrglem  20309  cnmsubglem  20322  nn0srg  20329  rge0srg  20330  ust0  22543  cnngp  23103  cnfldtgp  23192  htpycc  23299  pco0  23333  pcocn  23336  pcohtpylem  23338  pcopt  23341  pcopt2  23342  pcoass  23343  pcorevlem  23345  sinhalfpilem  24764  sincos4thpi  24814  sincos6thpi  24816  argregt0  24906  argrege0  24907  elogb  25061  2logb9irr  25086  2logb9irrALT  25089  sqrt2cxp2logb9e3  25090  asin1  25185  atanbnd  25217  atan1  25219  harmonicbnd3  25299  ppiublem1  25492  usgrexmplef  26756  usgr2pthlem  27264  uspgrn2crct  27306  upgr3v3e3cycl  27721  upgr4cycl4dv4e  27726  konigsbergiedgw  27792  konigsberglem1  27796  konigsberglem2  27797  konigsberglem3  27798  konigsberglem4  27799  ex-opab  28001  isgrpoi  28064  isvciOLD  28146  isnvi  28179  adj1o  29464  bra11  29678  xrge0omnd  30453  reofld  30621  xrge0slmod  30625  ccfldsrarelvec  30714  unitssxrge0  30816  iistmd  30818  mhmhmeotmd  30843  xrge0tmdOLD  30861  rerrext  30923  cnrrext  30924  volmeas  31164  ddemeas  31169  fib1  31333  ballotlem2  31421  ballotth  31470  prodfzo03  31551  logi  32515  bj-pinftyccb  34001  fdc  34491  riscer  34737  jm2.27dlem2  39032  arearect  39247  areaquad  39248  lhe4.4ex1a  40106  wallispilem4  41809  fourierdlem20  41868  fourierdlem62  41909  fourierdlem104  41951  fourierdlem111  41958  sqwvfoura  41969  sqwvfourb  41970  fouriersw  41972  fmtnoprmfac2lem1  43121  fmtno4prmfac  43127  31prm  43153  341fppr2  43292  4fppr1  43293  9fppr8  43295  nfermltl8rev  43300  nfermltl2rev  43301  sbgoldbo  43345  nnsum4primeseven  43358  nnsum4primesevenALTV  43359  wtgoldbnnsum4prm  43360  bgoldbnnsum3prm  43362  tgblthelfgott  43373  2zlidl  43594  2zrngALT  43608  nnpw2blen  44033