Theorem mpbir3an 1358

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

Syntax hints:   ↔ wb 209   ∧ w3a 1101

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 401  df-3an 1103

This theorem is referenced by:  3jaoi  1452  snopeqopsnid  5492  f1oi  6859  limon  7831  issmo  8334  xpider  8785  omina  10675  1eluzge0  12903  2eluzge1  12905  5eluz3  12906  0elunit  13495  1elunit  13496  fz0to3un2pr  13657  fz0to4untppr  13658  fz0to5un2tp  13659  4fvwrd4  13676  fzo0to42pr  13782  fvf1tp  13822  tpf1ofv1  14534  tpf1ofv2  14535  tpfo  14537  ccat2s1p2  14668  cats1fv  14896  pfx2  14984  wwlktovf  14993  fprodge0  16047  fprodge1  16049  sincos1sgn  16248  sincos2sgn  16249  divalglem7  16456  igz  16993  strleun  17216  strle1  17217  letsr  18648  psgnunilem2  19564  cnfldfun  21515  cnsubmlem  21544  cnsubglem  21545  cnsubrglem  21546  cnmsubglem  21559  nn0srg  21566  rge0srg  21567  xrge0subm  21572  xrge0omnd  21574  pzriprnglem4  21613  ust0  24356  cnngp  24915  cnfldtgp  25007  htpycc  25118  pco0  25152  pcocn  25155  pcohtpylem  25157  pcopt  25160  pcopt2  25161  pcoass  25162  pcorevlem  25164  sinhalfpilem  26604  sincos4thpi  26654  sincos6thpi  26657  logi  26728  argregt0  26751  argrege0  26752  elogb  26911  2logb9irr  26936  2logb9irrALT  26939  sqrt2cxp2logb9e3  26940  asin1  27035  atanbnd  27067  atan1  27069  harmonicbnd3  27148  ppiublem1  27342  zsoring  28578  usgrexmplef  29575  usgr2pthlem  30078  uspgrn2crct  30123  upgr3v3e3cycl  30497  upgr4cycl4dv4e  30502  konigsbergiedgw  30565  konigsberglem1  30569  konigsberglem2  30570  konigsberglem3  30571  konigsberglem4  30572  ex-opab  30749  isgrpoi  30816  isvciOLD  30898  isnvi  30931  adj1o  32212  bra11  32426  1fldgenq  33609  reofld  33629  xrge0slmod  33634  ccfldsrarelvec  34027  constrextdg2  34105  constrext2chnlem  34106  constrcon  34130  2sqr3minply  34136  cos9thpiminply  34144  unitssxrge0  34256  iistmd  34258  mhmhmeotmd  34283  xrge0tmdALT  34302  rerrext  34365  cnrrext  34366  volmeas  34587  ddemeas  34592  fib1  34756  ballotlem2  34845  ballotth  34894  prodfzo03  34956  bj-pinftyccb  37831  fdc  38362  riscer  38605  asin1half  43086  acos1half  43087  readvrec2  43090  jm2.27dlem2  43707  arearect  43912  areaquad  43913  onsucf1o  43969  lhe4.4ex1a  45009  wallispilem4  46752  fourierdlem20  46811  fourierdlem62  46852  fourierdlem104  46894  fourierdlem111  46901  sqwvfoura  46912  sqwvfourb  46913  fouriersw  46915  goldrapos  47587  fmtnoprmfac2lem1  48285  fmtno4prmfac  48291  31prm  48316  nprmdvdsfacm1lem4  48342  nprmdvdsfacm1  48343  ppivalnnnprmge6  48345  341fppr2  48466  4fppr1  48467  9fppr8  48469  nfermltl8rev  48474  nfermltl2rev  48475  sbgoldbo  48519  nnsum4primeseven  48532  nnsum4primesevenALTV  48533  wtgoldbnnsum4prm  48534  bgoldbnnsum3prm  48536  tgblthelfgott  48547  cycl3grtri  48679  usgrexmpl1lem  48753  usgrexmpl2lem  48758  usgrexmpl2trifr  48769  gpg5nbgrvtx13starlem2  48804  gpg5nbgr3star  48813  gpg5edgnedg  48862  grlimedgnedg  48863  2zlidl  48972  2zrngALT  48986  nnpw2blen  49327