Theorem mpbir3an 1338

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

Syntax hints:   ↔ wb 209   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  snopeqopsnid  5364  limon  7531  issmo  7968  xpider  8351  omina  10102  1eluzge0  12280  2eluzge1  12282  0elunit  12847  1elunit  12848  fz0to3un2pr  13004  4fvwrd4  13022  fzo0to42pr  13119  ccat2s1p2  13977  ccat2s1p2OLD  13979  cats1fv  14212  pfx2  14300  wwlktovf  14311  fprodge0  15339  fprodge1  15341  sincos1sgn  15538  sincos2sgn  15539  divalglem7  15740  igz  16260  strleun  16583  strle1  16584  letsr  17829  psgnunilem2  18615  cnfldfunALT  20104  xrge0subm  20132  cnsubmlem  20139  cnsubglem  20140  cnsubrglem  20141  cnmsubglem  20154  nn0srg  20161  rge0srg  20162  ust0  22825  cnngp  23385  cnfldtgp  23474  htpycc  23585  pco0  23619  pcocn  23622  pcohtpylem  23624  pcopt  23627  pcopt2  23628  pcoass  23629  pcorevlem  23631  sinhalfpilem  25056  sincos4thpi  25106  sincos6thpi  25108  argregt0  25201  argrege0  25202  elogb  25356  2logb9irr  25381  2logb9irrALT  25384  sqrt2cxp2logb9e3  25385  asin1  25480  atanbnd  25512  atan1  25514  harmonicbnd3  25593  ppiublem1  25786  usgrexmplef  27049  usgr2pthlem  27552  uspgrn2crct  27594  upgr3v3e3cycl  27965  upgr4cycl4dv4e  27970  konigsbergiedgw  28033  konigsberglem1  28037  konigsberglem2  28038  konigsberglem3  28039  konigsberglem4  28040  ex-opab  28217  isgrpoi  28281  isvciOLD  28363  isnvi  28396  adj1o  29677  bra11  29891  xrge0omnd  30762  reofld  30964  xrge0slmod  30968  ccfldsrarelvec  31144  unitssxrge0  31253  iistmd  31255  mhmhmeotmd  31280  xrge0tmdALT  31299  rerrext  31360  cnrrext  31361  volmeas  31600  ddemeas  31605  fib1  31768  ballotlem2  31856  ballotth  31905  prodfzo03  31984  logi  33079  bj-pinftyccb  34636  fdc  35183  riscer  35426  jm2.27dlem2  39951  arearect  40165  areaquad  40166  lhe4.4ex1a  41033  wallispilem4  42710  fourierdlem20  42769  fourierdlem62  42810  fourierdlem104  42852  fourierdlem111  42859  sqwvfoura  42870  sqwvfourb  42871  fouriersw  42873  fmtnoprmfac2lem1  44083  fmtno4prmfac  44089  31prm  44114  341fppr2  44252  4fppr1  44253  9fppr8  44255  nfermltl8rev  44260  nfermltl2rev  44261  sbgoldbo  44305  nnsum4primeseven  44318  nnsum4primesevenALTV  44319  wtgoldbnnsum4prm  44320  bgoldbnnsum3prm  44322  tgblthelfgott  44333  2zlidl  44558  2zrngALT  44572  nnpw2blen  44994