Theorem mpbir3an 1337

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

Syntax hints:   ↔ wb 208   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  snopeqopsnid  5398  limon  7550  issmo  7984  xpider  8367  omina  10112  1eluzge0  12291  2eluzge1  12293  0elunit  12854  1elunit  12855  fz0to3un2pr  13008  4fvwrd4  13026  fzo0to42pr  13123  ccat2s1p2  13985  ccat2s1p2OLD  13987  cats1fv  14220  pfx2  14308  wwlktovf  14319  fprodge0  15346  fprodge1  15348  sincos1sgn  15545  sincos2sgn  15546  divalglem7  15749  igz  16269  strleun  16590  strle1  16591  letsr  17836  psgnunilem2  18622  cnfldfunALT  20557  xrge0subm  20585  cnsubmlem  20592  cnsubglem  20593  cnsubrglem  20594  cnmsubglem  20607  nn0srg  20614  rge0srg  20615  ust0  22827  cnngp  23387  cnfldtgp  23476  htpycc  23583  pco0  23617  pcocn  23620  pcohtpylem  23622  pcopt  23625  pcopt2  23626  pcoass  23627  pcorevlem  23629  sinhalfpilem  25048  sincos4thpi  25098  sincos6thpi  25100  argregt0  25192  argrege0  25193  elogb  25347  2logb9irr  25372  2logb9irrALT  25375  sqrt2cxp2logb9e3  25376  asin1  25471  atanbnd  25503  atan1  25505  harmonicbnd3  25584  ppiublem1  25777  usgrexmplef  27040  usgr2pthlem  27543  uspgrn2crct  27585  upgr3v3e3cycl  27958  upgr4cycl4dv4e  27963  konigsbergiedgw  28026  konigsberglem1  28030  konigsberglem2  28031  konigsberglem3  28032  konigsberglem4  28033  ex-opab  28210  isgrpoi  28274  isvciOLD  28356  isnvi  28389  adj1o  29670  bra11  29884  xrge0omnd  30712  reofld  30913  xrge0slmod  30917  ccfldsrarelvec  31056  unitssxrge0  31143  iistmd  31145  mhmhmeotmd  31170  xrge0tmdALT  31189  rerrext  31250  cnrrext  31251  volmeas  31490  ddemeas  31495  fib1  31658  ballotlem2  31746  ballotth  31795  prodfzo03  31874  logi  32966  bj-pinftyccb  34502  fdc  35019  riscer  35265  jm2.27dlem2  39605  arearect  39820  areaquad  39821  lhe4.4ex1a  40659  wallispilem4  42352  fourierdlem20  42411  fourierdlem62  42452  fourierdlem104  42494  fourierdlem111  42501  sqwvfoura  42512  sqwvfourb  42513  fouriersw  42515  fmtnoprmfac2lem1  43727  fmtno4prmfac  43733  31prm  43759  341fppr2  43898  4fppr1  43899  9fppr8  43901  nfermltl8rev  43906  nfermltl2rev  43907  sbgoldbo  43951  nnsum4primeseven  43964  nnsum4primesevenALTV  43965  wtgoldbnnsum4prm  43966  bgoldbnnsum3prm  43968  tgblthelfgott  43979  2zlidl  44204  2zrngALT  44218  nnpw2blen  44639