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

Theorem mpbir3and 1166
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 1163 . 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 960
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 962
This theorem is referenced by:  canthwelem  8809  intwun  8894  tskwun  8943  gruwun  8972  ixxss1  11310  ixxss2  11311  ixxss12  11312  ixxub  11313  ixxlb  11314  ubioc1  11341  lbico1  11342  lbicc2  11392  ubicc2  11393  difreicc  11408  zmodfz  11717  phicl2  13830  4sqlem12  14004  isfuncd  14762  idfucl  14778  cofucl  14785  invfuc  14871  cnvps  15369  psss  15371  issubmd  15463  submid  15465  subsubm  15471  mhmima  15477  mhmeql  15478  gsumwspan  15508  frmdsssubm  15523  issubgrpd2  15681  subgint  15689  0subg  15690  cycsubgcl  15691  nmzsubg  15706  eqger  15715  eqgcpbl  15719  ghmrn  15744  ghmpreima  15752  gastacl  15811  cntzsubm  15837  sylow2blem1  16103  lsmsubm  16136  torsubg  16320  oddvdssubg  16321  dmdprdd  16459  dprdwd  16473  dprdwdOLD  16479  dprdsubg  16499  dprdres  16503  unitsubm  16700  subrgsubm  16806  subrgugrp  16812  subrgint  16815  issubdrg  16818  cntzsubr  16825  lsssubg  16964  islmhm2  17045  pj1lmhm  17107  islbs2  17161  islbs3  17162  lbsextlem4  17168  issubrngd2  17196  lidlsubg  17223  2idlcpbl  17242  mplsubglem  17448  mplsubglemOLD  17450  mplsubrg  17457  mplind  17520  isphld  17929  lmcnp  18754  isufil2  19327  ufileu  19338  filufint  19339  fmfnfm  19377  flimclslem  19403  fclsfnflim  19446  flimfnfcls  19447  fclscmp  19449  clssubg  19525  tgpconcompeqg  19528  tgpconcomp  19529  divstgpopn  19536  tgptsmscls  19570  xmeter  19854  metustOLD  19988  metust  19989  tgqioo  20223  zcld  20236  iccntr  20244  icccmplem2  20246  icccmplem3  20247  reconnlem1  20249  reconnlem2  20250  xrge0tsms  20257  cnheiborlem  20372  om1addcl  20451  pi1blem  20457  pi1grplem  20467  pi1inv  20470  pi1xfr  20473  pi1xfrcnvlem  20474  pi1coghm  20479  cmetcaulem  20645  ivthlem2  20782  ivthlem3  20783  ovolicc2lem2  20847  ovolicc2lem5  20850  opnmbllem  20927  volcn  20932  ismbf3d  20978  mbfi1fseqlem6  21044  itg2const2  21065  i1fibl  21131  ibladd  21144  ditgsplitlem  21181  dvferm1lem  21302  dvferm2lem  21304  dvlip2  21313  dvivthlem1  21326  dvne0  21329  lhop1lem  21331  lhop1  21332  lhop  21334  dvcnvrelem1  21335  dvcnvrelem2  21336  dvcnvre  21337  ftc1lem1  21353  itgsubst  21367  aaliou3lem2  21698  psercnlem2  21778  efif1olem2  21888  logtayl  21994  log2tlbnd  22229  xrlimcnp  22251  pntibndlem2  22729  pntlemj  22741  pntleml  22749  axlowdim  23034  wlkonwlk  23261  0wlkon  23273  constr1trl  23314  constr2wlk  23324  constr2trl  23325  constr2pth  23327  2pthon  23328  isgrp2d  23549  isgrpda  23611  rngomndo  23735  eliccelico  25894  elicoelioo  25895  xrge0tsmsd  26110  tpr2rico  26200  measinb  26493  cntmeas  26498  dya2icoseg  26550  rescon  26987  cvmsss2  27015  cvmliftlem10  27035  dfrtrcl2  27201  cgrextend  27890  cgr3rflx  27936  cgrxfr  27937  btwnconn1lem4  27972  btwnconn1lem8  27976  btwnconn1lem11  27979  opnmbllem0  28275  dvtanlem  28289  ibladdnc  28297  bddiblnc  28310  ftc1anc  28323  isbnd3  28531  prdsbnd  28540  rngohomco  28628  rngoisocnv  28635  rngoidl  28672  0idl  28673  intidl  28677  unichnidl  28679  keridl  28680  smprngopr  28700  modelico  29011  mon1psubm  29423  iocinico  29436  wwlkextinj  30212  cusgraisrusgra  30401  extwwlkfablem1  30517  dmatsgrp  30692  dmatsrng  30694  scmatsgrp  30699  scmatsrng  30701  scmatsgrp1  30703  scmatsrng1  30704  bj-pinftynminfty  32193  lshpnel2N  32266  lkrshp  32386  4atexlemex2  33351  4atex  33356  cdleme0moN  33505  istendod  34042  dihlspsnat  34614  dochsatshp  34732
  Copyright terms: Public domain W3C validator