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  5454  f1oi  6809  limon  7775  issmo  8277  xpider  8721  omina  10592  1eluzge0  12788  2eluzge1  12790  5eluz3  12791  0elunit  13379  1elunit  13380  fz0to3un2pr  13539  fz0to4untppr  13540  fz0to5un2tp  13541  4fvwrd4  13558  fzo0to42pr  13663  fvf1tp  13703  tpf1ofv1  14414  tpf1ofv2  14415  tpfo  14417  ccat2s1p2  14548  cats1fv  14776  pfx2  14864  wwlktovf  14873  fprodge0  15910  fprodge1  15912  sincos1sgn  16112  sincos2sgn  16113  divalglem7  16320  igz  16856  strleun  17078  strle1  17079  letsr  18509  psgnunilem2  19417  cnfldfun  21315  cnfldfunOLD  21328  cnsubmlem  21361  cnsubglem  21362  cnsubrglem  21363  cnsubrglemOLD  21364  cnmsubglem  21377  nn0srg  21384  rge0srg  21385  xrge0subm  21390  xrge0omnd  21392  pzriprnglem4  21431  ust0  24145  cnngp  24704  cnfldtgp  24797  htpycc  24916  pco0  24951  pcocn  24954  pcohtpylem  24956  pcopt  24959  pcopt2  24960  pcoass  24961  pcorevlem  24963  sinhalfpilem  26409  sincos4thpi  26459  sincos6thpi  26462  logi  26533  argregt0  26556  argrege0  26557  elogb  26717  2logb9irr  26742  2logb9irrALT  26745  sqrt2cxp2logb9e3  26746  asin1  26841  atanbnd  26873  atan1  26875  harmonicbnd3  26955  ppiublem1  27150  zsoring  28342  usgrexmplef  29248  usgr2pthlem  29752  uspgrn2crct  29797  upgr3v3e3cycl  30171  upgr4cycl4dv4e  30176  konigsbergiedgw  30239  konigsberglem1  30243  konigsberglem2  30244  konigsberglem3  30245  konigsberglem4  30246  ex-opab  30423  isgrpoi  30489  isvciOLD  30571  isnvi  30604  adj1o  31885  bra11  32099  1fldgenq  33299  reofld  33319  xrge0slmod  33324  ccfldsrarelvec  33695  constrextdg2  33773  constrext2chnlem  33774  constrcon  33798  2sqr3minply  33804  cos9thpiminply  33812  unitssxrge0  33924  iistmd  33926  mhmhmeotmd  33951  xrge0tmdALT  33970  rerrext  34033  cnrrext  34034  volmeas  34255  ddemeas  34260  fib1  34424  ballotlem2  34513  ballotth  34562  prodfzo03  34627  bj-pinftyccb  37276  fdc  37795  riscer  38038  asin1half  42465  acos1half  42466  readvrec2  42469  jm2.27dlem2  43117  arearect  43322  areaquad  43323  onsucf1o  43379  lhe4.4ex1a  44436  wallispilem4  46180  fourierdlem20  46239  fourierdlem62  46280  fourierdlem104  46322  fourierdlem111  46329  sqwvfoura  46340  sqwvfourb  46341  fouriersw  46343  fmtnoprmfac2lem1  47680  fmtno4prmfac  47686  31prm  47711  341fppr2  47848  4fppr1  47849  9fppr8  47851  nfermltl8rev  47856  nfermltl2rev  47857  sbgoldbo  47901  nnsum4primeseven  47914  nnsum4primesevenALTV  47915  wtgoldbnnsum4prm  47916  bgoldbnnsum3prm  47918  tgblthelfgott  47929  cycl3grtri  48061  usgrexmpl1lem  48135  usgrexmpl2lem  48140  usgrexmpl2trifr  48151  gpg5nbgrvtx13starlem2  48186  gpg5nbgr3star  48195  gpg5edgnedg  48244  grlimedgnedg  48245  2zlidl  48354  2zrngALT  48368  nnpw2blen  48695