Theorem mpbir3an 1359

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

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

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 401  df-3an 1104

This theorem is used by:  3jaoi  1453  snopeqopsnid  5491  f1oi  6859  limon  7830  issmo  8333  xpider  8784  omina  10682  1eluzge0  12910  2eluzge1  12912  5eluz3  12913  0elunit  13502  1elunit  13503  fz0to3un2pr  13664  fz0to4untppr  13665  fz0to5un2tp  13666  4fvwrd4  13683  fzo0to42pr  13789  fvf1tp  13829  tpf1ofv1  14541  tpf1ofv2  14542  tpfo  14544  ccat2s1p2  14675  cats1fv  14903  pfx2  14991  wwlktovf  15000  fprodge0  16054  fprodge1  16056  sincos1sgn  16255  sincos2sgn  16256  divalglem7  16463  igz  17000  strleun  17223  strle1  17224  letsr  18655  psgnunilem2  19571  cnfldfun  21547  cnsubmlem  21576  cnsubglem  21577  cnsubrglem  21578  cnmsubglem  21591  nn0srg  21598  rge0srg  21599  xrge0subm  21604  xrge0omnd  21606  pzriprnglem4  21645  ust0  24388  cnngp  24947  cnfldtgp  25039  htpycc  25150  pco0  25184  pcocn  25187  pcohtpylem  25189  pcopt  25192  pcopt2  25193  pcoass  25194  pcorevlem  25196  sinhalfpilem  26639  sincos4thpi  26689  sincos6thpi  26692  logi  26763  argregt0  26786  argrege0  26787  elogb  26946  2logb9irr  26971  2logb9irrALT  26974  sqrt2cxp2logb9e3  26975  asin1  27070  atanbnd  27102  atan1  27104  harmonicbnd3  27183  ppiublem1  27377  zsoring  28613  usgrexmplef  29620  usgr2pthlem  30123  uspgrn2crct  30168  upgr3v3e3cycl  30542  upgr4cycl4dv4e  30547  konigsbergiedgw  30610  konigsberglem1  30614  konigsberglem2  30615  konigsberglem3  30616  konigsberglem4  30617  ex-opab  30794  isgrpoi  30861  isvciOLD  30943  isnvi  30976  adj1o  32257  bra11  32471  1fldgenq  33652  reofld  33672  xrge0slmod  33677  ccfldsrarelvec  34070  constrextdg2  34148  constrext2chnlem  34149  constrcon  34173  2sqr3minply  34179  cos9thpiminply  34187  unitssxrge0  34299  iistmd  34301  mhmhmeotmd  34326  xrge0tmdALT  34345  rerrext  34408  cnrrext  34409  volmeas  34630  ddemeas  34635  fib1  34799  ballotlem2  34888  ballotth  34937  prodfzo03  34999  bj-pinftyccb  37893  fdc  38424  riscer  38667  asin1half  43146  acos1half  43147  readvrec2  43150  jm2.27dlem2  43765  arearect  43970  areaquad  43971  onsucf1o  44027  lhe4.4ex1a  45067  wallispilem4  46810  fourierdlem20  46869  fourierdlem62  46910  fourierdlem104  46952  fourierdlem111  46959  sqwvfoura  46970  sqwvfourb  46971  fouriersw  46973  goldrapos  47648  fmtnoprmfac2lem1  48346  fmtno4prmfac  48352  31prm  48377  nprmdvdsfacm1lem4  48403  nprmdvdsfacm1  48404  ppivalnnnprmge6  48406  341fppr2  48527  4fppr1  48528  9fppr8  48530  nfermltl8rev  48535  nfermltl2rev  48536  sbgoldbo  48580  nnsum4primeseven  48593  nnsum4primesevenALTV  48594  wtgoldbnnsum4prm  48595  bgoldbnnsum3prm  48597  tgblthelfgott  48608  cycl3grtri  48740  usgrexmpl1lem  48814  usgrexmpl2lem  48819  usgrexmpl2trifr  48830  gpg5nbgrvtx13starlem2  48865  gpg5nbgr3star  48874  gpg5edgnedg  48923  grlimedgnedg  48924  2zlidl  49033  2zrngALT  49047  nnpw2blen  49388  1elfz13  50652