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

Theorem mpbir3and 1264
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 1261 . 2 (𝜑 → (𝜒𝜃𝜏))
5 mpbir3and.4 . 2 (𝜑 → (𝜓 ↔ (𝜒𝜃𝜏)))
64, 5mpbird 247 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  w3a 1054
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 197  df-an 385  df-3an 1056
This theorem is referenced by:  canthwelem  9510  intwun  9595  tskwun  9644  gruwun  9673  ixxss1  12231  ixxss2  12232  ixxss12  12233  ixxub  12234  ixxlb  12235  elicod  12262  ubioc1  12265  lbico1  12266  lbicc2  12326  ubicc2  12327  difreicc  12342  supicc  12358  modelico  12720  zmodfz  12732  addmodid  12758  dfrtrcl2  13846  phicl2  15520  4sqlem12  15707  isfuncd  16572  idfucl  16588  cofucl  16595  invfuc  16681  cnvps  17259  psss  17261  issubmd  17396  submid  17398  subsubm  17404  mhmima  17410  mhmeql  17411  gsumwspan  17430  frmdsssubm  17445  issubgrpd2  17657  grpissubg  17661  subgint  17665  0subg  17666  cycsubgcl  17667  nmzsubg  17682  eqger  17691  eqgcpbl  17695  ghmrn  17720  ghmpreima  17729  gastacl  17788  cntzsubm  17814  sylow2blem1  18081  lsmsubm  18114  torsubg  18303  oddvdssubg  18304  dmdprdd  18444  dprdsubg  18469  dprdres  18473  unitsubm  18716  subrgsubm  18841  subrgugrp  18847  subrgint  18850  issubdrg  18853  cntzsubr  18860  lsssubg  19005  islmhm2  19086  pj1lmhm  19148  islbs2  19202  islbs3  19203  lbsextlem4  19209  issubrngd2  19237  lidlsubg  19263  2idlcpbl  19282  mplsubglem  19482  mplsubrg  19488  mplind  19550  isphld  20047  dmatsgrp  20353  dmatsrng  20355  scmatsgrp  20373  scmatsrng  20374  scmatsgrp1  20376  scmatsrng1  20377  cpmatsubgpmat  20573  cpmatsrgpmat  20574  lmcnp  21156  isufil2  21759  ufileu  21770  filufint  21771  fmfnfm  21809  flimclslem  21835  fclsfnflim  21878  flimfnfcls  21879  fclscmp  21881  clssubg  21959  tgpconncompeqg  21962  tgpconncomp  21963  qustgpopn  21970  tgptsmscls  22000  xmeter  22285  metust  22410  tgqioo  22650  zcld  22663  iccntr  22671  icccmplem2  22673  icccmplem3  22674  reconnlem1  22676  reconnlem2  22677  xrge0tsms  22684  cnheiborlem  22800  om1addcl  22879  pi1blem  22885  pi1grplem  22895  pi1inv  22898  pi1xfr  22901  pi1xfrcnvlem  22902  pi1coghm  22907  cmetcaulem  23132  ivthlem2  23267  ivthlem3  23268  ovolicc2lem2  23332  ovolicc2lem5  23335  opnmbllem  23415  volcn  23420  ismbf3d  23466  mbfi1fseqlem6  23532  itg2const2  23553  i1fibl  23619  ibladd  23632  ditgsplitlem  23669  dvferm1lem  23792  dvferm2lem  23794  dvlip2  23803  dvivthlem1  23816  dvne0  23819  lhop1lem  23821  lhop1  23822  lhop  23824  dvcnvrelem1  23825  dvcnvrelem2  23826  dvcnvre  23827  ftc1lem1  23843  itgsubst  23857  aaliou3lem2  24143  psercnlem2  24223  efif1olem2  24334  logtayl  24451  log2tlbnd  24717  xrlimcnp  24740  pntibndlem2  25325  pntlemj  25337  pntleml  25345  trgcgr  25456  axlowdim  25886  uhgrissubgr  26212  egrsubgr  26214  uhgrspansubgr  26228  uhgrspan1  26240  cusgrrusgr  26533  wlkonwlk  26614  wlkonwlk1l  26615  wlkres  26623  wlkp1  26634  wlkd  26639  lfgriswlk  26641  wwlksnextinj  26862  2wlkond  26902  wpthswwlks2on  26927  wpthswwlks2onOLD  26928  0wlkon  27098  1wlkd  27119  1pthond  27122  eliccelico  29667  elicoelioo  29668  xrge0tsmsd  29913  tpr2rico  30086  measinb  30412  cntmeas  30417  dya2icoseg  30467  sibf0  30524  sibfof  30530  resconn  31354  cvmsss2  31382  cvmliftlem10  31402  mrsubco  31544  cgrextend  32240  cgr3rflx  32286  cgrxfr  32287  btwnconn1lem4  32322  btwnconn1lem8  32326  btwnconn1lem11  32329  bj-pinftynminfty  33244  iooelexlt  33340  opnmbllem0  33575  ibladdnc  33597  bddiblnc  33610  ftc1anc  33623  isbnd3  33713  prdsbnd  33722  rngomndo  33864  isgrpda  33884  rngohomco  33903  rngoisocnv  33910  rngoidl  33953  0idl  33954  intidl  33958  unichnidl  33960  keridl  33961  smprngopr  33981  lshpnel2N  34590  lkrshp  34710  4atexlemex2  35675  4atex  35680  cdleme0moN  35830  istendod  36367  dihlspsnat  36939  dochsatshp  37057  mon1psubm  38101  iocinico  38114  dfrtrcl3  38342  eliood  40038  eliccd  40044  eliocd  40048  limciccioolb  40171  limcicciooub  40187  icccncfext  40418  iblspltprt  40507  itgspltprt  40513  fourierdlem1  40643  fourierdlem4  40646  fourierdlem32  40674  fourierdlem33  40675  fourierdlem43  40685  fourierdlem65  40706  fourierdlem79  40720  issald  40869  iccpartrn  41691  bgoldbtbnd  42022  expnegico01  42633  dignnld  42722
  Copyright terms: Public domain W3C validator