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

Theorem mpbir3an 1342
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 1340 . 2 (𝜓𝜒𝜃)
5 mpbir3an.4 . 2 (𝜑 ↔ (𝜓𝜒𝜃))
64, 5mpbir 230 1 𝜑
Colors of variables: wff setvar class
Syntax hints:  wb 205  w3a 1088
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 206  df-an 398  df-3an 1090
This theorem is referenced by:  snopeqopsnid  5470  limon  7775  issmo  8298  xpider  8733  omina  10635  1eluzge0  12825  2eluzge1  12827  0elunit  13395  1elunit  13396  fz0to3un2pr  13552  4fvwrd4  13570  fzo0to42pr  13668  ccat2s1p2  14527  cats1fv  14757  pfx2  14845  wwlktovf  14854  fprodge0  15884  fprodge1  15886  sincos1sgn  16083  sincos2sgn  16084  divalglem7  16289  igz  16814  strleun  17037  strle1  17038  letsr  18490  psgnunilem2  19285  cnfldfun  20831  xrge0subm  20861  cnsubmlem  20868  cnsubglem  20869  cnsubrglem  20870  cnmsubglem  20883  nn0srg  20890  rge0srg  20891  ust0  23594  cnngp  24166  cnfldtgp  24255  htpycc  24366  pco0  24400  pcocn  24403  pcohtpylem  24405  pcopt  24408  pcopt2  24409  pcoass  24410  pcorevlem  24412  sinhalfpilem  25843  sincos4thpi  25893  sincos6thpi  25895  argregt0  25988  argrege0  25989  elogb  26143  2logb9irr  26168  2logb9irrALT  26171  sqrt2cxp2logb9e3  26172  asin1  26267  atanbnd  26299  atan1  26301  harmonicbnd3  26380  ppiublem1  26573  usgrexmplef  28256  usgr2pthlem  28760  uspgrn2crct  28802  upgr3v3e3cycl  29173  upgr4cycl4dv4e  29178  konigsbergiedgw  29241  konigsberglem1  29245  konigsberglem2  29246  konigsberglem3  29247  konigsberglem4  29248  ex-opab  29425  isgrpoi  29489  isvciOLD  29571  isnvi  29604  adj1o  30885  bra11  31099  xrge0omnd  31975  1fldgenq  32143  reofld  32190  xrge0slmod  32194  ccfldsrarelvec  32419  unitssxrge0  32545  iistmd  32547  mhmhmeotmd  32572  xrge0tmdALT  32591  rerrext  32654  cnrrext  32655  volmeas  32894  ddemeas  32899  fib1  33064  ballotlem2  33152  ballotth  33201  prodfzo03  33280  logi  34370  bj-pinftyccb  35742  fdc  36254  riscer  36497  acos1half  40672  jm2.27dlem2  41381  arearect  41596  areaquad  41597  onsucf1o  41654  lhe4.4ex1a  42701  wallispilem4  44399  fourierdlem20  44458  fourierdlem62  44499  fourierdlem104  44541  fourierdlem111  44548  sqwvfoura  44559  sqwvfourb  44560  fouriersw  44562  tworepnotupword  45215  fmtnoprmfac2lem1  45848  fmtno4prmfac  45854  31prm  45879  341fppr2  46016  4fppr1  46017  9fppr8  46019  nfermltl8rev  46024  nfermltl2rev  46025  sbgoldbo  46069  nnsum4primeseven  46082  nnsum4primesevenALTV  46083  wtgoldbnnsum4prm  46084  bgoldbnnsum3prm  46086  tgblthelfgott  46097  2zlidl  46322  2zrngALT  46336  nnpw2blen  46756
  Copyright terms: Public domain W3C validator