Theorem mpbir3an 1360

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3jaoi  1454  snopeqopsnid  5490  f1oi  6860  limon  7835  issmo  8340  xpider  8791  omina  10703  1eluzge0  12932  2eluzge1  12934  5eluz3  12935  0elunit  13524  1elunit  13525  fz0to3un2pr  13686  fz0to4untppr  13687  fz0to5un2tp  13688  4fvwrd4  13705  fzo0to42pr  13811  fvf1tp  13852  tpf1ofv1  14564  tpf1ofv2  14565  tpfo  14567  ccat2s1p2  14700  cats1fv  14932  pfx2  15020  wwlktovf  15031  fprodge0  16084  fprodge1  16086  sincos1sgn  16285  sincos2sgn  16286  divalglem7  16493  igz  17030  strleun  17253  strle1  17254  letsr  18685  psgnunilem2  19626  cnfldfun  21603  cnsubmlem  21632  cnsubglem  21633  cnsubrglem  21634  cnmsubglem  21647  nn0srg  21654  rge0srg  21655  xrge0subm  21660  xrge0omnd  21662  pzriprnglem4  21701  ust0  24450  cnngp  25009  cnfldtgp  25101  htpycc  25212  pco0  25246  pcocn  25249  pcohtpylem  25251  pcopt  25254  pcopt2  25255  pcoass  25256  pcorevlem  25258  sinhalfpilem  26701  sincos4thpi  26751  sincos6thpi  26754  logi  26825  argregt0  26848  argrege0  26849  elogb  27008  2logb9irr  27033  2logb9irrALT  27036  sqrt2cxp2logb9e3  27037  asin1  27132  atanbnd  27164  atan1  27166  harmonicbnd3  27245  ppiublem1  27439  zsoring  28675  usgrexmplef  29720  usgr2pthlem  30229  uspgrn2crct  30277  upgr3v3e3cycl  30661  upgr4cycl4dv4e  30666  konigsbergiedgw  30729  konigsberglem1  30733  konigsberglem2  30734  konigsberglem3  30735  konigsberglem4  30736  ex-opab  30913  isgrpoi  30980  isvciOLD  31062  isnvi  31095  adj1o  32376  bra11  32590  1fldgenq  33765  reofld  33785  xrge0slmod  33790  ccfldsrarelvec  34183  constrextdg2  34261  constrext2chnlem  34262  constrcon  34286  2sqr3minply  34292  cos9thpiminply  34300  unitssxrge0  34412  iistmd  34414  mhmhmeotmd  34439  xrge0tmdALT  34458  rerrext  34521  cnrrext  34522  volmeas  34744  ddemeas  34749  fib1  34913  ballotlem2  35002  ballotth  35051  prodfzo03  35113  bj-pinftyccb  37975  fdc  38497  riscer  38740  asin1half  43234  acos1half  43235  readvrec2  43238  jm2.27dlem2  43853  arearect  44058  areaquad  44059  onsucf1o  44115  lhe4.4ex1a  45155  wallispilem4  46898  fourierdlem20  46957  fourierdlem62  46998  fourierdlem104  47040  fourierdlem111  47047  sqwvfoura  47058  sqwvfourb  47059  fouriersw  47061  goldrapos  47750  fmtnoprmfac2lem1  48471  fmtno4prmfac  48477  31prm  48502  nprmdvdsfacm1lem4  48528  nprmdvdsfacm1  48529  ppivalnnnprmge6  48531  341fppr2  48652  4fppr1  48653  9fppr8  48655  nfermltl8rev  48660  nfermltl2rev  48661  sbgoldbo  48705  nnsum4primeseven  48718  nnsum4primesevenALTV  48719  wtgoldbnnsum4prm  48720  bgoldbnnsum3prm  48722  tgblthelfgott  48733  cycl3grtri  48865  usgrexmpl1lem  48939  usgrexmpl2lem  48944  usgrexmpl2trifr  48955  gpg5nbgrvtx13starlem2  48990  gpg5nbgr3star  48999  gpg5edgnedg  49048  grlimedgnedg  49049  2zlidl  49157  2zrngALT  49171  nnpw2blen  49512  1elfz13  50778  2elfz13  50779  veronesevrowd  50814  veronesematrowd  50816  veroquadgsumlem  50818  veroquadmodzerod  50819  veroquadnolindfd  50820