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  8272  intwun  8357  tskwun  8406  gruwun  8435  ixxss1  10674  ixxss2  10675  ixxss12  10676  ixxub  10677  ixxlb  10678  ubioc1  10705  lbico1  10706  lbicc2  10752  ubicc2  10753  difreicc  10767  zmodfz  10991  phicl2  12836  4sqlem12  13003  isfuncd  13739  idfucl  13755  cofucl  13762  invfuc  13848  cnvps  14321  psss  14323  submid  14428  subsubm  14434  mhmima  14440  mhmeql  14441  gsumwspan  14468  frmdsssubm  14483  subgint  14641  0subg  14642  cycsubgcl  14643  nmzsubg  14658  eqger  14667  eqgcpbl  14671  ghmrn  14696  ghmpreima  14704  gastacl  14763  cntzsubm  14811  sylow2blem1  14931  lsmsubm  14964  torsubg  15146  oddvdssubg  15147  dmdprdd  15237  dprdwd  15246  dprdsubg  15259  dprdres  15263  unitsubm  15452  subrgsubm  15558  subrgugrp  15564  subrgint  15567  issubdrg  15570  cntzsubr  15577  lsssubg  15714  islmhm2  15795  pj1lmhm  15853  islbs2  15907  islbs3  15908  lbsextlem4  15914  issubgrpd2  15941  issubrngd2  15943  lidlsubg  15967  2idlcpbl  15986  mplsubglem  16179  mplsubrg  16184  mplind  16243  isphld  16558  lmcnp  17032  isufil2  17603  ufileu  17614  filufint  17615  fmfnfm  17653  flimclslem  17679  fclsfnflim  17722  flimfnfcls  17723  fclscmp  17725  clssubg  17791  tgpconcompeqg  17794  tgpconcomp  17795  divstgpopn  17802  tgptsmscls  17832  xmeter  17979  tgqioo  18306  zcld  18319  iccntr  18326  icccmplem2  18328  icccmplem3  18329  reconnlem1  18331  reconnlem2  18332  xrge0tsms  18339  cnheiborlem  18452  om1addcl  18531  pi1blem  18537  pi1grplem  18547  pi1inv  18550  pi1xfr  18553  pi1xfrcnvlem  18554  pi1coghm  18559  cmetcaulem  18714  ivthlem2  18812  ivthlem3  18813  ovolicc2lem2  18877  ovolicc2lem5  18880  opnmbllem  18956  volcn  18961  ismbf3d  19009  mbfi1fseqlem6  19075  itg2const2  19096  i1fibl  19162  ibladd  19175  ditgsplitlem  19210  dvferm1lem  19331  dvferm2lem  19333  dvlip2  19342  dvivthlem1  19355  dvne0  19358  lhop1lem  19360  lhop1  19361  lhop  19363  dvcnvrelem1  19364  dvcnvrelem2  19365  dvcnvre  19366  ftc1lem1  19382  itgsubst  19396  aaliou3lem2  19723  psercnlem2  19800  efif1olem2  19905  logtayl  20007  log2tlbnd  20241  xrlimcnp  20263  pntibndlem2  20740  pntlemj  20752  pntleml  20760  isgrp2d  20902  isgrpda  20964  rngomndo  21088  rescon  23188  cvmsss2  23216  cvmliftlem10  23236  dfrtrcl2  23456  axlowdim  24000  cgrextend  24042  cgr3rflx  24088  cgrxfr  24089  btwnconn1lem4  24124  btwnconn1lem8  24128  btwnconn1lem11  24131  sqpre  24650  truni3  24919  efilcp  24964  fgsb2  24967  tcnvec  25102  icccon3  25113  idcatfun  25353  rocatval  25371  clscnc  25422  isbnd3  25920  prdsbnd  25929  rngohomco  26017  rngoisocnv  26024  rngoidl  26061  0idl  26062  intidl  26066  unichnidl  26068  keridl  26069  smprngopr  26089  modelico  26318  issubmd  26795  mon1psubm  26937  lshpnel2N  28548  lkrshp  28668  4atexlemex2  29633  4atex  29638  cdleme0moN  29787  istendod  30324  dihlspsnat  30896  dochsatshp  31014
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