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  5480  f1oi  6863  limon  7847  issmo  8357  xpider  8810  omina  10777  1eluzge0  13008  2eluzge1  13010  5eluz3  13011  0elunit  13601  1elunit  13602  fz0to3un2pr  13764  fz0to4untppr  13765  fz0to5un2tp  13766  4fvwrd4  13783  fzo0to42pr  13889  fvf1tp  13930  tpf1ofv1  14643  tpf1ofv2  14644  tpfo  14646  ccat2s1p2  14779  cats1fv  15011  pfx2  15099  wwlktovf  15110  fprodge0  16161  fprodge1  16163  sincos1sgn  16362  sincos2sgn  16363  divalglem7  16570  igz  17113  strleun  17336  strle1  17337  letsr  18768  psgnunilem2  19710  cnfldfun  21693  cnsubmlem  21722  cnsubglem  21723  cnsubrglem  21724  cnmsubglem  21737  nn0srg  21744  rge0srg  21745  xrge0subm  21750  xrge0omnd  21752  pzriprnglem4  21791  ust0  24540  cnngp  25099  cnfldtgp  25191  htpycc  25302  pco0  25336  pcocn  25339  pcohtpylem  25341  pcopt  25344  pcopt2  25345  pcoass  25346  pcorevlem  25348  sinhalfpilem  26793  sincos4thpi  26843  sincos6thpi  26845  logi  26916  argregt0  26939  argrege0  26940  elogb  27099  2logb9irr  27124  2logb9irrALT  27127  sqrt2cxp2logb9e3  27128  asin1  27223  atanbnd  27255  atan1  27257  harmonicbnd3  27336  ppiublem1  27530  zsoring  28796  usgrexmplef  29841  usgr2pthlem  30350  uspgrn2crct  30398  upgr3v3e3cycl  30782  upgr4cycl4dv4e  30787  konigsbergiedgw  30850  konigsberglem1  30854  konigsberglem2  30855  konigsberglem3  30856  konigsberglem4  30857  ex-opab  31034  isgrpoi  31101  isvciOLD  31183  isnvi  31216  adj1o  32497  bra11  32711  1fldgenq  33927  reofld  33947  xrge0slmod  33952  ccfldsrarelvec  34346  constrextdg2  34424  constrext2chnlem  34425  constrcon  34449  2sqr3minply  34455  cos9thpiminply  34463  unitssxrge0  34575  iistmd  34577  mhmhmeotmd  34602  xrge0tmdALT  34621  rerrext  34684  cnrrext  34685  volmeas  34907  ddemeas  34912  fib1  35075  ballotlem2  35164  ballotth  35213  prodfzo03  35275  bj-pinftyccb  38218  fdc  38755  riscer  38998  asin1half  43484  acos1half  43485  readvrec2  43488  jm2.27dlem2  44093  arearect  44293  areaquad  44294  onsucf1o  44350  lhe4.4ex1a  45389  wallispilem4  47154  fourierdlem20  47213  fourierdlem62  47254  fourierdlem104  47296  fourierdlem111  47303  sqwvfoura  47314  sqwvfourb  47315  fouriersw  47317  goldrapos  48006  fmtnoprmfac2lem1  48727  fmtno4prmfac  48733  31prm  48758  nprmdvdsfacm1lem4  48784  nprmdvdsfacm1  48785  ppivalnnnprmge6  48787  341fppr2  48908  4fppr1  48909  9fppr8  48911  nfermltl8rev  48916  nfermltl2rev  48917  sbgoldbo  48961  nnsum4primeseven  48974  nnsum4primesevenALTV  48975  wtgoldbnnsum4prm  48976  bgoldbnnsum3prm  48978  tgblthelfgott  48989  cycl3grtri  49121  usgrexmpl1lem  49195  usgrexmpl2lem  49200  usgrexmpl2trifr  49211  gpg5nbgrvtx13starlem2  49246  gpg5nbgr3star  49255  gpg5edgnedg  49304  grlimedgnedg  49305  2zlidl  49413  2zrngALT  49427  nnpw2blen  49768  1elfz13  51019  2elfz13  51020  veronesevrowd  51055  veronesematrowd  51057  veroquadgsumlem  51059  veroquadmodzerod  51060  veroquadnolindfd  51061