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

Theorem mpbir3and 1188
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 1185 . 2  |-  ( ph  ->  ( ch  /\  th  /\  ta ) )
5 mpbir3and.4 . 2  |-  ( ph  ->  ( ps  <->  ( ch  /\ 
th  /\  ta )
) )
64, 5mpbird 235 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  canthwelem  9074  intwun  9159  tskwun  9208  gruwun  9237  ixxss1  11653  ixxss2  11654  ixxss12  11655  ixxub  11656  ixxlb  11657  ixxlbOLD  11658  elicod  11685  ubioc1  11688  lbico1  11689  lbicc2  11746  ubicc2  11747  difreicc  11762  supicc  11778  zmodfz  12115  addmodid  12136  dfrtrcl2  13104  phicl2  14685  4sqlem12  14863  isfuncd  15721  idfucl  15737  cofucl  15744  invfuc  15830  cnvps  16409  psss  16411  issubmd  16547  submid  16549  subsubm  16555  mhmima  16561  mhmeql  16562  gsumwspan  16581  frmdsssubm  16596  issubgrpd2  16784  grpissubg  16788  subgint  16792  0subg  16793  cycsubgcl  16794  nmzsubg  16809  eqger  16818  eqgcpbl  16822  ghmrn  16847  ghmpreima  16855  gastacl  16914  cntzsubm  16940  sylow2blem1  17207  lsmsubm  17240  torsubg  17427  oddvdssubg  17428  dmdprdd  17566  dprdwdOLD  17579  dprdsubg  17592  dprdres  17596  unitsubm  17833  subrgsubm  17956  subrgugrp  17962  subrgint  17965  issubdrg  17968  cntzsubr  17975  lsssubg  18115  islmhm2  18196  pj1lmhm  18258  islbs2  18312  islbs3  18313  lbsextlem4  18319  issubrngd2  18347  lidlsubg  18373  2idlcpbl  18393  mplsubglem  18593  mplsubrg  18599  mplind  18660  isphld  19152  dmatsgrp  19455  dmatsrng  19457  scmatsgrp  19475  scmatsrng  19476  scmatsgrp1  19478  scmatsrng1  19479  cpmatsubgpmat  19675  cpmatsrgpmat  19676  lmcnp  20251  isufil2  20854  ufileu  20865  filufint  20866  fmfnfm  20904  flimclslem  20930  fclsfnflim  20973  flimfnfcls  20974  fclscmp  20976  clssubg  21054  tgpconcompeqg  21057  tgpconcomp  21058  qustgpopn  21065  tgptsmscls  21095  xmeter  21379  metust  21504  tgqioo  21729  zcld  21742  iccntr  21750  icccmplem2  21752  icccmplem3  21753  reconnlem1  21755  reconnlem2  21756  xrge0tsms  21763  cnheiborlem  21878  om1addcl  21957  pi1blem  21963  pi1grplem  21973  pi1inv  21976  pi1xfr  21979  pi1xfrcnvlem  21980  pi1coghm  21985  cmetcaulem  22151  ivthlem2  22284  ivthlem3  22285  ovolicc2lem2  22349  ovolicc2lem5  22352  opnmbllem  22436  volcn  22441  ismbf3d  22487  mbfi1fseqlem6  22555  itg2const2  22576  i1fibl  22642  ibladd  22655  ditgsplitlem  22692  dvferm1lem  22813  dvferm2lem  22815  dvlip2  22824  dvivthlem1  22837  dvne0  22840  lhop1lem  22842  lhop1  22843  lhop  22845  dvcnvrelem1  22846  dvcnvrelem2  22847  dvcnvre  22848  ftc1lem1  22864  itgsubst  22878  aaliou3lem2  23164  psercnlem2  23244  efif1olem2  23357  logtayl  23470  log2tlbnd  23736  xrlimcnp  23759  pntibndlem2  24292  pntlemj  24304  pntleml  24312  trgcgr  24423  axlowdim  24837  wlkonwlk  25110  0wlkon  25122  constr1trl  25163  constr2wlk  25173  constr2trl  25174  constr2pth  25176  2pthon  25177  wwlkextinj  25303  el2spthonot  25443  cusgraisrusgra  25511  extwwlkfablem1  25647  isgrp2d  25808  isgrpda  25870  rngomndo  25994  eliccelico  28195  elicoelioo  28196  xrge0tsmsd  28387  tpr2rico  28557  measinb  28882  cntmeas  28887  dya2icoseg  28938  sibf0  28995  sibfof  29001  rescon  29757  cvmsss2  29785  cvmliftlem10  29805  mrsubco  29947  cgrextend  30560  cgr3rflx  30606  cgrxfr  30607  btwnconn1lem4  30642  btwnconn1lem8  30646  btwnconn1lem11  30649  bj-pinftynminfty  31414  iooelexlt  31499  opnmbllem0  31680  dvtanlemOLD  31695  ibladdnc  31703  bddiblnc  31716  ftc1anc  31729  isbnd3  31820  prdsbnd  31829  rngohomco  31917  rngoisocnv  31924  rngoidl  31961  0idl  31962  intidl  31966  unichnidl  31968  keridl  31969  smprngopr  31989  lshpnel2N  32260  lkrshp  32380  4atexlemex2  33345  4atex  33350  cdleme0moN  33500  istendod  34038  dihlspsnat  34610  dochsatshp  34728  modelico  35375  mon1psubm  35782  iocinico  35795  dfrtrcl3  35964  eliood  37180  eliccd  37186  eliocd  37190  limciccioolb  37273  limcicciooub  37289  icccncfext  37337  iblspltprt  37419  itgspltprt  37425  fourierdlem1  37539  fourierdlem4  37542  fourierdlem32  37570  fourierdlem33  37571  fourierdlem43  37581  fourierdlem65  37603  fourierdlem79  37617  iccpartrn  38143  bgoldbtbnd  38303  expnegico01  39084  dignnld  39184
  Copyright terms: Public domain W3C validator