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

Theorem mpbir3and 1339
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 1125 . 2 (𝜑 → (𝜒𝜃𝜏))
5 mpbir3and.4 . 2 (𝜑 → (𝜓 ↔ (𝜒𝜃𝜏)))
64, 5mpbird 260 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  w3a 1084
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 210  df-an 400  df-3an 1086
This theorem is referenced by:  canthwelem  10070  intwun  10155  tskwun  10204  gruwun  10233  ixxss1  12753  ixxss2  12754  ixxss12  12755  ixxub  12756  ixxlb  12757  elicod  12784  ubioc1  12787  lbico1  12788  lbicc2  12851  ubicc2  12852  difreicc  12871  supicc  12888  modelico  13253  zmodfz  13265  addmodid  13291  dfrtrcl2  14421  phicl2  16103  4sqlem12  16290  isfuncd  17135  idfucl  17151  cofucl  17158  invfuc  17244  cnvps  17822  psss  17824  issubmd  17971  mndissubm  17972  submid  17975  subsubm  17981  0subm  17982  mhmima  17989  mhmeql  17990  gsumwspan  18011  frmdsssubm  18026  sursubmefmnd  18061  injsubmefmnd  18062  issubgrpd2  18295  grpissubg  18299  subgint  18303  0subg  18304  nmzsubg  18317  eqger  18330  eqgcpbl  18334  cycsubm  18345  cycsubgcl  18349  ghmrn  18371  ghmpreima  18380  gastacl  18439  cntzsubm  18466  sylow2blem1  18745  lsmsubm  18778  torsubg  18974  oddvdssubg  18975  dmdprdd  19121  dprdsubg  19146  dprdres  19150  unitsubm  19423  subrgsubm  19548  subrgugrp  19554  subrgint  19557  issubdrg  19560  cntzsubr  19568  lsssubg  19729  islmhm2  19810  pj1lmhm  19872  islbs2  19926  islbs3  19927  lbsextlem4  19933  issubrngd2  19961  lidlsubg  19988  2idlcpbl  20007  isphld  20350  mplsubglem  20679  mplsubrg  20685  mplind  20748  mhpsubg  20808  dmatsgrp  21111  dmatsrng  21113  scmatsgrp  21131  scmatsrng  21132  scmatsgrp1  21134  scmatsrng1  21135  cpmatsubgpmat  21331  cpmatsrgpmat  21332  lmcnp  21915  isufil2  22519  ufileu  22530  filufint  22531  fmfnfm  22569  flimclslem  22595  fclsfnflim  22638  flimfnfcls  22639  fclscmp  22641  clssubg  22720  tgpconncompeqg  22723  tgpconncomp  22724  qustgpopn  22731  tgptsmscls  22761  xmeter  23046  metust  23171  tgqioo  23411  zcld  23424  iccntr  23432  icccmplem2  23434  icccmplem3  23435  reconnlem1  23437  reconnlem2  23438  xrge0tsms  23445  cnheiborlem  23565  om1addcl  23644  pi1blem  23650  pi1grplem  23660  pi1inv  23663  pi1xfr  23666  pi1xfrcnvlem  23667  pi1coghm  23672  cmetcaulem  23898  ivthlem2  24062  ivthlem3  24063  ovolicc2lem2  24128  ovolicc2lem5  24131  opnmbllem  24211  volcn  24216  ismbf3d  24264  mbfi1fseqlem6  24330  itg2const2  24351  i1fibl  24417  ibladd  24430  bddiblnc  24451  ditgsplitlem  24469  dvferm1lem  24593  dvferm2lem  24595  dvlip2  24604  dvivthlem1  24617  dvne0  24620  lhop1lem  24622  lhop1  24623  lhop  24625  dvcnvrelem1  24626  dvcnvrelem2  24627  dvcnvre  24628  ftc1lem1  24644  itgsubst  24658  aaliou3lem2  24945  psercnlem2  25025  efif1olem2  25141  logtayl  25257  log2tlbnd  25537  xrlimcnp  25560  pntibndlem2  26181  pntlemj  26193  pntleml  26201  trgcgr  26316  hlid  26409  hltr  26410  btwnhl1  26412  btwnhl2  26413  hlcgrex  26416  mirhl  26479  mirbtwnhl  26480  mirhl2  26481  hlpasch  26556  lnopp2hpgb  26563  cgrahl  26627  axlowdim  26761  uhgrissubgr  27071  egrsubgr  27073  uhgrspansubgr  27087  uhgrspan1  27099  cusgrrusgr  27377  wlkonwlk  27458  wlkonwlk1l  27459  wlkres  27466  wlkp1  27477  wlkd  27482  lfgriswlk  27484  wwlksnextinj  27691  2wlkond  27729  wpthswwlks2on  27753  0wlkon  27911  1wlkd  27932  1pthond  27935  eliccelico  30514  elicoelioo  30515  xrge0tsmsd  30727  tpr2rico  31215  measinb  31540  cntmeas  31545  dya2icoseg  31595  sibf0  31652  sibfof  31658  pfxwlk  32430  revwlk  32431  resconn  32553  cvmsss2  32581  cvmliftlem10  32601  mrsubco  32828  cgrextend  33529  cgr3rflx  33575  cgrxfr  33576  btwnconn1lem4  33611  btwnconn1lem8  33615  btwnconn1lem11  33618  bj-pinftynminfty  34590  bj-rveccmod  34664  iooelexlt  34727  opnmbllem0  35041  ibladdnc  35062  ftc1anc  35086  isbnd3  35170  prdsbnd  35179  rngomndo  35321  isgrpda  35341  rngohomco  35360  rngoisocnv  35367  rngoidl  35410  0idl  35411  intidl  35415  unichnidl  35417  keridl  35418  smprngopr  35438  lshpnel2N  36229  lkrshp  36349  4atexlemex2  37315  4atex  37320  cdleme0moN  37469  istendod  38006  dihlspsnat  38577  dochsatshp  38695  mon1psubm  40070  iocinico  40082  dfrtrcl3  40354  eliood  42065  eliccd  42071  eliocd  42074  limciccioolb  42193  limcicciooub  42209  icccncfext  42459  iblspltprt  42545  itgspltprt  42551  fourierdlem1  42680  fourierdlem4  42683  fourierdlem32  42711  fourierdlem33  42712  fourierdlem43  42722  fourierdlem65  42743  fourierdlem79  42757  prsal  42890  issald  42903  iccpartrn  43877  fpprwpprb  44188  bgoldbtbnd  44257  expnegico01  44857  dignnld  44947  reorelicc  45054
  Copyright terms: Public domain W3C validator