Theorem mpbir3an 1351

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

Syntax hints:   ↔ wb 208   ∧ w3a 1095

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 209  df-an 399  df-3an 1097

This theorem is referenced by:  snopeqopsnid  5472  f1oi  6834  limon  7805  issmo  8307  xpider  8758  omina  10639  1eluzge0  12871  2eluzge1  12873  5eluz3  12874  0elunit  13463  1elunit  13464  fz0to3un2pr  13624  fz0to4untppr  13625  fz0to5un2tp  13626  4fvwrd4  13643  fzo0to42pr  13749  fvf1tp  13789  tpf1ofv1  14500  tpf1ofv2  14501  tpfo  14503  ccat2s1p2  14634  cats1fv  14862  pfx2  14950  wwlktovf  14959  fprodge0  15999  fprodge1  16001  sincos1sgn  16201  sincos2sgn  16202  divalglem7  16409  igz  16946  strleun  17169  strle1  17170  letsr  18601  psgnunilem2  19511  cnfldfun  21411  cnsubmlem  21440  cnsubglem  21441  cnsubrglem  21442  cnmsubglem  21455  nn0srg  21462  rge0srg  21463  xrge0subm  21468  xrge0omnd  21470  pzriprnglem4  21509  ust0  24253  cnngp  24812  cnfldtgp  24904  htpycc  25015  pco0  25049  pcocn  25052  pcohtpylem  25054  pcopt  25057  pcopt2  25058  pcoass  25059  pcorevlem  25061  sinhalfpilem  26498  sincos4thpi  26548  sincos6thpi  26551  logi  26622  argregt0  26645  argrege0  26646  elogb  26805  2logb9irr  26830  2logb9irrALT  26833  sqrt2cxp2logb9e3  26834  asin1  26929  atanbnd  26961  atan1  26963  harmonicbnd3  27042  ppiublem1  27236  zsoring  28472  usgrexmplef  29399  usgr2pthlem  29902  uspgrn2crct  29947  upgr3v3e3cycl  30321  upgr4cycl4dv4e  30326  konigsbergiedgw  30389  konigsberglem1  30393  konigsberglem2  30394  konigsberglem3  30395  konigsberglem4  30396  ex-opab  30573  isgrpoi  30640  isvciOLD  30722  isnvi  30755  adj1o  32036  bra11  32250  1fldgenq  33463  reofld  33483  xrge0slmod  33488  ccfldsrarelvec  33922  constrextdg2  34000  constrext2chnlem  34001  constrcon  34025  2sqr3minply  34031  cos9thpiminply  34039  unitssxrge0  34151  iistmd  34153  mhmhmeotmd  34178  xrge0tmdALT  34197  rerrext  34260  cnrrext  34261  volmeas  34482  ddemeas  34487  fib1  34651  ballotlem2  34740  ballotth  34789  prodfzo03  34854  bj-pinftyccb  37661  fdc  38192  riscer  38435  asin1half  42914  acos1half  42915  readvrec2  42918  jm2.27dlem2  43535  arearect  43740  areaquad  43741  onsucf1o  43797  lhe4.4ex1a  44853  wallispilem4  46590  fourierdlem20  46649  fourierdlem62  46690  fourierdlem104  46732  fourierdlem111  46739  sqwvfoura  46750  sqwvfourb  46751  fouriersw  46753  goldrapos  47425  fmtnoprmfac2lem1  48123  fmtno4prmfac  48129  31prm  48154  nprmdvdsfacm1lem4  48180  nprmdvdsfacm1  48181  ppivalnnnprmge6  48183  341fppr2  48304  4fppr1  48305  9fppr8  48307  nfermltl8rev  48312  nfermltl2rev  48313  sbgoldbo  48357  nnsum4primeseven  48370  nnsum4primesevenALTV  48371  wtgoldbnnsum4prm  48372  bgoldbnnsum3prm  48374  tgblthelfgott  48385  cycl3grtri  48517  usgrexmpl1lem  48591  usgrexmpl2lem  48596  usgrexmpl2trifr  48607  gpg5nbgrvtx13starlem2  48642  gpg5nbgr3star  48651  gpg5edgnedg  48700  grlimedgnedg  48701  2zlidl  48810  2zrngALT  48824  nnpw2blen  49150