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

Theorem mpbir3and 1177
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 1174 . 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 971
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 369  df-3an 973
This theorem is referenced by:  canthwelem  9017  intwun  9102  tskwun  9151  gruwun  9180  ixxss1  11550  ixxss2  11551  ixxss12  11552  ixxub  11553  ixxlb  11554  ubioc1  11581  lbico1  11582  lbicc2  11639  ubicc2  11640  difreicc  11655  supicc  11671  zmodfz  11999  dfrtrcl2  12977  phicl2  14382  4sqlem12  14558  isfuncd  15353  idfucl  15369  cofucl  15376  invfuc  15462  cnvps  16041  psss  16043  issubmd  16179  submid  16181  subsubm  16187  mhmima  16193  mhmeql  16194  gsumwspan  16213  frmdsssubm  16228  issubgrpd2  16416  grpissubg  16420  subgint  16424  0subg  16425  cycsubgcl  16426  nmzsubg  16441  eqger  16450  eqgcpbl  16454  ghmrn  16479  ghmpreima  16487  gastacl  16546  cntzsubm  16572  sylow2blem1  16839  lsmsubm  16872  torsubg  17059  oddvdssubg  17060  dmdprdd  17225  dprdwdOLD2  17240  dprdwdOLD  17246  dprdsubg  17266  dprdres  17270  unitsubm  17514  subrgsubm  17637  subrgugrp  17643  subrgint  17646  issubdrg  17649  cntzsubr  17656  lsssubg  17798  islmhm2  17879  pj1lmhm  17941  islbs2  17995  islbs3  17996  lbsextlem4  18002  issubrngd2  18030  lidlsubg  18057  2idlcpbl  18077  mplsubglem  18288  mplsubglemOLD  18290  mplsubrg  18297  mplind  18362  isphld  18862  dmatsgrp  19168  dmatsrng  19170  scmatsgrp  19188  scmatsrng  19189  scmatsgrp1  19191  scmatsrng1  19192  cpmatsubgpmat  19388  cpmatsrgpmat  19389  lmcnp  19972  isufil2  20575  ufileu  20586  filufint  20587  fmfnfm  20625  flimclslem  20651  fclsfnflim  20694  flimfnfcls  20695  fclscmp  20697  clssubg  20773  tgpconcompeqg  20776  tgpconcomp  20777  qustgpopn  20784  tgptsmscls  20818  xmeter  21102  metustOLD  21236  metust  21237  tgqioo  21471  zcld  21484  iccntr  21492  icccmplem2  21494  icccmplem3  21495  reconnlem1  21497  reconnlem2  21498  xrge0tsms  21505  cnheiborlem  21620  om1addcl  21699  pi1blem  21705  pi1grplem  21715  pi1inv  21718  pi1xfr  21721  pi1xfrcnvlem  21722  pi1coghm  21727  cmetcaulem  21893  ivthlem2  22030  ivthlem3  22031  ovolicc2lem2  22095  ovolicc2lem5  22098  opnmbllem  22176  volcn  22181  ismbf3d  22227  mbfi1fseqlem6  22293  itg2const2  22314  i1fibl  22380  ibladd  22393  ditgsplitlem  22430  dvferm1lem  22551  dvferm2lem  22553  dvlip2  22562  dvivthlem1  22575  dvne0  22578  lhop1lem  22580  lhop1  22581  lhop  22583  dvcnvrelem1  22584  dvcnvrelem2  22585  dvcnvre  22586  ftc1lem1  22602  itgsubst  22616  aaliou3lem2  22905  psercnlem2  22985  efif1olem2  23096  logtayl  23209  log2tlbnd  23473  xrlimcnp  23496  pntibndlem2  23974  pntlemj  23986  pntleml  23994  trgcgr  24108  axlowdim  24466  wlkonwlk  24739  0wlkon  24751  constr1trl  24792  constr2wlk  24802  constr2trl  24803  constr2pth  24805  2pthon  24806  wwlkextinj  24932  el2spthonot  25072  cusgraisrusgra  25140  extwwlkfablem1  25276  isgrp2d  25435  isgrpda  25497  rngomndo  25621  eliccelico  27822  elicoelioo  27823  xrge0tsmsd  28010  tpr2rico  28129  measinb  28429  cntmeas  28434  dya2icoseg  28485  sibf0  28540  sibfof  28546  rescon  28955  cvmsss2  28983  cvmliftlem10  29003  mrsubco  29145  cgrextend  29886  cgr3rflx  29932  cgrxfr  29933  btwnconn1lem4  29968  btwnconn1lem8  29972  btwnconn1lem11  29975  opnmbllem0  30290  dvtanlem  30304  ibladdnc  30312  bddiblnc  30325  ftc1anc  30338  isbnd3  30520  prdsbnd  30529  rngohomco  30617  rngoisocnv  30624  rngoidl  30661  0idl  30662  intidl  30666  unichnidl  30668  keridl  30669  smprngopr  30689  modelico  30996  mon1psubm  31407  iocinico  31420  eliood  31770  eliccd  31777  eliocd  31782  elicod  31790  limciccioolb  31866  limcicciooub  31882  icccncfext  31929  iblspltprt  32011  itgspltprt  32017  fourierdlem1  32129  fourierdlem4  32132  fourierdlem32  32160  fourierdlem33  32161  fourierdlem43  32171  fourierdlem65  32193  fourierdlem79  32207  expnegico01  33377  dignnld  33478  bj-pinftynminfty  35030  lshpnel2N  35107  lkrshp  35227  4atexlemex2  36192  4atex  36197  cdleme0moN  36347  istendod  36885  dihlspsnat  37457  dochsatshp  37575  dfrtrcl3  38214
  Copyright terms: Public domain W3C validator