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

Theorem mpbir3an 1178
Description: Detach a conjunction of truths in a biconditional. (Contributed by NM, 16-Sep-2011.)
Hypotheses
Ref Expression
mpbir3an.1  |-  ps
mpbir3an.2  |-  ch
mpbir3an.3  |-  th
mpbir3an.4  |-  ( ph  <->  ( ps  /\  ch  /\  th ) )
Assertion
Ref Expression
mpbir3an  |-  ph

Proof of Theorem mpbir3an
StepHypRef Expression
1 mpbir3an.1 . . 3  |-  ps
2 mpbir3an.2 . . 3  |-  ch
3 mpbir3an.3 . . 3  |-  th
41, 2, 33pm3.2i 1174 . 2  |-  ( ps 
/\  ch  /\  th )
5 mpbir3an.4 . 2  |-  ( ph  <->  ( ps  /\  ch  /\  th ) )
64, 5mpbir 209 1  |-  ph
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ w3a 973
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 185  df-an 371  df-3an 975
This theorem is referenced by:  limon  6670  issmo  7037  xpider  7400  omina  9086  1eluzge0  11149  2eluzge0OLD  11151  2eluzge1  11152  0elunit  11663  1elunit  11664  4fvwrd4  11819  fzo0to42pr  11904  ccat2s1p2  12642  cats1fv  12836  wwlktovf  12906  sincos1sgn  13940  sincos2sgn  13941  divalglem7  14069  igz  14464  strlemor1  14739  strleun  14742  strle1  14743  letsr  15984  psgnunilem2  16647  xrge0subm  18586  cnsubmlem  18593  cnsubglem  18594  cnsubrglem  18595  cnmsubglem  18607  nn0srg  18613  rge0srg  18614  ust0  20848  cnngp  21413  cnfldtgp  21499  htpycc  21606  pco0  21640  pcocn  21643  pcohtpylem  21645  pcopt  21648  pcopt2  21649  pcoass  21650  pcorevlem  21652  sinhalfpilem  22982  sincos4thpi  23032  sincos6thpi  23034  argregt0  23121  argrege0  23122  asin1  23351  atanbnd  23383  atan1  23385  harmonicbnd3  23463  ppiublem1  23603  usgraex0elv  24523  usgraex1elv  24524  usgraex2elv  24525  usgraex3elv  24526  usgrcyclnl1  24767  usgrcyclnl2  24768  4cycl4v4e  24793  4cycl4dv  24794  4cycl4dv4e  24795  ex-opab  25280  isgrpoi  25327  issubgoi  25439  isvci  25602  isnvi  25633  adj1o  26940  bra11  27154  xrge0omnd  27861  reofld  27991  xrge0slmod  27995  unitssxrge0  28043  iistmd  28045  mhmhmeotmd  28070  xrge0tmdOLD  28088  rerrext  28151  cnrrext  28152  volmeas  28376  ddemeas  28381  fib1  28536  ballotlem2  28624  ballotth  28673  logi  29339  fdc  30443  riscer  30596  jm2.27dlem2  31156  arearect  31387  areaquad  31388  lhe4.4ex1a  31438  wallispilem4  32053  fourierdlem20  32112  fourierdlem62  32154  fourierdlem104  32196  fourierdlem111  32203  sqwvfoura  32214  sqwvfourb  32215  fouriersw  32217  pfx2  32530  usgra2pthlem1  32615  2zlidl  32884  2zrngALT  32898  elogb  33313  bj-pinftyccb  34767
  Copyright terms: Public domain W3C validator