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

Theorem mpbir3an 1338
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 1336 . 2 (𝜓𝜒𝜃)
5 mpbir3an.4 . 2 (𝜑 ↔ (𝜓𝜒𝜃))
64, 5mpbir 234 1 𝜑
Colors of variables: wff setvar class
Syntax hints:  wb 209  w3a 1084
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 210  df-an 400  df-3an 1086
This theorem is referenced by:  snopeqopsnid  5376  limon  7536  issmo  7972  xpider  8355  omina  10102  1eluzge0  12280  2eluzge1  12282  0elunit  12847  1elunit  12848  fz0to3un2pr  13004  4fvwrd4  13022  fzo0to42pr  13119  ccat2s1p2  13977  ccat2s1p2OLD  13979  cats1fv  14212  pfx2  14300  wwlktovf  14311  fprodge0  15338  fprodge1  15340  sincos1sgn  15537  sincos2sgn  15538  divalglem7  15739  igz  16259  strleun  16582  strle1  16583  letsr  17828  psgnunilem2  18614  cnfldfunALT  20102  xrge0subm  20130  cnsubmlem  20137  cnsubglem  20138  cnsubrglem  20139  cnmsubglem  20152  nn0srg  20159  rge0srg  20160  ust0  22823  cnngp  23383  cnfldtgp  23472  htpycc  23583  pco0  23617  pcocn  23620  pcohtpylem  23622  pcopt  23625  pcopt2  23626  pcoass  23627  pcorevlem  23629  sinhalfpilem  25054  sincos4thpi  25104  sincos6thpi  25106  argregt0  25199  argrege0  25200  elogb  25354  2logb9irr  25379  2logb9irrALT  25382  sqrt2cxp2logb9e3  25383  asin1  25478  atanbnd  25510  atan1  25512  harmonicbnd3  25591  ppiublem1  25784  usgrexmplef  27047  usgr2pthlem  27550  uspgrn2crct  27592  upgr3v3e3cycl  27963  upgr4cycl4dv4e  27968  konigsbergiedgw  28031  konigsberglem1  28035  konigsberglem2  28036  konigsberglem3  28037  konigsberglem4  28038  ex-opab  28215  isgrpoi  28279  isvciOLD  28361  isnvi  28394  adj1o  29675  bra11  29889  xrge0omnd  30743  reofld  30945  xrge0slmod  30949  ccfldsrarelvec  31113  unitssxrge0  31217  iistmd  31219  mhmhmeotmd  31244  xrge0tmdALT  31263  rerrext  31324  cnrrext  31325  volmeas  31564  ddemeas  31569  fib1  31732  ballotlem2  31820  ballotth  31869  prodfzo03  31948  logi  33040  bj-pinftyccb  34597  fdc  35145  riscer  35388  jm2.27dlem2  39885  arearect  40099  areaquad  40100  lhe4.4ex1a  40971  wallispilem4  42653  fourierdlem20  42712  fourierdlem62  42753  fourierdlem104  42795  fourierdlem111  42802  sqwvfoura  42813  sqwvfourb  42814  fouriersw  42816  fmtnoprmfac2lem1  44026  fmtno4prmfac  44032  31prm  44057  341fppr2  44195  4fppr1  44196  9fppr8  44198  nfermltl8rev  44203  nfermltl2rev  44204  sbgoldbo  44248  nnsum4primeseven  44261  nnsum4primesevenALTV  44262  wtgoldbnnsum4prm  44263  bgoldbnnsum3prm  44265  tgblthelfgott  44276  2zlidl  44501  2zrngALT  44515  nnpw2blen  44937
  Copyright terms: Public domain W3C validator