Theorem mpbir3an 1342

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

Syntax hints:   ↔ wb 206   ∧ w3a 1086

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 1088

This theorem is referenced by:  snopeqopsnid  5447  limon  7761  issmo  8263  xpider  8707  omina  10574  1eluzge0  12770  2eluzge1  12772  5eluz3  12773  0elunit  13361  1elunit  13362  fz0to3un2pr  13521  fz0to4untppr  13522  fz0to5un2tp  13523  4fvwrd4  13540  fzo0to42pr  13645  fvf1tp  13685  tpf1ofv1  14396  tpf1ofv2  14397  tpfo  14399  ccat2s1p2  14530  cats1fv  14758  pfx2  14846  wwlktovf  14855  fprodge0  15892  fprodge1  15894  sincos1sgn  16094  sincos2sgn  16095  divalglem7  16302  igz  16838  strleun  17060  strle1  17061  letsr  18491  psgnunilem2  19400  cnfldfun  21298  cnfldfunOLD  21311  cnsubmlem  21344  cnsubglem  21345  cnsubrglem  21346  cnsubrglemOLD  21347  cnmsubglem  21360  nn0srg  21367  rge0srg  21368  xrge0subm  21373  xrge0omnd  21375  pzriprnglem4  21414  ust0  24128  cnngp  24687  cnfldtgp  24780  htpycc  24899  pco0  24934  pcocn  24937  pcohtpylem  24939  pcopt  24942  pcopt2  24943  pcoass  24944  pcorevlem  24946  sinhalfpilem  26392  sincos4thpi  26442  sincos6thpi  26445  logi  26516  argregt0  26539  argrege0  26540  elogb  26700  2logb9irr  26725  2logb9irrALT  26728  sqrt2cxp2logb9e3  26729  asin1  26824  atanbnd  26856  atan1  26858  harmonicbnd3  26938  ppiublem1  27133  zsoring  28325  usgrexmplef  29230  usgr2pthlem  29734  uspgrn2crct  29779  upgr3v3e3cycl  30150  upgr4cycl4dv4e  30155  konigsbergiedgw  30218  konigsberglem1  30222  konigsberglem2  30223  konigsberglem3  30224  konigsberglem4  30225  ex-opab  30402  isgrpoi  30468  isvciOLD  30550  isnvi  30583  adj1o  31864  bra11  32078  1fldgenq  33278  reofld  33298  xrge0slmod  33303  ccfldsrarelvec  33674  constrextdg2  33752  constrext2chnlem  33753  constrcon  33777  2sqr3minply  33783  cos9thpiminply  33791  unitssxrge0  33903  iistmd  33905  mhmhmeotmd  33930  xrge0tmdALT  33949  rerrext  34012  cnrrext  34013  volmeas  34234  ddemeas  34239  fib1  34403  ballotlem2  34492  ballotth  34541  prodfzo03  34606  bj-pinftyccb  37234  fdc  37764  riscer  38007  asin1half  42369  acos1half  42370  readvrec2  42373  jm2.27dlem2  43022  arearect  43227  areaquad  43228  onsucf1o  43284  lhe4.4ex1a  44341  wallispilem4  46085  fourierdlem20  46144  fourierdlem62  46185  fourierdlem104  46227  fourierdlem111  46234  sqwvfoura  46245  sqwvfourb  46246  fouriersw  46248  fmtnoprmfac2lem1  47576  fmtno4prmfac  47582  31prm  47607  341fppr2  47744  4fppr1  47745  9fppr8  47747  nfermltl8rev  47752  nfermltl2rev  47753  sbgoldbo  47797  nnsum4primeseven  47810  nnsum4primesevenALTV  47811  wtgoldbnnsum4prm  47812  bgoldbnnsum3prm  47814  tgblthelfgott  47825  cycl3grtri  47957  usgrexmpl1lem  48031  usgrexmpl2lem  48036  usgrexmpl2trifr  48047  gpg5nbgrvtx13starlem2  48082  gpg5nbgr3star  48091  gpg5edgnedg  48140  grlimedgnedg  48141  2zlidl  48250  2zrngALT  48264  nnpw2blen  48591