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  5469  limon  7811  issmo  8317  xpider  8761  omina  10644  1eluzge0  12839  2eluzge1  12841  5eluz3  12842  0elunit  13430  1elunit  13431  fz0to3un2pr  13590  fz0to4untppr  13591  fz0to5un2tp  13592  4fvwrd4  13609  fzo0to42pr  13714  fvf1tp  13751  tpf1ofv1  14462  tpf1ofv2  14463  tpfo  14465  ccat2s1p2  14595  cats1fv  14825  pfx2  14913  wwlktovf  14922  fprodge0  15959  fprodge1  15961  sincos1sgn  16161  sincos2sgn  16162  divalglem7  16369  igz  16905  strleun  17127  strle1  17128  letsr  18552  psgnunilem2  19425  cnfldfun  21278  cnfldfunOLD  21291  xrge0subm  21324  cnsubmlem  21331  cnsubglem  21332  cnsubrglem  21333  cnsubrglemOLD  21334  cnmsubglem  21347  nn0srg  21354  rge0srg  21355  pzriprnglem4  21394  ust0  24107  cnngp  24667  cnfldtgp  24760  htpycc  24879  pco0  24914  pcocn  24917  pcohtpylem  24919  pcopt  24922  pcopt2  24923  pcoass  24924  pcorevlem  24926  sinhalfpilem  26372  sincos4thpi  26422  sincos6thpi  26425  logi  26496  argregt0  26519  argrege0  26520  elogb  26680  2logb9irr  26705  2logb9irrALT  26708  sqrt2cxp2logb9e3  26709  asin1  26804  atanbnd  26836  atan1  26838  harmonicbnd3  26918  ppiublem1  27113  usgrexmplef  29186  usgr2pthlem  29693  uspgrn2crct  29738  upgr3v3e3cycl  30109  upgr4cycl4dv4e  30114  konigsbergiedgw  30177  konigsberglem1  30181  konigsberglem2  30182  konigsberglem3  30183  konigsberglem4  30184  ex-opab  30361  isgrpoi  30427  isvciOLD  30509  isnvi  30542  adj1o  31823  bra11  32037  xrge0omnd  33025  1fldgenq  33272  reofld  33315  xrge0slmod  33319  ccfldsrarelvec  33666  constrextdg2  33739  constrext2chnlem  33740  constrcon  33764  2sqr3minply  33770  cos9thpiminply  33778  unitssxrge0  33890  iistmd  33892  mhmhmeotmd  33917  xrge0tmdALT  33936  rerrext  33999  cnrrext  34000  volmeas  34221  ddemeas  34226  fib1  34391  ballotlem2  34480  ballotth  34529  prodfzo03  34594  bj-pinftyccb  37209  fdc  37739  riscer  37982  asin1half  42345  acos1half  42346  readvrec2  42349  jm2.27dlem2  42999  arearect  43204  areaquad  43205  onsucf1o  43261  lhe4.4ex1a  44318  wallispilem4  46066  fourierdlem20  46125  fourierdlem62  46166  fourierdlem104  46208  fourierdlem111  46215  sqwvfoura  46226  sqwvfourb  46227  fouriersw  46229  tworepnotupword  46884  fmtnoprmfac2lem1  47567  fmtno4prmfac  47573  31prm  47598  341fppr2  47735  4fppr1  47736  9fppr8  47738  nfermltl8rev  47743  nfermltl2rev  47744  sbgoldbo  47788  nnsum4primeseven  47801  nnsum4primesevenALTV  47802  wtgoldbnnsum4prm  47803  bgoldbnnsum3prm  47805  tgblthelfgott  47816  cycl3grtri  47946  usgrexmpl1lem  48012  usgrexmpl2lem  48017  usgrexmpl2trifr  48028  gpg5nbgrvtx13starlem2  48063  gpg5nbgr3star  48072  2zlidl  48228  2zrngALT  48242  nnpw2blen  48569