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  1450  snopeqopsnid  5483  f1oi  6849  limon  7820  issmo  8323  xpider  8774  omina  10664  1eluzge0  12895  2eluzge1  12897  5eluz3  12898  0elunit  13487  1elunit  13488  fz0to3un2pr  13648  fz0to4untppr  13649  fz0to5un2tp  13650  4fvwrd4  13667  fzo0to42pr  13773  fvf1tp  13813  tpf1ofv1  14524  tpf1ofv2  14525  tpfo  14527  ccat2s1p2  14658  cats1fv  14886  pfx2  14974  wwlktovf  14983  fprodge0  16037  fprodge1  16039  sincos1sgn  16239  sincos2sgn  16240  divalglem7  16447  igz  16984  strleun  17207  strle1  17208  letsr  18639  psgnunilem2  19556  cnfldfun  21496  cnsubmlem  21525  cnsubglem  21526  cnsubrglem  21527  cnmsubglem  21540  nn0srg  21547  rge0srg  21548  xrge0subm  21553  xrge0omnd  21555  pzriprnglem4  21594  ust0  24338  cnngp  24897  cnfldtgp  24989  htpycc  25100  pco0  25134  pcocn  25137  pcohtpylem  25139  pcopt  25142  pcopt2  25143  pcoass  25144  pcorevlem  25146  sinhalfpilem  26586  sincos4thpi  26636  sincos6thpi  26639  logi  26710  argregt0  26733  argrege0  26734  elogb  26893  2logb9irr  26918  2logb9irrALT  26921  sqrt2cxp2logb9e3  26922  asin1  27017  atanbnd  27049  atan1  27051  harmonicbnd3  27130  ppiublem1  27324  zsoring  28560  usgrexmplef  29518  usgr2pthlem  30021  uspgrn2crct  30066  upgr3v3e3cycl  30440  upgr4cycl4dv4e  30445  konigsbergiedgw  30508  konigsberglem1  30512  konigsberglem2  30513  konigsberglem3  30514  konigsberglem4  30515  ex-opab  30692  isgrpoi  30759  isvciOLD  30841  isnvi  30874  adj1o  32155  bra11  32369  1fldgenq  33558  reofld  33578  xrge0slmod  33583  ccfldsrarelvec  33978  constrextdg2  34056  constrext2chnlem  34057  constrcon  34081  2sqr3minply  34087  cos9thpiminply  34095  unitssxrge0  34207  iistmd  34209  mhmhmeotmd  34234  xrge0tmdALT  34253  rerrext  34316  cnrrext  34317  volmeas  34538  ddemeas  34543  fib1  34707  ballotlem2  34796  ballotth  34845  prodfzo03  34907  bj-pinftyccb  37725  fdc  38256  riscer  38499  asin1half  42978  acos1half  42979  readvrec2  42982  jm2.27dlem2  43599  arearect  43804  areaquad  43805  onsucf1o  43861  lhe4.4ex1a  44903  wallispilem4  46640  fourierdlem20  46699  fourierdlem62  46740  fourierdlem104  46782  fourierdlem111  46789  sqwvfoura  46800  sqwvfourb  46801  fouriersw  46803  goldrapos  47475  fmtnoprmfac2lem1  48173  fmtno4prmfac  48179  31prm  48204  nprmdvdsfacm1lem4  48230  nprmdvdsfacm1  48231  ppivalnnnprmge6  48233  341fppr2  48354  4fppr1  48355  9fppr8  48357  nfermltl8rev  48362  nfermltl2rev  48363  sbgoldbo  48407  nnsum4primeseven  48420  nnsum4primesevenALTV  48421  wtgoldbnnsum4prm  48422  bgoldbnnsum3prm  48424  tgblthelfgott  48435  cycl3grtri  48567  usgrexmpl1lem  48641  usgrexmpl2lem  48646  usgrexmpl2trifr  48657  gpg5nbgrvtx13starlem2  48692  gpg5nbgr3star  48701  gpg5edgnedg  48750  grlimedgnedg  48751  2zlidl  48860  2zrngALT  48874  nnpw2blen  49211