Theorem mpbir3an 1341

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

Syntax hints:   ↔ wb 205   ∧ w3a 1087

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 1089

This theorem is referenced by:  snopeqopsnid  5509  limon  7826  issmo  8350  xpider  8784  omina  10688  1eluzge0  12878  2eluzge1  12880  0elunit  13448  1elunit  13449  fz0to3un2pr  13605  4fvwrd4  13623  fzo0to42pr  13721  ccat2s1p2  14582  cats1fv  14812  pfx2  14900  wwlktovf  14909  fprodge0  15939  fprodge1  15941  sincos1sgn  16138  sincos2sgn  16139  divalglem7  16344  igz  16869  strleun  17092  strle1  17093  letsr  18548  psgnunilem2  19365  cnfldfun  20962  xrge0subm  20992  cnsubmlem  20999  cnsubglem  21000  cnsubrglem  21001  cnmsubglem  21014  nn0srg  21021  rge0srg  21022  ust0  23731  cnngp  24303  cnfldtgp  24392  htpycc  24503  pco0  24537  pcocn  24540  pcohtpylem  24542  pcopt  24545  pcopt2  24546  pcoass  24547  pcorevlem  24549  sinhalfpilem  25980  sincos4thpi  26030  sincos6thpi  26032  argregt0  26125  argrege0  26126  elogb  26282  2logb9irr  26307  2logb9irrALT  26310  sqrt2cxp2logb9e3  26311  asin1  26406  atanbnd  26438  atan1  26440  harmonicbnd3  26519  ppiublem1  26712  usgrexmplef  28554  usgr2pthlem  29058  uspgrn2crct  29100  upgr3v3e3cycl  29471  upgr4cycl4dv4e  29476  konigsbergiedgw  29539  konigsberglem1  29543  konigsberglem2  29544  konigsberglem3  29545  konigsberglem4  29546  ex-opab  29723  isgrpoi  29789  isvciOLD  29871  isnvi  29904  adj1o  31185  bra11  31399  xrge0omnd  32270  1fldgenq  32453  reofld  32500  xrge0slmod  32504  ccfldsrarelvec  32805  unitssxrge0  32949  iistmd  32951  mhmhmeotmd  32976  xrge0tmdALT  32995  rerrext  33058  cnrrext  33059  volmeas  33298  ddemeas  33303  fib1  33468  ballotlem2  33556  ballotth  33605  prodfzo03  33684  logi  34773  gg-cnfldfun  35266  bj-pinftyccb  36188  fdc  36699  riscer  36942  acos1half  41497  jm2.27dlem2  41831  arearect  42046  areaquad  42047  onsucf1o  42104  lhe4.4ex1a  43170  wallispilem4  44863  fourierdlem20  44922  fourierdlem62  44963  fourierdlem104  45005  fourierdlem111  45012  sqwvfoura  45023  sqwvfourb  45024  fouriersw  45026  tworepnotupword  45679  fmtnoprmfac2lem1  46313  fmtno4prmfac  46319  31prm  46344  341fppr2  46481  4fppr1  46482  9fppr8  46484  nfermltl8rev  46489  nfermltl2rev  46490  sbgoldbo  46534  nnsum4primeseven  46547  nnsum4primesevenALTV  46548  wtgoldbnnsum4prm  46549  bgoldbnnsum3prm  46551  tgblthelfgott  46562  pzriprnglem4  46887  2zlidl  46911  2zrngALT  46925  nnpw2blen  47344