MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpbir3and 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
mpbir3and.2
mpbir3and.3
mpbir3and.4
Assertion
Ref Expression
mpbir3and

Proof of Theorem mpbir3and
StepHypRef Expression
1 mpbir3and.1 . . 3
2 mpbir3and.2 . . 3
3 mpbir3and.3 . . 3
41, 2, 33jca 1176 . 2
5 mpbir3and.4 . 2
64, 5mpbird 232 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\w3a 973
This theorem is referenced by:  canthwelem  9049  intwun  9134  tskwun  9183  gruwun  9212  ixxss1  11576  ixxss2  11577  ixxss12  11578  ixxub  11579  ixxlb  11580  ubioc1  11607  lbico1  11608  lbicc2  11665  ubicc2  11666  difreicc  11681  supicc  11697  zmodfz  12017  phicl2  14298  4sqlem12  14474  isfuncd  15234  idfucl  15250  cofucl  15257  invfuc  15343  cnvps  15842  psss  15844  issubmd  15980  submid  15982  subsubm  15988  mhmima  15994  mhmeql  15995  gsumwspan  16014  frmdsssubm  16029  issubgrpd2  16217  grpissubg  16221  subgint  16225  0subg  16226  cycsubgcl  16227  nmzsubg  16242  eqger  16251  eqgcpbl  16255  ghmrn  16280  ghmpreima  16288  gastacl  16347  cntzsubm  16373  sylow2blem1  16640  lsmsubm  16673  torsubg  16860  oddvdssubg  16861  dmdprdd  17030  dprdwdOLD2  17045  dprdwdOLD  17051  dprdsubg  17071  dprdres  17075  unitsubm  17319  subrgsubm  17442  subrgugrp  17448  subrgint  17451  issubdrg  17454  cntzsubr  17461  lsssubg  17603  islmhm2  17684  pj1lmhm  17746  islbs2  17800  islbs3  17801  lbsextlem4  17807  issubrngd2  17835  lidlsubg  17862  2idlcpbl  17882  mplsubglem  18093  mplsubglemOLD  18095  mplsubrg  18102  mplind  18167  isphld  18689  dmatsgrp  19001  dmatsrng  19003  scmatsgrp  19021  scmatsrng  19022  scmatsgrp1  19024  scmatsrng1  19025  cpmatsubgpmat  19221  cpmatsrgpmat  19222  lmcnp  19805  isufil2  20409  ufileu  20420  filufint  20421  fmfnfm  20459  flimclslem  20485  fclsfnflim  20528  flimfnfcls  20529  fclscmp  20531  clssubg  20607  tgpconcompeqg  20610  tgpconcomp  20611  qustgpopn  20618  tgptsmscls  20652  xmeter  20936  metustOLD  21070  metust  21071  tgqioo  21305  zcld  21318  iccntr  21326  icccmplem2  21328  icccmplem3  21329  reconnlem1  21331  reconnlem2  21332  xrge0tsms  21339  cnheiborlem  21454  om1addcl  21533  pi1blem  21539  pi1grplem  21549  pi1inv  21552  pi1xfr  21555  pi1xfrcnvlem  21556  pi1coghm  21561  cmetcaulem  21727  ivthlem2  21864  ivthlem3  21865  ovolicc2lem2  21929  ovolicc2lem5  21932  opnmbllem  22010  volcn  22015  ismbf3d  22061  mbfi1fseqlem6  22127  itg2const2  22148  i1fibl  22214  ibladd  22227  ditgsplitlem  22264  dvferm1lem  22385  dvferm2lem  22387  dvlip2  22396  dvivthlem1  22409  dvne0  22412  lhop1lem  22414  lhop1  22415  lhop  22417  dvcnvrelem1  22418  dvcnvrelem2  22419  dvcnvre  22420  ftc1lem1  22436  itgsubst  22450  aaliou3lem2  22739  psercnlem2  22819  efif1olem2  22930  logtayl  23041  log2tlbnd  23276  xrlimcnp  23298  pntibndlem2  23776  pntlemj  23788  pntleml  23796  trgcgr  23907  axlowdim  24264  wlkonwlk  24537  0wlkon  24549  constr1trl  24590  constr2wlk  24600  constr2trl  24601  constr2pth  24603  2pthon  24604  wwlkextinj  24730  el2spthonot  24870  cusgraisrusgra  24938  extwwlkfablem1  25074  isgrp2d  25237  isgrpda  25299  rngomndo  25423  eliccelico  27588  elicoelioo  27589  xrge0tsmsd  27775  tpr2rico  27894  measinb  28192  cntmeas  28197  dya2icoseg  28248  sibf0  28276  sibfof  28282  rescon  28691  cvmsss2  28719  cvmliftlem10  28739  mrsubco  28881  dfrtrcl2  29071  cgrextend  29658  cgr3rflx  29704  cgrxfr  29705  btwnconn1lem4  29740  btwnconn1lem8  29744  btwnconn1lem11  29747  opnmbllem0  30050  dvtanlem  30064  ibladdnc  30072  bddiblnc  30085  ftc1anc  30098  isbnd3  30280  prdsbnd  30289  rngohomco  30377  rngoisocnv  30384  rngoidl  30421  0idl  30422  intidl  30426  unichnidl  30428  keridl  30429  smprngopr  30449  modelico  30757  mon1psubm  31166  iocinico  31179  eliood  31531  eliccd  31538  eliocd  31543  elicod  31551  limciccioolb  31627  limcicciooub  31643  icccncfext  31690  iblspltprt  31772  itgspltprt  31778  fourierdlem1  31890  fourierdlem4  31893  fourierdlem32  31921  fourierdlem33  31922  fourierdlem43  31932  fourierdlem65  31954  fourierdlem79  31968  bj-pinftynminfty  34630  lshpnel2N  34710  lkrshp  34830  4atexlemex2  35795  4atex  35800  cdleme0moN  35950  istendod  36488  dihlspsnat  37060  dochsatshp  37178
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
  Copyright terms: Public domain W3C validator