Theorem mpbir3an 1342

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

Syntax hints:   ↔ wb 206   ∧ 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  snopeqopsnid  5472  limon  7814  issmo  8320  xpider  8764  omina  10651  1eluzge0  12846  2eluzge1  12848  5eluz3  12849  0elunit  13437  1elunit  13438  fz0to3un2pr  13597  fz0to4untppr  13598  fz0to5un2tp  13599  4fvwrd4  13616  fzo0to42pr  13721  fvf1tp  13758  tpf1ofv1  14469  tpf1ofv2  14470  tpfo  14472  ccat2s1p2  14602  cats1fv  14832  pfx2  14920  wwlktovf  14929  fprodge0  15966  fprodge1  15968  sincos1sgn  16168  sincos2sgn  16169  divalglem7  16376  igz  16912  strleun  17134  strle1  17135  letsr  18559  psgnunilem2  19432  cnfldfun  21285  cnfldfunOLD  21298  xrge0subm  21331  cnsubmlem  21338  cnsubglem  21339  cnsubrglem  21340  cnsubrglemOLD  21341  cnmsubglem  21354  nn0srg  21361  rge0srg  21362  pzriprnglem4  21401  ust0  24114  cnngp  24674  cnfldtgp  24767  htpycc  24886  pco0  24921  pcocn  24924  pcohtpylem  24926  pcopt  24929  pcopt2  24930  pcoass  24931  pcorevlem  24933  sinhalfpilem  26379  sincos4thpi  26429  sincos6thpi  26432  logi  26503  argregt0  26526  argrege0  26527  elogb  26687  2logb9irr  26712  2logb9irrALT  26715  sqrt2cxp2logb9e3  26716  asin1  26811  atanbnd  26843  atan1  26845  harmonicbnd3  26925  ppiublem1  27120  usgrexmplef  29193  usgr2pthlem  29700  uspgrn2crct  29745  upgr3v3e3cycl  30116  upgr4cycl4dv4e  30121  konigsbergiedgw  30184  konigsberglem1  30188  konigsberglem2  30189  konigsberglem3  30190  konigsberglem4  30191  ex-opab  30368  isgrpoi  30434  isvciOLD  30516  isnvi  30549  adj1o  31830  bra11  32044  xrge0omnd  33032  1fldgenq  33279  reofld  33322  xrge0slmod  33326  ccfldsrarelvec  33673  constrextdg2  33746  constrext2chnlem  33747  constrcon  33771  2sqr3minply  33777  cos9thpiminply  33785  unitssxrge0  33897  iistmd  33899  mhmhmeotmd  33924  xrge0tmdALT  33943  rerrext  34006  cnrrext  34007  volmeas  34228  ddemeas  34233  fib1  34398  ballotlem2  34487  ballotth  34536  prodfzo03  34601  bj-pinftyccb  37216  fdc  37746  riscer  37989  asin1half  42352  acos1half  42353  readvrec2  42356  jm2.27dlem2  43006  arearect  43211  areaquad  43212  onsucf1o  43268  lhe4.4ex1a  44325  wallispilem4  46073  fourierdlem20  46132  fourierdlem62  46173  fourierdlem104  46215  fourierdlem111  46222  sqwvfoura  46233  sqwvfourb  46234  fouriersw  46236  tworepnotupword  46891  fmtnoprmfac2lem1  47571  fmtno4prmfac  47577  31prm  47602  341fppr2  47739  4fppr1  47740  9fppr8  47742  nfermltl8rev  47747  nfermltl2rev  47748  sbgoldbo  47792  nnsum4primeseven  47805  nnsum4primesevenALTV  47806  wtgoldbnnsum4prm  47807  bgoldbnnsum3prm  47809  tgblthelfgott  47820  cycl3grtri  47950  usgrexmpl1lem  48016  usgrexmpl2lem  48021  usgrexmpl2trifr  48032  gpg5nbgrvtx13starlem2  48067  gpg5nbgr3star  48076  2zlidl  48232  2zrngALT  48246  nnpw2blen  48573