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

Theorem mpbir3and 1135
Description: Detach a conjunction of truths in a biconditional. (Contributed by Mario Carneiro, 11-May-2014.) (Revised by Mario Carneiro, 9-Jan-2015.)
Hypotheses
Ref Expression
mpbir3and.1  |-  ( ph  ->  ch )
mpbir3and.2  |-  ( ph  ->  th )
mpbir3and.3  |-  ( ph  ->  ta )
mpbir3and.4  |-  ( ph  ->  ( ps  <->  ( ch  /\ 
th  /\  ta )
) )
Assertion
Ref Expression
mpbir3and  |-  ( ph  ->  ps )

Proof of Theorem mpbir3and
StepHypRef Expression
1 mpbir3and.1 . . 3  |-  ( ph  ->  ch )
2 mpbir3and.2 . . 3  |-  ( ph  ->  th )
3 mpbir3and.3 . . 3  |-  ( ph  ->  ta )
41, 2, 33jca 1132 . 2  |-  ( ph  ->  ( ch  /\  th  /\  ta ) )
5 mpbir3and.4 . 2  |-  ( ph  ->  ( ps  <->  ( ch  /\ 
th  /\  ta )
) )
64, 5mpbird 223 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ w3a 934
This theorem is referenced by:  canthwelem  8288  intwun  8373  tskwun  8422  gruwun  8451  ixxss1  10690  ixxss2  10691  ixxss12  10692  ixxub  10693  ixxlb  10694  ubioc1  10721  lbico1  10722  lbicc2  10768  ubicc2  10769  difreicc  10783  zmodfz  11007  phicl2  12852  4sqlem12  13019  isfuncd  13755  idfucl  13771  cofucl  13778  invfuc  13864  cnvps  14337  psss  14339  submid  14444  subsubm  14450  mhmima  14456  mhmeql  14457  gsumwspan  14484  frmdsssubm  14499  subgint  14657  0subg  14658  cycsubgcl  14659  nmzsubg  14674  eqger  14683  eqgcpbl  14687  ghmrn  14712  ghmpreima  14720  gastacl  14779  cntzsubm  14827  sylow2blem1  14947  lsmsubm  14980  torsubg  15162  oddvdssubg  15163  dmdprdd  15253  dprdwd  15262  dprdsubg  15275  dprdres  15279  unitsubm  15468  subrgsubm  15574  subrgugrp  15580  subrgint  15583  issubdrg  15586  cntzsubr  15593  lsssubg  15730  islmhm2  15811  pj1lmhm  15869  islbs2  15923  islbs3  15924  lbsextlem4  15930  issubgrpd2  15957  issubrngd2  15959  lidlsubg  15983  2idlcpbl  16002  mplsubglem  16195  mplsubrg  16200  mplind  16259  isphld  16574  lmcnp  17048  isufil2  17619  ufileu  17630  filufint  17631  fmfnfm  17669  flimclslem  17695  fclsfnflim  17738  flimfnfcls  17739  fclscmp  17741  clssubg  17807  tgpconcompeqg  17810  tgpconcomp  17811  divstgpopn  17818  tgptsmscls  17848  xmeter  17995  tgqioo  18322  zcld  18335  iccntr  18342  icccmplem2  18344  icccmplem3  18345  reconnlem1  18347  reconnlem2  18348  xrge0tsms  18355  cnheiborlem  18468  om1addcl  18547  pi1blem  18553  pi1grplem  18563  pi1inv  18566  pi1xfr  18569  pi1xfrcnvlem  18570  pi1coghm  18575  cmetcaulem  18730  ivthlem2  18828  ivthlem3  18829  ovolicc2lem2  18893  ovolicc2lem5  18896  opnmbllem  18972  volcn  18977  ismbf3d  19025  mbfi1fseqlem6  19091  itg2const2  19112  i1fibl  19178  ibladd  19191  ditgsplitlem  19226  dvferm1lem  19347  dvferm2lem  19349  dvlip2  19358  dvivthlem1  19371  dvne0  19374  lhop1lem  19376  lhop1  19377  lhop  19379  dvcnvrelem1  19380  dvcnvrelem2  19381  dvcnvre  19382  ftc1lem1  19398  itgsubst  19412  aaliou3lem2  19739  psercnlem2  19816  efif1olem2  19921  logtayl  20023  log2tlbnd  20257  xrlimcnp  20279  pntibndlem2  20756  pntlemj  20768  pntleml  20776  isgrp2d  20918  isgrpda  20980  rngomndo  21104  xrge0tsmsd  23397  measinb  23563  rescon  23792  cvmsss2  23820  cvmliftlem10  23840  dfrtrcl2  24060  axlowdim  24661  cgrextend  24703  cgr3rflx  24749  cgrxfr  24750  btwnconn1lem4  24785  btwnconn1lem8  24789  btwnconn1lem11  24792  ibladdnc  25008  bddiblnc  25021  sqpre  25341  truni3  25610  efilcp  25655  fgsb2  25658  tcnvec  25793  icccon3  25804  idcatfun  26044  rocatval  26062  clscnc  26113  isbnd3  26611  prdsbnd  26620  rngohomco  26708  rngoisocnv  26715  rngoidl  26752  0idl  26753  intidl  26757  unichnidl  26759  keridl  26760  smprngopr  26780  modelico  27009  issubmd  27486  mon1psubm  27628  wlkonwlk  28334  lshpnel2N  29797  lkrshp  29917  4atexlemex2  30882  4atex  30887  cdleme0moN  31036  istendod  31573  dihlspsnat  32145  dochsatshp  32263
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator