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

Theorem mpbir3and 1237
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 1234 . 2 (𝜑 → (𝜒𝜃𝜏))
5 mpbir3and.4 . 2 (𝜑 → (𝜓 ↔ (𝜒𝜃𝜏)))
64, 5mpbird 245 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  canthwelem  9328  intwun  9413  tskwun  9462  gruwun  9491  ixxss1  12020  ixxss2  12021  ixxss12  12022  ixxub  12023  ixxlb  12024  elicod  12051  ubioc1  12054  lbico1  12055  lbicc2  12115  ubicc2  12116  difreicc  12131  supicc  12147  modelico  12497  zmodfz  12509  addmodid  12535  dfrtrcl2  13596  phicl2  15257  4sqlem12  15444  isfuncd  16294  idfucl  16310  cofucl  16317  invfuc  16403  cnvps  16981  psss  16983  issubmd  17118  submid  17120  subsubm  17126  mhmima  17132  mhmeql  17133  gsumwspan  17152  frmdsssubm  17167  issubgrpd2  17379  grpissubg  17383  subgint  17387  0subg  17388  cycsubgcl  17389  nmzsubg  17404  eqger  17413  eqgcpbl  17417  ghmrn  17442  ghmpreima  17451  gastacl  17511  cntzsubm  17537  sylow2blem1  17804  lsmsubm  17837  torsubg  18026  oddvdssubg  18027  dmdprdd  18167  dprdsubg  18192  dprdres  18196  unitsubm  18439  subrgsubm  18562  subrgugrp  18568  subrgint  18571  issubdrg  18574  cntzsubr  18581  lsssubg  18724  islmhm2  18805  pj1lmhm  18867  islbs2  18921  islbs3  18922  lbsextlem4  18928  issubrngd2  18956  lidlsubg  18982  2idlcpbl  19001  mplsubglem  19201  mplsubrg  19207  mplind  19269  isphld  19763  dmatsgrp  20066  dmatsrng  20068  scmatsgrp  20086  scmatsrng  20087  scmatsgrp1  20089  scmatsrng1  20090  cpmatsubgpmat  20286  cpmatsrgpmat  20287  lmcnp  20860  isufil2  21464  ufileu  21475  filufint  21476  fmfnfm  21514  flimclslem  21540  fclsfnflim  21583  flimfnfcls  21584  fclscmp  21586  clssubg  21664  tgpconcompeqg  21667  tgpconcomp  21668  qustgpopn  21675  tgptsmscls  21705  xmeter  21989  metust  22114  tgqioo  22343  zcld  22356  iccntr  22364  icccmplem2  22366  icccmplem3  22367  reconnlem1  22369  reconnlem2  22370  xrge0tsms  22377  cnheiborlem  22492  om1addcl  22572  pi1blem  22578  pi1grplem  22588  pi1inv  22591  pi1xfr  22594  pi1xfrcnvlem  22595  pi1coghm  22600  cmetcaulem  22812  ivthlem2  22945  ivthlem3  22946  ovolicc2lem2  23010  ovolicc2lem5  23013  opnmbllem  23092  volcn  23097  ismbf3d  23144  mbfi1fseqlem6  23210  itg2const2  23231  i1fibl  23297  ibladd  23310  ditgsplitlem  23347  dvferm1lem  23468  dvferm2lem  23470  dvlip2  23479  dvivthlem1  23492  dvne0  23495  lhop1lem  23497  lhop1  23498  lhop  23500  dvcnvrelem1  23501  dvcnvrelem2  23502  dvcnvre  23503  ftc1lem1  23519  itgsubst  23533  aaliou3lem2  23819  psercnlem2  23899  efif1olem2  24010  logtayl  24123  log2tlbnd  24389  xrlimcnp  24412  pntibndlem2  24997  pntlemj  25009  pntleml  25017  trgcgr  25129  axlowdim  25559  wlkonwlk  25831  0wlkon  25843  constr1trl  25884  constr2wlk  25894  constr2trl  25895  constr2pth  25897  2pthon  25898  wwlkextinj  26024  el2spthonot  26163  cusgraisrusgra  26231  extwwlkfablem1  26367  eliccelico  28735  elicoelioo  28736  xrge0tsmsd  28922  tpr2rico  29092  measinb  29417  cntmeas  29422  dya2icoseg  29472  sibf0  29529  sibfof  29535  rescon  30288  cvmsss2  30316  cvmliftlem10  30336  mrsubco  30478  cgrextend  31091  cgr3rflx  31137  cgrxfr  31138  btwnconn1lem4  31173  btwnconn1lem8  31177  btwnconn1lem11  31180  bj-pinftynminfty  32087  iooelexlt  32182  opnmbllem0  32411  ibladdnc  32433  bddiblnc  32446  ftc1anc  32459  isbnd3  32549  prdsbnd  32558  rngomndo  32700  isgrpda  32720  rngohomco  32739  rngoisocnv  32746  rngoidl  32789  0idl  32790  intidl  32794  unichnidl  32796  keridl  32797  smprngopr  32817  lshpnel2N  33086  lkrshp  33206  4atexlemex2  34171  4atex  34176  cdleme0moN  34326  istendod  34864  dihlspsnat  35436  dochsatshp  35554  mon1psubm  36599  iocinico  36612  dfrtrcl3  36840  eliood  38364  eliccd  38370  eliocd  38374  limciccioolb  38485  limcicciooub  38501  icccncfext  38570  iblspltprt  38662  itgspltprt  38668  fourierdlem1  38798  fourierdlem4  38801  fourierdlem32  38829  fourierdlem33  38830  fourierdlem43  38840  fourierdlem65  38861  fourierdlem79  38875  iccpartrn  39766  bgoldbtbnd  40023  uhgrissubgr  40494  egrsubgr  40496  uhgrspansubgr  40510  uhgrspan1  40522  nbgr2vtx1edg  40567  nbuhgr2vtx1edgb  40569  cusgrexi  40657  cusgrrusgr  40776  wlkOnwlk  40865  wlkOnwlk1l  40866  1wlkres  40874  1wlkp1  40885  1wlkd  40890  lfgriswlk  40892  pthd  40970  wwlksnextinj  41100  21wlkond  41139  wpthswwlks2on  41159  0wlkOn  41283  11wlkd  41303  1pthd  41305  1pthond  41306  expnegico01  42097  dignnld  42190
  Copyright terms: Public domain W3C validator