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

Theorem mpbir3and 1179
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 1176 . 2  |-  ( ph  ->  ( ch  /\  th  /\  ta ) )
5 mpbir3and.4 . 2  |-  ( ph  ->  ( ps  <->  ( ch  /\ 
th  /\  ta )
) )
64, 5mpbird 232 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ w3a 973
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 185  df-an 371  df-3an 975
This theorem is referenced by:  canthwelem  9028  intwun  9113  tskwun  9162  gruwun  9191  ixxss1  11547  ixxss2  11548  ixxss12  11549  ixxub  11550  ixxlb  11551  ubioc1  11578  lbico1  11579  lbicc2  11636  ubicc2  11637  difreicc  11652  zmodfz  11985  phicl2  14157  4sqlem12  14333  isfuncd  15092  idfucl  15108  cofucl  15115  invfuc  15201  cnvps  15699  psss  15701  issubmd  15799  submid  15801  subsubm  15807  mhmima  15813  mhmeql  15814  gsumwspan  15846  frmdsssubm  15861  issubgrpd2  16022  subgint  16030  0subg  16031  cycsubgcl  16032  nmzsubg  16047  eqger  16056  eqgcpbl  16060  ghmrn  16085  ghmpreima  16093  gastacl  16152  cntzsubm  16178  sylow2blem1  16446  lsmsubm  16479  torsubg  16663  oddvdssubg  16664  dmdprdd  16833  dprdwd  16847  dprdwdOLD  16853  dprdsubg  16873  dprdres  16877  unitsubm  17120  subrgsubm  17242  subrgugrp  17248  subrgint  17251  issubdrg  17254  cntzsubr  17261  lsssubg  17403  islmhm2  17484  pj1lmhm  17546  islbs2  17600  islbs3  17601  lbsextlem4  17607  issubrngd2  17635  lidlsubg  17662  2idlcpbl  17681  mplsubglem  17892  mplsubglemOLD  17894  mplsubrg  17901  mplind  17966  isphld  18484  dmatsgrp  18796  dmatsrng  18798  scmatsgrp  18816  scmatsrng  18817  scmatsgrp1  18819  scmatsrng1  18820  cpmatsubgpmat  19016  cpmatsrgpmat  19017  lmcnp  19599  isufil2  20172  ufileu  20183  filufint  20184  fmfnfm  20222  flimclslem  20248  fclsfnflim  20291  flimfnfcls  20292  fclscmp  20294  clssubg  20370  tgpconcompeqg  20373  tgpconcomp  20374  divstgpopn  20381  tgptsmscls  20415  xmeter  20699  metustOLD  20833  metust  20834  tgqioo  21068  zcld  21081  iccntr  21089  icccmplem2  21091  icccmplem3  21092  reconnlem1  21094  reconnlem2  21095  xrge0tsms  21102  cnheiborlem  21217  om1addcl  21296  pi1blem  21302  pi1grplem  21312  pi1inv  21315  pi1xfr  21318  pi1xfrcnvlem  21319  pi1coghm  21324  cmetcaulem  21490  ivthlem2  21627  ivthlem3  21628  ovolicc2lem2  21692  ovolicc2lem5  21695  opnmbllem  21773  volcn  21778  ismbf3d  21824  mbfi1fseqlem6  21890  itg2const2  21911  i1fibl  21977  ibladd  21990  ditgsplitlem  22027  dvferm1lem  22148  dvferm2lem  22150  dvlip2  22159  dvivthlem1  22172  dvne0  22175  lhop1lem  22177  lhop1  22178  lhop  22180  dvcnvrelem1  22181  dvcnvrelem2  22182  dvcnvre  22183  ftc1lem1  22199  itgsubst  22213  aaliou3lem2  22501  psercnlem2  22581  efif1olem2  22691  logtayl  22797  log2tlbnd  23032  xrlimcnp  23054  pntibndlem2  23532  pntlemj  23544  pntleml  23552  axlowdim  23968  wlkonwlk  24241  0wlkon  24253  constr1trl  24294  constr2wlk  24304  constr2trl  24305  constr2pth  24307  2pthon  24308  wwlkextinj  24434  cusgraisrusgra  24642  extwwlkfablem1  24779  isgrp2d  24941  isgrpda  25003  rngomndo  25127  eliccelico  27284  elicoelioo  27285  xrge0tsmsd  27466  tpr2rico  27558  measinb  27860  cntmeas  27865  dya2icoseg  27916  rescon  28359  cvmsss2  28387  cvmliftlem10  28407  dfrtrcl2  28574  cgrextend  29263  cgr3rflx  29309  cgrxfr  29310  btwnconn1lem4  29345  btwnconn1lem8  29349  btwnconn1lem11  29352  opnmbllem0  29655  dvtanlem  29669  ibladdnc  29677  bddiblnc  29690  ftc1anc  29703  isbnd3  29911  prdsbnd  29920  rngohomco  30008  rngoisocnv  30015  rngoidl  30052  0idl  30053  intidl  30057  unichnidl  30059  keridl  30060  smprngopr  30080  modelico  30389  mon1psubm  30799  iocinico  30812  bj-pinftynminfty  33720  lshpnel2N  33800  lkrshp  33920  4atexlemex2  34885  4atex  34890  cdleme0moN  35039  istendod  35576  dihlspsnat  36148  dochsatshp  36266
  Copyright terms: Public domain W3C validator