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

Theorem mpbir3an 1237
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 1232 . 2 (𝜓𝜒𝜃)
5 mpbir3an.4 . 2 (𝜑 ↔ (𝜓𝜒𝜃))
64, 5mpbir 220 1 𝜑
Colors of variables: wff setvar class
Syntax hints:  wb 195  w3a 1031
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 196  df-an 385  df-3an 1033
This theorem is referenced by:  limon  6928  issmo  7332  xpider  7705  omina  9392  1eluzge0  11608  2eluzge1  11610  0elunit  12161  1elunit  12162  fz0to3un2pr  12310  4fvwrd4  12328  fzo0to42pr  12422  ccat2s1p2  13258  cats1fv  13455  wwlktovf  13547  sincos1sgn  14762  sincos2sgn  14763  divalglem7  14960  igz  15476  strlemor1  15796  strleun  15799  strle1  15800  letsr  17050  psgnunilem2  17738  xrge0subm  19606  cnsubmlem  19613  cnsubglem  19614  cnsubrglem  19615  cnmsubglem  19628  nn0srg  19635  rge0srg  19636  ust0  21833  cnngp  22393  cnfldtgp  22480  htpycc  22587  pco0  22622  pcocn  22625  pcohtpylem  22627  pcopt  22630  pcopt2  22631  pcoass  22632  pcorevlem  22634  sinhalfpilem  24019  sincos4thpi  24069  sincos6thpi  24071  argregt0  24160  argrege0  24161  elogb  24308  asin1  24421  atanbnd  24453  atan1  24455  harmonicbnd3  24534  ppiublem1  24727  usgraex0elv  25924  usgraex1elv  25925  usgraex2elv  25926  usgraex3elv  25927  usgrcyclnl1  26168  usgrcyclnl2  26169  4cycl4v4e  26194  4cycl4dv  26195  4cycl4dv4e  26196  ex-opab  26681  isgrpoi  26736  isvciOLD  26819  isnvi  26852  adj1o  28137  bra11  28351  xrge0omnd  29042  reofld  29171  xrge0slmod  29175  unitssxrge0  29274  iistmd  29276  mhmhmeotmd  29301  xrge0tmdOLD  29319  rerrext  29381  cnrrext  29382  volmeas  29621  ddemeas  29626  fib1  29789  ballotlem2  29877  ballotth  29926  logi  30873  bj-pinftyccb  32285  fdc  32711  riscer  32957  jm2.27dlem2  36595  arearect  36820  areaquad  36821  lhe4.4ex1a  37550  wallispilem4  38961  fourierdlem20  39020  fourierdlem62  39061  fourierdlem104  39103  fourierdlem111  39110  sqwvfoura  39121  sqwvfourb  39122  fouriersw  39124  fmtnoprmfac2lem1  40016  fmtno4prmfac  40022  31prm  40050  nnsum4primeseven  40216  nnsum4primesevenALTV  40217  wtgoldbnnsum4prm  40218  bgoldbnnsum3prm  40220  tgblthelfgott  40229  tgblthelfgottOLD  40236  pfx2  40275  usgr2pthlem  40969  uspgrn2crct  41011  upgr3v3e3cycl  41347  upgr4cycl4dv4e  41352  konigsbergiedgw  41416  konigsbergiedgwOLD  41417  konigsberglem1  41422  konigsberglem2  41423  konigsberglem3  41424  konigsberglem4  41425  2zlidl  41724  2zrngALT  41738  nnpw2blen  42172
  Copyright terms: Public domain W3C validator