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

Theorem mpbir3and 1138
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 1135 . 2  |-  ( ph  ->  ( ch  /\  th  /\  ta ) )
5 mpbir3and.4 . 2  |-  ( ph  ->  ( ps  <->  ( ch  /\ 
th  /\  ta )
) )
64, 5mpbird 225 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ w3a 937
This theorem is referenced by:  canthwelem  8530  intwun  8615  tskwun  8664  gruwun  8693  ixxss1  10939  ixxss2  10940  ixxss12  10941  ixxub  10942  ixxlb  10943  ubioc1  10970  lbico1  10971  lbicc2  11018  ubicc2  11019  difreicc  11033  zmodfz  11273  phicl2  13162  4sqlem12  13329  isfuncd  14067  idfucl  14083  cofucl  14090  invfuc  14176  cnvps  14649  psss  14651  submid  14756  subsubm  14762  mhmima  14768  mhmeql  14769  gsumwspan  14796  frmdsssubm  14811  subgint  14969  0subg  14970  cycsubgcl  14971  nmzsubg  14986  eqger  14995  eqgcpbl  14999  ghmrn  15024  ghmpreima  15032  gastacl  15091  cntzsubm  15139  sylow2blem1  15259  lsmsubm  15292  torsubg  15474  oddvdssubg  15475  dmdprdd  15565  dprdwd  15574  dprdsubg  15587  dprdres  15591  unitsubm  15780  subrgsubm  15886  subrgugrp  15892  subrgint  15895  issubdrg  15898  cntzsubr  15905  lsssubg  16038  islmhm2  16119  pj1lmhm  16177  islbs2  16231  islbs3  16232  lbsextlem4  16238  issubgrpd2  16265  issubrngd2  16267  lidlsubg  16291  2idlcpbl  16310  mplsubglem  16503  mplsubrg  16508  mplind  16567  isphld  16890  lmcnp  17373  isufil2  17945  ufileu  17956  filufint  17957  fmfnfm  17995  flimclslem  18021  fclsfnflim  18064  flimfnfcls  18065  fclscmp  18067  clssubg  18143  tgpconcompeqg  18146  tgpconcomp  18147  divstgpopn  18154  tgptsmscls  18184  xmeter  18468  metustOLD  18602  metust  18603  tgqioo  18836  zcld  18849  iccntr  18857  icccmplem2  18859  icccmplem3  18860  reconnlem1  18862  reconnlem2  18863  xrge0tsms  18870  cnheiborlem  18984  om1addcl  19063  pi1blem  19069  pi1grplem  19079  pi1inv  19082  pi1xfr  19085  pi1xfrcnvlem  19086  pi1coghm  19091  cmetcaulem  19246  ivthlem2  19354  ivthlem3  19355  ovolicc2lem2  19419  ovolicc2lem5  19422  opnmbllem  19498  volcn  19503  ismbf3d  19549  mbfi1fseqlem6  19615  itg2const2  19636  i1fibl  19702  ibladd  19715  ditgsplitlem  19752  dvferm1lem  19873  dvferm2lem  19875  dvlip2  19884  dvivthlem1  19897  dvne0  19900  lhop1lem  19902  lhop1  19903  lhop  19905  dvcnvrelem1  19906  dvcnvrelem2  19907  dvcnvre  19908  ftc1lem1  19924  itgsubst  19938  aaliou3lem2  20265  psercnlem2  20345  efif1olem2  20450  logtayl  20556  log2tlbnd  20790  xrlimcnp  20812  pntibndlem2  21290  pntlemj  21302  pntleml  21310  wlkonwlk  21540  0wlkon  21552  constr1trl  21593  constr2wlk  21603  constr2trl  21604  constr2pth  21606  2pthon  21607  isgrp2d  21828  isgrpda  21890  rngomndo  22014  eliccelico  24145  elicoelioo  24146  xrge0tsmsd  24228  tpr2rico  24315  measinb  24580  cntmeas  24585  dya2icoseg  24632  rescon  24938  cvmsss2  24966  cvmliftlem10  24986  dfrtrcl2  25153  axlowdim  25905  cgrextend  25947  cgr3rflx  25993  cgrxfr  25994  btwnconn1lem4  26029  btwnconn1lem8  26033  btwnconn1lem11  26036  opnmbllem0  26254  dvtanlem  26268  ibladdnc  26276  bddiblnc  26289  ftc1anc  26302  isbnd3  26507  prdsbnd  26516  rngohomco  26604  rngoisocnv  26611  rngoidl  26648  0idl  26649  intidl  26653  unichnidl  26655  keridl  26656  smprngopr  26676  modelico  26898  issubmd  27374  mon1psubm  27516  cusgraisrusgra  28449  lshpnel2N  29857  lkrshp  29977  4atexlemex2  30942  4atex  30947  cdleme0moN  31096  istendod  31633  dihlspsnat  32205  dochsatshp  32323
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator