Theorem mpbir3an 1343

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

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

This theorem is referenced by:  snopeqopsnid  5458  f1oi  6813  limon  7780  issmo  8282  xpider  8729  omina  10606  1eluzge0  12797  2eluzge1  12799  5eluz3  12800  0elunit  13389  1elunit  13390  fz0to3un2pr  13549  fz0to4untppr  13550  fz0to5un2tp  13551  4fvwrd4  13568  fzo0to42pr  13673  fvf1tp  13713  tpf1ofv1  14424  tpf1ofv2  14425  tpfo  14427  ccat2s1p2  14558  cats1fv  14786  pfx2  14874  wwlktovf  14883  fprodge0  15920  fprodge1  15922  sincos1sgn  16122  sincos2sgn  16123  divalglem7  16330  igz  16866  strleun  17088  strle1  17089  letsr  18520  psgnunilem2  19428  cnfldfun  21327  cnfldfunOLD  21340  cnsubmlem  21373  cnsubglem  21374  cnsubrglem  21375  cnsubrglemOLD  21376  cnmsubglem  21389  nn0srg  21396  rge0srg  21397  xrge0subm  21402  xrge0omnd  21404  pzriprnglem4  21443  ust0  24168  cnngp  24727  cnfldtgp  24820  htpycc  24939  pco0  24974  pcocn  24977  pcohtpylem  24979  pcopt  24982  pcopt2  24983  pcoass  24984  pcorevlem  24986  sinhalfpilem  26432  sincos4thpi  26482  sincos6thpi  26485  logi  26556  argregt0  26579  argrege0  26580  elogb  26740  2logb9irr  26765  2logb9irrALT  26768  sqrt2cxp2logb9e3  26769  asin1  26864  atanbnd  26896  atan1  26898  harmonicbnd3  26978  ppiublem1  27173  zsoring  28388  usgrexmplef  29315  usgr2pthlem  29819  uspgrn2crct  29864  upgr3v3e3cycl  30238  upgr4cycl4dv4e  30243  konigsbergiedgw  30306  konigsberglem1  30310  konigsberglem2  30311  konigsberglem3  30312  konigsberglem4  30313  ex-opab  30490  isgrpoi  30556  isvciOLD  30638  isnvi  30671  adj1o  31952  bra11  32166  1fldgenq  33385  reofld  33405  xrge0slmod  33410  ccfldsrarelvec  33809  constrextdg2  33887  constrext2chnlem  33888  constrcon  33912  2sqr3minply  33918  cos9thpiminply  33926  unitssxrge0  34038  iistmd  34040  mhmhmeotmd  34065  xrge0tmdALT  34084  rerrext  34147  cnrrext  34148  volmeas  34369  ddemeas  34374  fib1  34538  ballotlem2  34627  ballotth  34676  prodfzo03  34741  bj-pinftyccb  37397  fdc  37917  riscer  38160  asin1half  42648  acos1half  42649  readvrec2  42652  jm2.27dlem2  43288  arearect  43493  areaquad  43494  onsucf1o  43550  lhe4.4ex1a  44606  wallispilem4  46348  fourierdlem20  46407  fourierdlem62  46448  fourierdlem104  46490  fourierdlem111  46497  sqwvfoura  46508  sqwvfourb  46509  fouriersw  46511  fmtnoprmfac2lem1  47848  fmtno4prmfac  47854  31prm  47879  341fppr2  48016  4fppr1  48017  9fppr8  48019  nfermltl8rev  48024  nfermltl2rev  48025  sbgoldbo  48069  nnsum4primeseven  48082  nnsum4primesevenALTV  48083  wtgoldbnnsum4prm  48084  bgoldbnnsum3prm  48086  tgblthelfgott  48097  cycl3grtri  48229  usgrexmpl1lem  48303  usgrexmpl2lem  48308  usgrexmpl2trifr  48319  gpg5nbgrvtx13starlem2  48354  gpg5nbgr3star  48363  gpg5edgnedg  48412  grlimedgnedg  48413  2zlidl  48522  2zrngALT  48536  nnpw2blen  48862