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

Theorem mpbir3and 1171
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 1168 . 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 965
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 967
This theorem is referenced by:  canthwelem  8817  intwun  8902  tskwun  8951  gruwun  8980  ixxss1  11318  ixxss2  11319  ixxss12  11320  ixxub  11321  ixxlb  11322  ubioc1  11349  lbico1  11350  lbicc2  11401  ubicc2  11402  difreicc  11417  zmodfz  11729  phicl2  13843  4sqlem12  14017  isfuncd  14775  idfucl  14791  cofucl  14798  invfuc  14884  cnvps  15382  psss  15384  issubmd  15477  submid  15479  subsubm  15485  mhmima  15491  mhmeql  15492  gsumwspan  15524  frmdsssubm  15539  issubgrpd2  15697  subgint  15705  0subg  15706  cycsubgcl  15707  nmzsubg  15722  eqger  15731  eqgcpbl  15735  ghmrn  15760  ghmpreima  15768  gastacl  15827  cntzsubm  15853  sylow2blem1  16119  lsmsubm  16152  torsubg  16336  oddvdssubg  16337  dmdprdd  16481  dprdwd  16495  dprdwdOLD  16501  dprdsubg  16521  dprdres  16525  unitsubm  16762  subrgsubm  16878  subrgugrp  16884  subrgint  16887  issubdrg  16890  cntzsubr  16897  lsssubg  17038  islmhm2  17119  pj1lmhm  17181  islbs2  17235  islbs3  17236  lbsextlem4  17242  issubrngd2  17270  lidlsubg  17297  2idlcpbl  17316  mplsubglem  17510  mplsubglemOLD  17512  mplsubrg  17519  mplind  17584  isphld  18083  lmcnp  18908  isufil2  19481  ufileu  19492  filufint  19493  fmfnfm  19531  flimclslem  19557  fclsfnflim  19600  flimfnfcls  19601  fclscmp  19603  clssubg  19679  tgpconcompeqg  19682  tgpconcomp  19683  divstgpopn  19690  tgptsmscls  19724  xmeter  20008  metustOLD  20142  metust  20143  tgqioo  20377  zcld  20390  iccntr  20398  icccmplem2  20400  icccmplem3  20401  reconnlem1  20403  reconnlem2  20404  xrge0tsms  20411  cnheiborlem  20526  om1addcl  20605  pi1blem  20611  pi1grplem  20621  pi1inv  20624  pi1xfr  20627  pi1xfrcnvlem  20628  pi1coghm  20633  cmetcaulem  20799  ivthlem2  20936  ivthlem3  20937  ovolicc2lem2  21001  ovolicc2lem5  21004  opnmbllem  21081  volcn  21086  ismbf3d  21132  mbfi1fseqlem6  21198  itg2const2  21219  i1fibl  21285  ibladd  21298  ditgsplitlem  21335  dvferm1lem  21456  dvferm2lem  21458  dvlip2  21467  dvivthlem1  21480  dvne0  21483  lhop1lem  21485  lhop1  21486  lhop  21488  dvcnvrelem1  21489  dvcnvrelem2  21490  dvcnvre  21491  ftc1lem1  21507  itgsubst  21521  aaliou3lem2  21809  psercnlem2  21889  efif1olem2  21999  logtayl  22105  log2tlbnd  22340  xrlimcnp  22362  pntibndlem2  22840  pntlemj  22852  pntleml  22860  axlowdim  23207  wlkonwlk  23434  0wlkon  23446  constr1trl  23487  constr2wlk  23497  constr2trl  23498  constr2pth  23500  2pthon  23501  isgrp2d  23722  isgrpda  23784  rngomndo  23908  eliccelico  26067  elicoelioo  26068  xrge0tsmsd  26253  tpr2rico  26342  measinb  26635  cntmeas  26640  dya2icoseg  26692  rescon  27135  cvmsss2  27163  cvmliftlem10  27183  dfrtrcl2  27350  cgrextend  28039  cgr3rflx  28085  cgrxfr  28086  btwnconn1lem4  28121  btwnconn1lem8  28125  btwnconn1lem11  28128  opnmbllem0  28427  dvtanlem  28441  ibladdnc  28449  bddiblnc  28462  ftc1anc  28475  isbnd3  28683  prdsbnd  28692  rngohomco  28780  rngoisocnv  28787  rngoidl  28824  0idl  28825  intidl  28829  unichnidl  28831  keridl  28832  smprngopr  28852  modelico  29162  mon1psubm  29574  iocinico  29587  wwlkextinj  30362  cusgraisrusgra  30551  extwwlkfablem1  30667  dmatsgrp  30878  dmatsrng  30880  scmatsgrp  30885  scmatsrng  30887  scmatsgrp1  30889  scmatsrng1  30890  bj-pinftynminfty  32550  lshpnel2N  32630  lkrshp  32750  4atexlemex2  33715  4atex  33720  cdleme0moN  33869  istendod  34406  dihlspsnat  34978  dochsatshp  35096
  Copyright terms: Public domain W3C validator