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

Theorem mpbir3an 1427
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 1424 . 2 (𝜓𝜒𝜃)
5 mpbir3an.4 . 2 (𝜑 ↔ (𝜓𝜒𝜃))
64, 5mpbir 221 1 𝜑
Colors of variables: wff setvar class
Syntax hints:  wb 196  w3a 1072
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 1074
This theorem is referenced by:  limon  7199  issmo  7612  xpider  7983  omina  9703  1eluzge0  11923  2eluzge1  11925  0elunit  12481  1elunit  12482  fz0to3un2pr  12633  4fvwrd4  12651  fzo0to42pr  12747  ccat2s1p2  13602  cats1fv  13802  wwlktovf  13898  sincos1sgn  15120  sincos2sgn  15121  divalglem7  15322  igz  15838  strlemor1OLD  16169  strleun  16172  strle1  16173  letsr  17426  psgnunilem2  18113  cnfldfunALT  19959  xrge0subm  19987  cnsubmlem  19994  cnsubglem  19995  cnsubrglem  19996  cnmsubglem  20009  nn0srg  20016  rge0srg  20017  ust0  22222  cnngp  22782  cnfldtgp  22871  htpycc  22978  pco0  23012  pcocn  23015  pcohtpylem  23017  pcopt  23020  pcopt2  23021  pcoass  23022  pcorevlem  23024  sinhalfpilem  24412  sincos4thpi  24462  sincos6thpi  24464  argregt0  24553  argrege0  24554  elogb  24705  asin1  24818  atanbnd  24850  atan1  24852  harmonicbnd3  24931  ppiublem1  25124  usgrexmplef  26348  usgr2pthlem  26867  uspgrn2crct  26909  upgr3v3e3cycl  27330  upgr4cycl4dv4e  27335  konigsbergiedgw  27398  konigsberglem1  27402  konigsberglem2  27403  konigsberglem3  27404  konigsberglem4  27405  ex-opab  27598  isgrpoi  27659  isvciOLD  27742  isnvi  27775  adj1o  29060  bra11  29274  xrge0omnd  30018  reofld  30147  xrge0slmod  30151  unitssxrge0  30253  iistmd  30255  mhmhmeotmd  30280  xrge0tmdOLD  30298  rerrext  30360  cnrrext  30361  volmeas  30601  ddemeas  30606  fib1  30769  ballotlem2  30857  ballotth  30906  prodfzo03  30988  logi  31925  bj-pinftyccb  33417  fdc  33852  riscer  34098  jm2.27dlem2  38077  arearect  38301  areaquad  38302  lhe4.4ex1a  39028  wallispilem4  40786  fourierdlem20  40845  fourierdlem62  40886  fourierdlem104  40928  fourierdlem111  40935  sqwvfoura  40946  sqwvfourb  40947  fouriersw  40949  pfx2  41920  fmtnoprmfac2lem1  41986  fmtno4prmfac  41992  31prm  42020  sbgoldbo  42183  nnsum4primeseven  42196  nnsum4primesevenALTV  42197  wtgoldbnnsum4prm  42198  bgoldbnnsum3prm  42200  tgblthelfgott  42211  tgblthelfgottOLD  42217  2zlidl  42442  2zrngALT  42456  nnpw2blen  42882
  Copyright terms: Public domain W3C validator