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

Theorem mpbir3and 1137
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 1134 . 2  |-  ( ph  ->  ( ch  /\  th  /\  ta ) )
5 mpbir3and.4 . 2  |-  ( ph  ->  ( ps  <->  ( ch  /\ 
th  /\  ta )
) )
64, 5mpbird 224 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ w3a 936
This theorem is referenced by:  canthwelem  8517  intwun  8602  tskwun  8651  gruwun  8680  ixxss1  10926  ixxss2  10927  ixxss12  10928  ixxub  10929  ixxlb  10930  ubioc1  10957  lbico1  10958  lbicc2  11005  ubicc2  11006  difreicc  11020  zmodfz  11260  phicl2  13149  4sqlem12  13316  isfuncd  14054  idfucl  14070  cofucl  14077  invfuc  14163  cnvps  14636  psss  14638  submid  14743  subsubm  14749  mhmima  14755  mhmeql  14756  gsumwspan  14783  frmdsssubm  14798  subgint  14956  0subg  14957  cycsubgcl  14958  nmzsubg  14973  eqger  14982  eqgcpbl  14986  ghmrn  15011  ghmpreima  15019  gastacl  15078  cntzsubm  15126  sylow2blem1  15246  lsmsubm  15279  torsubg  15461  oddvdssubg  15462  dmdprdd  15552  dprdwd  15561  dprdsubg  15574  dprdres  15578  unitsubm  15767  subrgsubm  15873  subrgugrp  15879  subrgint  15882  issubdrg  15885  cntzsubr  15892  lsssubg  16025  islmhm2  16106  pj1lmhm  16164  islbs2  16218  islbs3  16219  lbsextlem4  16225  issubgrpd2  16252  issubrngd2  16254  lidlsubg  16278  2idlcpbl  16297  mplsubglem  16490  mplsubrg  16495  mplind  16554  isphld  16877  lmcnp  17360  isufil2  17932  ufileu  17943  filufint  17944  fmfnfm  17982  flimclslem  18008  fclsfnflim  18051  flimfnfcls  18052  fclscmp  18054  clssubg  18130  tgpconcompeqg  18133  tgpconcomp  18134  divstgpopn  18141  tgptsmscls  18171  xmeter  18455  metustOLD  18589  metust  18590  tgqioo  18823  zcld  18836  iccntr  18844  icccmplem2  18846  icccmplem3  18847  reconnlem1  18849  reconnlem2  18850  xrge0tsms  18857  cnheiborlem  18971  om1addcl  19050  pi1blem  19056  pi1grplem  19066  pi1inv  19069  pi1xfr  19072  pi1xfrcnvlem  19073  pi1coghm  19078  cmetcaulem  19233  ivthlem2  19341  ivthlem3  19342  ovolicc2lem2  19406  ovolicc2lem5  19409  opnmbllem  19485  volcn  19490  ismbf3d  19538  mbfi1fseqlem6  19604  itg2const2  19625  i1fibl  19691  ibladd  19704  ditgsplitlem  19739  dvferm1lem  19860  dvferm2lem  19862  dvlip2  19871  dvivthlem1  19884  dvne0  19887  lhop1lem  19889  lhop1  19890  lhop  19892  dvcnvrelem1  19893  dvcnvrelem2  19894  dvcnvre  19895  ftc1lem1  19911  itgsubst  19925  aaliou3lem2  20252  psercnlem2  20332  efif1olem2  20437  logtayl  20543  log2tlbnd  20777  xrlimcnp  20799  pntibndlem2  21277  pntlemj  21289  pntleml  21297  wlkonwlk  21527  0wlkon  21539  constr1trl  21580  constr2wlk  21590  constr2trl  21591  constr2pth  21593  2pthon  21594  isgrp2d  21815  isgrpda  21877  rngomndo  22001  eliccelico  24132  elicoelioo  24133  xrge0tsmsd  24215  tpr2rico  24302  measinb  24567  cntmeas  24572  dya2icoseg  24619  rescon  24925  cvmsss2  24953  cvmliftlem10  24973  dfrtrcl2  25140  axlowdim  25892  cgrextend  25934  cgr3rflx  25980  cgrxfr  25981  btwnconn1lem4  26016  btwnconn1lem8  26020  btwnconn1lem11  26023  mblfinlem  26234  ibladdnc  26252  bddiblnc  26265  ftc1anc  26278  isbnd3  26484  prdsbnd  26493  rngohomco  26581  rngoisocnv  26588  rngoidl  26625  0idl  26626  intidl  26630  unichnidl  26632  keridl  26633  smprngopr  26653  modelico  26875  issubmd  27351  mon1psubm  27493  lshpnel2N  29720  lkrshp  29840  4atexlemex2  30805  4atex  30810  cdleme0moN  30959  istendod  31496  dihlspsnat  32068  dochsatshp  32186
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator