Theorem mpbir3an 1360

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3jaoi  1454  snopeqopsnid  5478  f1oi  6851  limon  7830  issmo  8334  xpider  8787  omina  10748  1eluzge0  12977  2eluzge1  12979  5eluz3  12980  0elunit  13570  1elunit  13571  fz0to3un2pr  13732  fz0to4untppr  13733  fz0to5un2tp  13734  4fvwrd4  13751  fzo0to42pr  13857  fvf1tp  13898  tpf1ofv1  14610  tpf1ofv2  14611  tpfo  14613  ccat2s1p2  14746  cats1fv  14978  pfx2  15066  wwlktovf  15077  fprodge0  16128  fprodge1  16130  sincos1sgn  16329  sincos2sgn  16330  divalglem7  16537  igz  17074  strleun  17297  strle1  17298  letsr  18729  psgnunilem2  19671  cnfldfun  21654  cnsubmlem  21683  cnsubglem  21684  cnsubrglem  21685  cnmsubglem  21698  nn0srg  21705  rge0srg  21706  xrge0subm  21711  xrge0omnd  21713  pzriprnglem4  21752  ust0  24501  cnngp  25060  cnfldtgp  25152  htpycc  25263  pco0  25297  pcocn  25300  pcohtpylem  25302  pcopt  25305  pcopt2  25306  pcoass  25307  pcorevlem  25309  sinhalfpilem  26756  sincos4thpi  26806  sincos6thpi  26808  logi  26879  argregt0  26902  argrege0  26903  elogb  27062  2logb9irr  27087  2logb9irrALT  27090  sqrt2cxp2logb9e3  27091  asin1  27186  atanbnd  27218  atan1  27220  harmonicbnd3  27299  ppiublem1  27493  zsoring  28729  usgrexmplef  29774  usgr2pthlem  30283  uspgrn2crct  30331  upgr3v3e3cycl  30715  upgr4cycl4dv4e  30720  konigsbergiedgw  30783  konigsberglem1  30787  konigsberglem2  30788  konigsberglem3  30789  konigsberglem4  30790  ex-opab  30967  isgrpoi  31034  isvciOLD  31116  isnvi  31149  adj1o  32430  bra11  32644  1fldgenq  33818  reofld  33838  xrge0slmod  33843  ccfldsrarelvec  34237  constrextdg2  34315  constrext2chnlem  34316  constrcon  34340  2sqr3minply  34346  cos9thpiminply  34354  unitssxrge0  34466  iistmd  34468  mhmhmeotmd  34493  xrge0tmdALT  34512  rerrext  34575  cnrrext  34576  volmeas  34798  ddemeas  34803  fib1  34967  ballotlem2  35056  ballotth  35105  prodfzo03  35167  bj-pinftyccb  38062  fdc  38599  riscer  38842  asin1half  43336  acos1half  43337  readvrec2  43340  jm2.27dlem2  43955  arearect  44160  areaquad  44161  onsucf1o  44217  lhe4.4ex1a  45257  wallispilem4  47000  fourierdlem20  47059  fourierdlem62  47100  fourierdlem104  47142  fourierdlem111  47149  sqwvfoura  47160  sqwvfourb  47161  fouriersw  47163  goldrapos  47852  fmtnoprmfac2lem1  48573  fmtno4prmfac  48579  31prm  48604  nprmdvdsfacm1lem4  48630  nprmdvdsfacm1  48631  ppivalnnnprmge6  48633  341fppr2  48754  4fppr1  48755  9fppr8  48757  nfermltl8rev  48762  nfermltl2rev  48763  sbgoldbo  48807  nnsum4primeseven  48820  nnsum4primesevenALTV  48821  wtgoldbnnsum4prm  48822  bgoldbnnsum3prm  48824  tgblthelfgott  48835  cycl3grtri  48967  usgrexmpl1lem  49041  usgrexmpl2lem  49046  usgrexmpl2trifr  49057  gpg5nbgrvtx13starlem2  49092  gpg5nbgr3star  49101  gpg5edgnedg  49150  grlimedgnedg  49151  2zlidl  49259  2zrngALT  49273  nnpw2blen  49614  1elfz13  50865  2elfz13  50866  veronesevrowd  50901  veronesematrowd  50903  veroquadgsumlem  50905  veroquadmodzerod  50906  veroquadnolindfd  50907