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

Theorem mpbir3and 1178
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 1175 . 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 972
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 974
This theorem is referenced by:  canthwelem  9026  intwun  9111  tskwun  9160  gruwun  9189  ixxss1  11551  ixxss2  11552  ixxss12  11553  ixxub  11554  ixxlb  11555  ubioc1  11582  lbico1  11583  lbicc2  11640  ubicc2  11641  difreicc  11656  supicc  11672  zmodfz  11991  phicl2  14170  4sqlem12  14346  isfuncd  15103  idfucl  15119  cofucl  15126  invfuc  15212  cnvps  15711  psss  15713  issubmd  15849  submid  15851  subsubm  15857  mhmima  15863  mhmeql  15864  gsumwspan  15883  frmdsssubm  15898  issubgrpd2  16086  grpissubg  16090  subgint  16094  0subg  16095  cycsubgcl  16096  nmzsubg  16111  eqger  16120  eqgcpbl  16124  ghmrn  16149  ghmpreima  16157  gastacl  16216  cntzsubm  16242  sylow2blem1  16509  lsmsubm  16542  torsubg  16729  oddvdssubg  16730  dmdprdd  16899  dprdwd  16913  dprdwdOLD  16919  dprdsubg  16939  dprdres  16943  unitsubm  17187  subrgsubm  17310  subrgugrp  17316  subrgint  17319  issubdrg  17322  cntzsubr  17329  lsssubg  17471  islmhm2  17552  pj1lmhm  17614  islbs2  17668  islbs3  17669  lbsextlem4  17675  issubrngd2  17703  lidlsubg  17730  2idlcpbl  17750  mplsubglem  17961  mplsubglemOLD  17963  mplsubrg  17970  mplind  18035  isphld  18556  dmatsgrp  18868  dmatsrng  18870  scmatsgrp  18888  scmatsrng  18889  scmatsgrp1  18891  scmatsrng1  18892  cpmatsubgpmat  19088  cpmatsrgpmat  19089  lmcnp  19671  isufil2  20275  ufileu  20286  filufint  20287  fmfnfm  20325  flimclslem  20351  fclsfnflim  20394  flimfnfcls  20395  fclscmp  20397  clssubg  20473  tgpconcompeqg  20476  tgpconcomp  20477  qustgpopn  20484  tgptsmscls  20518  xmeter  20802  metustOLD  20936  metust  20937  tgqioo  21171  zcld  21184  iccntr  21192  icccmplem2  21194  icccmplem3  21195  reconnlem1  21197  reconnlem2  21198  xrge0tsms  21205  cnheiborlem  21320  om1addcl  21399  pi1blem  21405  pi1grplem  21415  pi1inv  21418  pi1xfr  21421  pi1xfrcnvlem  21422  pi1coghm  21427  cmetcaulem  21593  ivthlem2  21730  ivthlem3  21731  ovolicc2lem2  21795  ovolicc2lem5  21798  opnmbllem  21876  volcn  21881  ismbf3d  21927  mbfi1fseqlem6  21993  itg2const2  22014  i1fibl  22080  ibladd  22093  ditgsplitlem  22130  dvferm1lem  22251  dvferm2lem  22253  dvlip2  22262  dvivthlem1  22275  dvne0  22278  lhop1lem  22280  lhop1  22281  lhop  22283  dvcnvrelem1  22284  dvcnvrelem2  22285  dvcnvre  22286  ftc1lem1  22302  itgsubst  22316  aaliou3lem2  22604  psercnlem2  22684  efif1olem2  22795  logtayl  22906  log2tlbnd  23141  xrlimcnp  23163  pntibndlem2  23641  pntlemj  23653  pntleml  23661  trgcgr  23772  axlowdim  24129  wlkonwlk  24402  0wlkon  24414  constr1trl  24455  constr2wlk  24465  constr2trl  24466  constr2pth  24468  2pthon  24469  wwlkextinj  24595  el2spthonot  24735  cusgraisrusgra  24803  extwwlkfablem1  24939  isgrp2d  25102  isgrpda  25164  rngomndo  25288  eliccelico  27453  elicoelioo  27454  xrge0tsmsd  27641  tpr2rico  27760  measinb  28058  cntmeas  28063  dya2icoseg  28114  sibf0  28142  sibfof  28148  rescon  28557  cvmsss2  28585  cvmliftlem10  28605  mrsubco  28747  dfrtrcl2  28937  cgrextend  29626  cgr3rflx  29672  cgrxfr  29673  btwnconn1lem4  29708  btwnconn1lem8  29712  btwnconn1lem11  29715  opnmbllem0  30018  dvtanlem  30032  ibladdnc  30040  bddiblnc  30053  ftc1anc  30066  isbnd3  30248  prdsbnd  30257  rngohomco  30345  rngoisocnv  30352  rngoidl  30389  0idl  30390  intidl  30394  unichnidl  30396  keridl  30397  smprngopr  30417  modelico  30725  mon1psubm  31135  iocinico  31148  eliood  31463  eliccd  31470  eliocd  31475  elicod  31483  limciccioolb  31531  limcicciooub  31547  icccncfext  31593  iblspltprt  31658  itgspltprt  31664  fourierdlem1  31775  fourierdlem4  31778  fourierdlem32  31806  fourierdlem33  31807  fourierdlem43  31817  fourierdlem65  31839  fourierdlem79  31853  bj-pinftynminfty  34332  lshpnel2N  34412  lkrshp  34532  4atexlemex2  35497  4atex  35502  cdleme0moN  35652  istendod  36190  dihlspsnat  36762  dochsatshp  36880
  Copyright terms: Public domain W3C validator