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

Theorem mpbir3and 1191
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 1188 . 2  |-  ( ph  ->  ( ch  /\  th  /\  ta ) )
5 mpbir3and.4 . 2  |-  ( ph  ->  ( ps  <->  ( ch  /\ 
th  /\  ta )
) )
64, 5mpbird 236 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    /\ w3a 985
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 189  df-an 373  df-3an 987
This theorem is referenced by:  canthwelem  9075  intwun  9160  tskwun  9209  gruwun  9238  ixxss1  11653  ixxss2  11654  ixxss12  11655  ixxub  11656  ixxlb  11657  ixxlbOLD  11658  elicod  11685  ubioc1  11688  lbico1  11689  lbicc2  11748  ubicc2  11749  difreicc  11764  supicc  11780  zmodfz  12118  addmodid  12139  dfrtrcl2  13125  phicl2  14716  4sqlem12  14900  isfuncd  15770  idfucl  15786  cofucl  15793  invfuc  15879  cnvps  16458  psss  16460  issubmd  16596  submid  16598  subsubm  16604  mhmima  16610  mhmeql  16611  gsumwspan  16630  frmdsssubm  16645  issubgrpd2  16833  grpissubg  16837  subgint  16841  0subg  16842  cycsubgcl  16843  nmzsubg  16858  eqger  16867  eqgcpbl  16871  ghmrn  16896  ghmpreima  16904  gastacl  16963  cntzsubm  16989  sylow2blem1  17272  lsmsubm  17305  torsubg  17492  oddvdssubg  17493  dmdprdd  17631  dprdwdOLD  17644  dprdsubg  17657  dprdres  17661  unitsubm  17898  subrgsubm  18021  subrgugrp  18027  subrgint  18030  issubdrg  18033  cntzsubr  18040  lsssubg  18180  islmhm2  18261  pj1lmhm  18323  islbs2  18377  islbs3  18378  lbsextlem4  18384  issubrngd2  18412  lidlsubg  18438  2idlcpbl  18458  mplsubglem  18658  mplsubrg  18664  mplind  18725  isphld  19221  dmatsgrp  19524  dmatsrng  19526  scmatsgrp  19544  scmatsrng  19545  scmatsgrp1  19547  scmatsrng1  19548  cpmatsubgpmat  19744  cpmatsrgpmat  19745  lmcnp  20320  isufil2  20923  ufileu  20934  filufint  20935  fmfnfm  20973  flimclslem  20999  fclsfnflim  21042  flimfnfcls  21043  fclscmp  21045  clssubg  21123  tgpconcompeqg  21126  tgpconcomp  21127  qustgpopn  21134  tgptsmscls  21164  xmeter  21448  metust  21573  tgqioo  21818  zcld  21831  iccntr  21839  icccmplem2  21841  icccmplem3  21842  reconnlem1  21844  reconnlem2  21845  xrge0tsms  21852  cnheiborlem  21982  om1addcl  22064  pi1blem  22070  pi1grplem  22080  pi1inv  22083  pi1xfr  22086  pi1xfrcnvlem  22087  pi1coghm  22092  cmetcaulem  22258  ivthlem2  22403  ivthlem3  22404  ovolicc2lem2  22471  ovolicc2lem5  22475  opnmbllem  22559  volcn  22564  ismbf3d  22610  mbfi1fseqlem6  22678  itg2const2  22699  i1fibl  22765  ibladd  22778  ditgsplitlem  22815  dvferm1lem  22936  dvferm2lem  22938  dvlip2  22947  dvivthlem1  22960  dvne0  22963  lhop1lem  22965  lhop1  22966  lhop  22968  dvcnvrelem1  22969  dvcnvrelem2  22970  dvcnvre  22971  ftc1lem1  22987  itgsubst  23001  aaliou3lem2  23299  psercnlem2  23379  efif1olem2  23492  logtayl  23605  log2tlbnd  23871  xrlimcnp  23894  pntibndlem2  24429  pntlemj  24441  pntleml  24449  trgcgr  24561  axlowdim  24991  wlkonwlk  25265  0wlkon  25277  constr1trl  25318  constr2wlk  25328  constr2trl  25329  constr2pth  25331  2pthon  25332  wwlkextinj  25458  el2spthonot  25598  cusgraisrusgra  25666  extwwlkfablem1  25802  isgrp2d  25963  isgrpda  26025  rngomndo  26149  eliccelico  28359  elicoelioo  28360  xrge0tsmsd  28548  tpr2rico  28718  measinb  29043  cntmeas  29048  dya2icoseg  29099  sibf0  29167  sibfof  29173  rescon  29969  cvmsss2  29997  cvmliftlem10  30017  mrsubco  30159  cgrextend  30775  cgr3rflx  30821  cgrxfr  30822  btwnconn1lem4  30857  btwnconn1lem8  30861  btwnconn1lem11  30864  bj-pinftynminfty  31669  iooelexlt  31765  opnmbllem0  31976  dvtanlemOLD  31991  ibladdnc  31999  bddiblnc  32012  ftc1anc  32025  isbnd3  32116  prdsbnd  32125  rngohomco  32213  rngoisocnv  32220  rngoidl  32257  0idl  32258  intidl  32262  unichnidl  32264  keridl  32265  smprngopr  32285  lshpnel2N  32551  lkrshp  32671  4atexlemex2  33636  4atex  33641  cdleme0moN  33791  istendod  34329  dihlspsnat  34901  dochsatshp  35019  modelico  35665  mon1psubm  36083  iocinico  36096  dfrtrcl3  36325  eliood  37595  eliccd  37601  eliocd  37605  limciccioolb  37701  limcicciooub  37717  icccncfext  37765  iblspltprt  37850  itgspltprt  37856  fourierdlem1  37970  fourierdlem4  37973  fourierdlem32  38002  fourierdlem33  38003  fourierdlem43  38014  fourierdlem65  38035  fourierdlem79  38049  iccpartrn  38744  bgoldbtbnd  38904  uhgrissubgr  39347  egrsubgr  39349  uhgrspansubgr  39363  uhgrspan1  39375  nbgr2vtx1edg  39418  nbuhgr2vtx1edgb  39420  cusgrexi  39507  cusgrrusgr  39597  wlkOnwlk  39662  0wlkOn  39709  expnegico01  40368  dignnld  40467
  Copyright terms: Public domain W3C validator