MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpbir3an Structured version   Visualization version   GIF version

Theorem mpbir3an 1263
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
StepHypRef Expression
1 mpbir3an.1 . . 3 𝜓
2 mpbir3an.2 . . 3 𝜒
3 mpbir3an.3 . . 3 𝜃
41, 2, 33pm3.2i 1259 . 2 (𝜓𝜒𝜃)
5 mpbir3an.4 . 2 (𝜑 ↔ (𝜓𝜒𝜃))
64, 5mpbir 221 1 𝜑
Colors of variables: wff setvar class
Syntax hints:  wb 196  w3a 1054
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 197  df-an 385  df-3an 1056
This theorem is referenced by:  limon  7078  issmo  7490  xpider  7861  omina  9551  1eluzge0  11770  2eluzge1  11772  0elunit  12328  1elunit  12329  fz0to3un2pr  12480  4fvwrd4  12498  fzo0to42pr  12595  ccat2s1p2  13450  cats1fv  13650  wwlktovf  13745  sincos1sgn  14967  sincos2sgn  14968  divalglem7  15169  igz  15685  strlemor1OLD  16016  strleun  16019  strle1  16020  letsr  17274  psgnunilem2  17961  cnfldfunALT  19807  xrge0subm  19835  cnsubmlem  19842  cnsubglem  19843  cnsubrglem  19844  cnmsubglem  19857  nn0srg  19864  rge0srg  19865  ust0  22070  cnngp  22630  cnfldtgp  22719  htpycc  22826  pco0  22860  pcocn  22863  pcohtpylem  22865  pcopt  22868  pcopt2  22869  pcoass  22870  pcorevlem  22872  sinhalfpilem  24260  sincos4thpi  24310  sincos6thpi  24312  argregt0  24401  argrege0  24402  elogb  24553  asin1  24666  atanbnd  24698  atan1  24700  harmonicbnd3  24779  ppiublem1  24972  usgrexmplef  26196  usgr2pthlem  26715  uspgrn2crct  26756  upgr3v3e3cycl  27158  upgr4cycl4dv4e  27163  konigsbergiedgw  27226  konigsberglem1  27230  konigsberglem2  27231  konigsberglem3  27232  konigsberglem4  27233  ex-opab  27419  isgrpoi  27480  isvciOLD  27563  isnvi  27596  adj1o  28881  bra11  29095  xrge0omnd  29839  reofld  29968  xrge0slmod  29972  unitssxrge0  30074  iistmd  30076  mhmhmeotmd  30101  xrge0tmdOLD  30119  rerrext  30181  cnrrext  30182  volmeas  30422  ddemeas  30427  fib1  30590  ballotlem2  30678  ballotth  30727  prodfzo03  30809  logi  31746  bj-pinftyccb  33238  fdc  33671  riscer  33917  jm2.27dlem2  37894  arearect  38118  areaquad  38119  lhe4.4ex1a  38845  wallispilem4  40603  fourierdlem20  40662  fourierdlem62  40703  fourierdlem104  40745  fourierdlem111  40752  sqwvfoura  40763  sqwvfourb  40764  fouriersw  40766  pfx2  41737  fmtnoprmfac2lem1  41803  fmtno4prmfac  41809  31prm  41837  sbgoldbo  42000  nnsum4primeseven  42013  nnsum4primesevenALTV  42014  wtgoldbnnsum4prm  42015  bgoldbnnsum3prm  42017  tgblthelfgott  42028  tgblthelfgottOLD  42034  2zlidl  42259  2zrngALT  42273  nnpw2blen  42699
  Copyright terms: Public domain W3C validator