MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpbir3and 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  8481  intwun  8566  tskwun  8615  gruwun  8644  ixxss1  10890  ixxss2  10891  ixxss12  10892  ixxub  10893  ixxlb  10894  ubioc1  10921  lbico1  10922  lbicc2  10969  ubicc2  10970  difreicc  10984  zmodfz  11223  phicl2  13112  4sqlem12  13279  isfuncd  14017  idfucl  14033  cofucl  14040  invfuc  14126  cnvps  14599  psss  14601  submid  14706  subsubm  14712  mhmima  14718  mhmeql  14719  gsumwspan  14746  frmdsssubm  14761  subgint  14919  0subg  14920  cycsubgcl  14921  nmzsubg  14936  eqger  14945  eqgcpbl  14949  ghmrn  14974  ghmpreima  14982  gastacl  15041  cntzsubm  15089  sylow2blem1  15209  lsmsubm  15242  torsubg  15424  oddvdssubg  15425  dmdprdd  15515  dprdwd  15524  dprdsubg  15537  dprdres  15541  unitsubm  15730  subrgsubm  15836  subrgugrp  15842  subrgint  15845  issubdrg  15848  cntzsubr  15855  lsssubg  15988  islmhm2  16069  pj1lmhm  16127  islbs2  16181  islbs3  16182  lbsextlem4  16188  issubgrpd2  16215  issubrngd2  16217  lidlsubg  16241  2idlcpbl  16260  mplsubglem  16453  mplsubrg  16458  mplind  16517  isphld  16840  lmcnp  17322  isufil2  17893  ufileu  17904  filufint  17905  fmfnfm  17943  flimclslem  17969  fclsfnflim  18012  flimfnfcls  18013  fclscmp  18015  clssubg  18091  tgpconcompeqg  18094  tgpconcomp  18095  divstgpopn  18102  tgptsmscls  18132  xmeter  18416  metustOLD  18550  metust  18551  tgqioo  18784  zcld  18797  iccntr  18805  icccmplem2  18807  icccmplem3  18808  reconnlem1  18810  reconnlem2  18811  xrge0tsms  18818  cnheiborlem  18932  om1addcl  19011  pi1blem  19017  pi1grplem  19027  pi1inv  19030  pi1xfr  19033  pi1xfrcnvlem  19034  pi1coghm  19039  cmetcaulem  19194  ivthlem2  19302  ivthlem3  19303  ovolicc2lem2  19367  ovolicc2lem5  19370  opnmbllem  19446  volcn  19451  ismbf3d  19499  mbfi1fseqlem6  19565  itg2const2  19586  i1fibl  19652  ibladd  19665  ditgsplitlem  19700  dvferm1lem  19821  dvferm2lem  19823  dvlip2  19832  dvivthlem1  19845  dvne0  19848  lhop1lem  19850  lhop1  19851  lhop  19853  dvcnvrelem1  19854  dvcnvrelem2  19855  dvcnvre  19856  ftc1lem1  19872  itgsubst  19886  aaliou3lem2  20213  psercnlem2  20293  efif1olem2  20398  logtayl  20504  log2tlbnd  20738  xrlimcnp  20760  pntibndlem2  21238  pntlemj  21250  pntleml  21258  wlkonwlk  21488  0wlkon  21500  constr1trl  21541  constr2wlk  21551  constr2trl  21552  constr2pth  21554  2pthon  21555  isgrp2d  21776  isgrpda  21838  rngomndo  21962  eliccelico  24093  elicoelioo  24094  xrge0tsmsd  24176  tpr2rico  24263  measinb  24528  cntmeas  24533  dya2icoseg  24580  rescon  24886  cvmsss2  24914  cvmliftlem10  24934  dfrtrcl2  25101  axlowdim  25804  cgrextend  25846  cgr3rflx  25892  cgrxfr  25893  btwnconn1lem4  25928  btwnconn1lem8  25932  btwnconn1lem11  25935  mblfinlem  26143  ibladdnc  26161  bddiblnc  26174  isbnd3  26383  prdsbnd  26392  rngohomco  26480  rngoisocnv  26487  rngoidl  26524  0idl  26525  intidl  26529  unichnidl  26531  keridl  26532  smprngopr  26552  modelico  26774  issubmd  27251  mon1psubm  27393  lshpnel2N  29468  lkrshp  29588  4atexlemex2  30553  4atex  30558  cdleme0moN  30707  istendod  31244  dihlspsnat  31816  dochsatshp  31934
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