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  1455  snopeqopsnid  5485  f1oi  6886  limon  7871  issmo  8384  xpider  8837  omina  10803  1eluzge0  13034  2eluzge1  13036  5eluz3  13037  0elunit  13627  1elunit  13628  fz0to3un2pr  13790  fz0to4untppr  13791  fz0to5un2tp  13792  4fvwrd4  13809  fzo0to42pr  13915  fvf1tp  13956  tpf1ofv1  14669  tpf1ofv2  14670  tpfo  14672  ccat2s1p2  14806  cats1fv  15038  pfx2  15127  wwlktovf  15138  fprodge0  16189  fprodge1  16191  sincos1sgn  16390  sincos2sgn  16391  divalglem7  16598  igz  17141  strleun  17364  strle1  17365  letsr  18796  psgnunilem2  19739  cnfldfun  21722  cnsubmlem  21751  cnsubglem  21752  cnsubrglem  21753  cnmsubglem  21766  nn0srg  21773  rge0srg  21774  xrge0subm  21779  xrge0omnd  21781  pzriprnglem4  21820  ust0  24569  cnngp  25128  cnfldtgp  25220  htpycc  25331  pco0  25365  pcocn  25368  pcohtpylem  25370  pcopt  25373  pcopt2  25374  pcoass  25375  pcorevlem  25377  sinhalfpilem  26822  sincos4thpi  26872  sincos6thpi  26874  logi  26945  argregt0  26968  argrege0  26969  elogb  27128  2logb9irr  27153  2logb9irrALT  27156  sqrt2cxp2logb9e3  27157  asin1  27252  atanbnd  27284  atan1  27286  harmonicbnd3  27365  ppiublem1  27559  zsoring  28825  usgrexmplef  29870  usgr2pthlem  30379  uspgrn2crct  30427  upgr3v3e3cycl  30811  upgr4cycl4dv4e  30816  konigsbergiedgw  30879  konigsberglem1  30883  konigsberglem2  30884  konigsberglem3  30885  konigsberglem4  30886  ex-opab  31063  isgrpoi  31130  isvciOLD  31212  isnvi  31245  adj1o  32526  bra11  32740  1fldgenq  33954  reofld  33974  xrge0slmod  33979  ccfldsrarelvec  34373  constrextdg2  34451  constrext2chnlem  34452  constrcon  34476  2sqr3minply  34482  cos9thpiminply  34490  unitssxrge0  34602  iistmd  34604  mhmhmeotmd  34629  xrge0tmdALT  34648  rerrext  34711  cnrrext  34712  volmeas  34934  ddemeas  34939  fib1  35102  ballotlem2  35191  ballotth  35240  prodfzo03  35302  bj-pinftyccb  38334  fdc  38871  riscer  39114  asin1half  43601  acos1half  43602  readvrec2  43605  jm2.27dlem2  44210  arearect  44409  areaquad  44410  onsucf1o  44466  lhe4.4ex1a  45505  wallispilem4  47283  fourierdlem20  47342  fourierdlem62  47383  fourierdlem104  47425  fourierdlem111  47432  sqwvfoura  47443  sqwvfourb  47444  fouriersw  47446  goldrapos  48135  fmtnoprmfac2lem1  48856  fmtno4prmfac  48862  31prm  48887  nprmdvdsfacm1lem4  48913  nprmdvdsfacm1  48914  ppivalnnnprmge6  48916  341fppr2  49037  4fppr1  49038  9fppr8  49040  nfermltl8rev  49045  nfermltl2rev  49046  sbgoldbo  49090  nnsum4primeseven  49103  nnsum4primesevenALTV  49104  wtgoldbnnsum4prm  49105  bgoldbnnsum3prm  49107  tgblthelfgott  49118  cycl3grtri  49250  usgrexmpl1lem  49324  usgrexmpl2lem  49329  usgrexmpl2trifr  49340  gpg5nbgrvtx13starlem2  49375  gpg5nbgr3star  49384  gpg5edgnedg  49433  grlimedgnedg  49434  2zlidl  49542  2zrngALT  49556  nnpw2blen  49897  1elfz13  51223  2elfz13  51224  veronesevrowd  51259  veronesematrowd  51261  veroquadgsumlem  51263  veroquadmodzerod  51264  veroquadnolindfd  51265