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

Theorem mpbir2and 920
Description: Detach a conjunction of truths in a biconditional. (Contributed by NM, 6-Nov-2011.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
Hypotheses
Ref Expression
mpbir2and.1  |-  ( ph  ->  ch )
mpbir2and.2  |-  ( ph  ->  th )
mpbir2and.3  |-  ( ph  ->  ( ps  <->  ( ch  /\ 
th ) ) )
Assertion
Ref Expression
mpbir2and  |-  ( ph  ->  ps )

Proof of Theorem mpbir2and
StepHypRef Expression
1 mpbir2and.1 . . 3  |-  ( ph  ->  ch )
2 mpbir2and.2 . . 3  |-  ( ph  ->  th )
31, 2jca 532 . 2  |-  ( ph  ->  ( ch  /\  th ) )
4 mpbir2and.3 . 2  |-  ( ph  ->  ( ps  <->  ( ch  /\ 
th ) ) )
53, 4mpbird 232 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  fmptsng  6080  fmptsnd  6081  fnprb  6117  fnprOLD  6118  fdmfifsupp  7835  fczfsuppd  7843  fsuppmptif  7855  fsuppco2  7858  fsuppcor  7859  dffi3  7887  supmax  7921  suppr  7925  ordtypelem7  7945  cantnf0  8090  cantnfp1lem1  8093  cantnfp1lem2  8094  cantnfp1lem3  8095  cantnflem1a  8100  cantnflem1d  8103  cantnflem1  8104  cantnf  8108  cantnfleOLD  8116  cantnfp1lem1OLD  8119  cantnfp1lem2OLD  8120  cantnfp1lem3OLD  8121  cantnflem1aOLD  8123  cantnflem1cOLD  8125  cantnflem1dOLD  8126  cantnflem1OLD  8127  cantnfOLD  8130  mapfienOLD  8134  rankpwi  8237  carduni  8358  fin23lem32  8720  fpwwe2lem6  9009  fpwwe2lem9  9012  fpwwe2lem12  9015  fpwwe2lem13  9016  fpwwe2  9017  inttsk  9148  grutsk1  9195  add20  10060  supmul  10507  suprzcl  10936  uzwo3  11173  rpnnen1lem5  11208  xrre  11366  xrre3  11368  xleadd1a  11441  xlemul1a  11476  supxrre  11515  infmxrre  11523  ixxub  11546  ixxlb  11547  elioc2  11583  elico2  11584  elicc2  11585  elfz1eq  11693  fznatpl1  11730  nn0fz0  11769  fzctr  11780  fzo1fzo0n0  11828  fzoaddel  11837  flid  11908  flval3  11914  fladdz  11921  fldiv  11950  modid  11983  seqf1olem1  12109  bcval5  12358  hashf1lem1  12464  ccat2s1fvw  12599  wwlktovf1  12852  sqeqd  12956  sqrlem7  13039  max0add  13100  abs2difabs  13123  rddif  13129  fzomaxdiflem  13131  rexico  13142  limsupgre  13260  rlim3  13277  icco1  13319  rlimclim  13325  rlimuni  13329  rlimresb  13344  isercolllem2  13444  isercolllem3  13445  isercoll  13446  caucvgrlem  13451  caurcvgr  13452  iseraltlem3  13462  fsum00  13568  o1fsum  13583  dvdseq  13885  bitsfzolem  13936  bitsfzo  13937  bitsmod  13938  bitscmp  13940  gcd0id  14013  gcdneg  14016  bezoutlem4  14031  nn0seqcvgd  14051  prmind2  14080  qredeq  14099  isprm5  14105  hashdvds  14157  eulerthlem2  14164  pcpremul  14219  pcidlem  14247  pcgcd1  14252  pcadd2  14261  fldivp1  14268  pcfaclem  14269  prmreclem5  14290  4sqlem17  14331  vdwlem1  14351  vdwlem6  14356  vdwlem12  14362  vdwlem13  14363  0ram  14390  ram0  14392  ramub1lem1  14396  invco  15019  sectmon  15026  monsect  15027  ssctr  15048  ssceq  15049  issubc3  15069  fullsubc  15070  funcinv  15093  fthmon  15147  fuccocl  15184  fucidcl  15185  invfuc  15194  elhomai  15211  setcmon  15265  setcepi  15266  catcisolem  15284  curf2cl  15351  yonedalem4c  15397  yonedalem3  15400  yoniso  15405  lublecl  15469  isacs3lem  15646  tsrdir  15718  nmznsg  16037  ghmpreima  16080  ghmeql  16081  ghmnsgpreima  16083  cntzsubm  16165  cntzsubg  16166  cntzmhm  16168  symgextfo  16239  symgfixf1  16255  symgfixfolem1  16256  odlem2  16356  gexlem2  16395  gexcl2  16402  sylow1lem5  16415  subgslw  16429  slwhash  16437  fislw  16438  sylow3lem1  16440  lsmsubg  16467  efgredlemd  16555  efgredlem  16558  efgcpbllemb  16566  frgpuplem  16583  cyggeninv  16674  iscygd  16678  iscygodd  16679  gsumzadd  16723  gsumconst  16742  gsumpt  16776  gsumptOLD  16777  gsum2dlem2  16786  gsum2d  16787  gsum2d2lem  16789  dprdfcntz  16836  dprdfcntzOLD  16842  eldprdi  16845  eldprdiOLD  16852  subgdmdprd  16868  subgdprd  16869  dprdpr  16886  ablfac1c  16909  ablfac1eu  16911  ablfaclem3  16925  kerf1hrm  17172  issubdrg  17234  rhmeql  17239  rhmima  17240  cntzsubr  17241  isabvd  17249  abvdiv  17266  lsslsp  17441  lmhmima  17473  lmhmpreima  17474  lmhmeql  17481  lsmcl  17509  lspfixed  17554  issubassa  17741  issubassa2  17762  snifpsrbag  17783  psrbaglesupp  17785  psrbaglesuppOLD  17786  psrbaglecl  17787  psrbagaddcl  17788  psrbagaddclOLD  17789  psrbagcon  17790  psrbasOLD  17799  psrlidmOLD  17825  psrridmOLD  17827  mvridlemOLD  17843  mplsubglem  17861  mpllsslem  17862  mplsubglemOLD  17863  mpllsslemOLD  17864  mplassa  17884  subrgmpl  17890  mplcoe3OLD  17897  mplcoe5  17899  mplcoe2OLD  17901  mplbas2  17902  mplbas2OLD  17903  mplind  17935  evlslem3  17951  mpfind  17973  ply1assa  18006  coe1tmmul2  18085  coe1tmmul  18086  qsssubdrg  18242  gzrngunit  18248  evpmodpmf1o  18396  ocvpj  18512  dsmm0cl  18535  dsmmacl  18536  dsmmsubg  18538  dsmmlss  18539  frlmsplit2  18567  uvcff  18586  lindfrn  18620  f1lindf  18621  lindsss  18623  mat1rngiso  18752  dmatid  18761  dmatsubcl  18764  dmatscmcl  18769  scmatid  18780  scmataddcl  18782  scmatsubcl  18783  scmatmulcl  18784  smatvscl  18790  scmatrhmcl  18794  scmatrngiso  18802  mat0scmat  18804  mat1scmat  18805  mdet0pr  18858  m2cpmrngiso  19023  pm2mprngiso  19087  chmaidscmat  19113  fvmptnn04if  19114  distop  19260  indistopon  19265  ppttop  19271  epttop  19273  mretopd  19356  toponmre  19357  neiss  19373  opnneissb  19378  ssnei2  19380  innei  19389  neiptoptop  19395  ordtcld1  19461  ordtcld2  19462  lmconst  19525  cnpnei  19528  iscncl  19533  cnss1  19540  cnss2  19541  cncnpi  19542  cncnp  19544  cnconst2  19547  cnrest  19549  cnpresti  19552  cnpdis  19557  paste  19558  lmcnp  19568  cnhaus  19618  hauscmp  19670  2ndcomap  19722  1stcelcls  19725  1stccnp  19726  llyrest  19749  nllyrest  19750  llyidm  19752  nllyidm  19753  kgentopon  19771  kgenidm  19780  kgencn3  19791  txcld  19836  neitx  19840  tx1cn  19842  tx2cn  19843  ptcld  19846  xkoccn  19852  txcnp  19853  ptcnp  19855  txcnmpt  19857  ptcn  19860  txdis1cn  19868  ptrescn  19872  txkgen  19885  xkoco1cn  19890  xkoco2cn  19891  xkococn  19893  xkoinjcn  19920  qtoptop2  19932  qtopuni  19935  qtopid  19938  qtopkgen  19943  basqtop  19944  tgqtop  19945  qtopss  19948  qtopeu  19949  qtoprest  19950  kqopn  19967  kqcld  19968  kqreglem2  19975  reghmph  20026  ordthmeolem  20034  qtopf1  20049  opnfbas  20075  isfil2  20089  fbasweak  20098  fsubbas  20100  filcon  20116  fbasrn  20117  rnelfmlem  20185  flimss2  20205  flimss1  20206  hausflim  20214  flimclslem  20217  flimsncls  20219  cnpflfi  20232  flfcnp2  20240  fclsfnflim  20260  cnextfvval  20297  cnextfres  20300  symgtgp  20332  opnsubg  20338  ghmcnp  20345  divstgpopn  20350  divstgplem  20351  divstgphaus  20353  tsmsfbas  20358  ustfilxp  20447  utoptop  20469  utopbas  20470  restutopopn  20473  iducn  20518  cstucnd  20519  ucncn  20520  fmucnd  20527  cfilufg  20528  trcfilu  20529  cfiluweak  20530  neipcfilu  20531  psmetsym  20546  isxmetd  20561  xmetsym  20582  imasdsf1olem  20608  imasf1oxmet  20610  xblss2ps  20636  xblss2  20637  xblcntrps  20645  xblcntr  20646  blcld  20740  metustfbasOLD  20800  metustfbas  20801  cfilucfilOLD  20804  cfilucfil  20805  restmetu  20822  ngptgp  20882  tngngpd  20899  tngnrg  20915  nlmvscn  20928  nrginvrcn  20932  nmo0  20974  nmoeq0  20975  nmoid  20981  nghmcn  20984  0nmhm  20994  blcvx  21035  zcld  21050  iccntr  21058  xrge0tsms  21071  xmetdcn2  21074  metdstri  21087  metdscn  21092  rescncf  21133  cncfco  21143  oprpiece1res2  21184  cnheibor  21187  cnllycmp  21188  bndth  21190  evth  21191  ishtpyd  21207  isphtpyd  21218  pcoval2  21248  nmhmcn  21335  ipcn  21418  lmnn  21434  cfilss  21441  iscfil3  21444  cfilfcls  21445  cmetcaulem  21459  iscmet3lem2  21463  cfilres  21467  lmcau  21483  flimcfil  21484  cncmet  21493  rlmbn  21533  minveclem3b  21575  pjthlem1  21584  pjth2  21587  ivthlem3  21597  ovolssnul  21630  ovolctb  21633  ovolunnul  21643  ovoliunnul  21650  ovolsca  21658  ovolicc  21666  ovolicopnf  21667  voliunlem2  21693  voliunlem3  21694  volsup  21698  uniioovol  21720  uniiccvol  21721  dyadmaxlem  21738  vitalilem5  21753  ismbfd  21779  mbfres  21783  mbfss  21785  mbfmulc2re  21787  mbfadd  21800  mbfmulc2  21802  mbflimsup  21805  mbflim  21807  i1faddlem  21832  i1fmullem  21833  mbfmul  21865  itg2itg1  21875  itg2seq  21881  itg2eqa  21884  itg2mulc  21886  itg2split  21888  itg2mono  21892  itg2cnlem1  21900  ibl0  21925  iblposlem  21930  itgreval  21935  iblneg  21941  iblss  21943  iblss2  21944  itgle  21948  iblconst  21956  iblabs  21967  iblabsr  21968  iblmulc2  21969  bddmulibl  21977  limciun  22030  limcun  22031  dvres2lem  22046  dvidlem  22051  dvcnp2  22055  dvcn  22056  cpnres  22072  dvaddbr  22073  dvmulbr  22074  dvcobr  22081  dvcjbr  22084  dvrec  22090  dvcnvlem  22109  dvferm  22121  dvlip2  22128  dveq0  22133  dv11cn  22134  dvivthlem1  22141  lhop1  22147  lhop2  22148  lhop  22149  dvcnvre  22152  dvfsumlem3  22161  dvfsumlem4  22162  dvfsumrlim  22164  dvfsum2  22167  ftc1a  22170  ftc1lem4  22172  ftc1lem6  22174  ftc1  22175  coe1mul3  22232  deg1addle2  22235  deg1add  22236  deg1sublt  22243  deg1mul2  22247  deg1tm  22251  fta1blem  22301  drnguc1p  22303  ig1prsp  22310  plyco0  22321  plyeq0lem  22339  dgrub  22363  dgreq  22373  dgradd2  22396  dgrmul  22398  dgrcolem2  22402  dgrco  22403  plycpn  22416  plydivlem4  22423  plydiveu  22425  vieta1lem2  22438  vieta1  22439  aalioulem2  22460  aalioulem3  22461  aaliou3lem7  22476  tayl0  22488  ulmcn  22525  ulmdvlem3  22528  psercn  22552  abelth  22567  pilem3  22579  efif1olem1  22659  abslogimle  22686  argregt0  22720  argrege0  22721  logf1o2  22756  cxpsqrtlem  22808  cxpcn3  22847  abscxpbnd  22852  ang180lem2  22867  ang180lem3  22868  logreclem  22875  xrlimcnp  23023  harmonicbnd4  23065  fsumharmonic  23066  basellem3  23081  basellem4  23082  dvdsppwf1o  23187  dvdsflf1o  23188  fsumfldivdiaglem  23190  chpeq0  23208  chteq0  23209  chtub  23212  chpub  23220  dchrelbasd  23239  dchrmulcl  23249  dchrinv  23261  bcmono  23277  bposlem1  23284  bposlem2  23285  lgslem1  23296  lgsdirprm  23329  lgsqrlem2  23342  lgsqrlem3  23343  lgsdchr  23348  lgseisenlem1  23349  lgseisenlem2  23350  lgseisenlem3  23351  lgsquadlem1  23354  2sqlem8  23372  2sqblem  23377  chebbnd1lem1  23379  dchrisumlem1  23399  dchrisumlem2  23400  dchrisumlem3  23401  dchrisum0fno1  23421  pntrmax  23474  pntpbnd1a  23495  pntibndlem3  23502  pntlemn  23510  pntlemi  23514  pntlem3  23519  pntleml  23521  ostth1  23543  ostth2  23547  ostth3  23548  ttgcontlem1  23861  brbtwn2  23881  axlowdimlem3  23920  axlowdimlem16  23933  axcontlem8  23947  cusgra0v  24133  cusgraexi  24141  cusgrares  24145  uvtxnb  24170  1pthon  24266  constr2spth  24275  2pthon  24277  usgra2wlkspth  24294  constr3trllem3  24325  constr3cycl  24334  wlklniswwlkn1  24372  vfwlkniswwlkn  24379  usg2wlkeq2  24382  wwlknred  24396  wwlknredwwlkn0  24400  clwwlkel  24466  wwlkext2clwwlk  24476  clwwnisshclwwn  24482  clwlkf1clwwlk  24523  0egra0rgra  24609  0vgrargra  24610  eupares  24648  eupap1  24649  frgra0v  24666  frgra1v  24671  nvabs  25249  vacn  25277  nmcvcn  25278  nmblore  25374  0lno  25378  0blo  25380  nmlno0lem  25381  occl  25895  pjhthlem1  25982  pjpjpre  26010  nmopre  26462  nmlnop0iALT  26587  nmophmi  26623  leoprf2  26719  stlesi  26833  disjdifprg  27106  fpwrelmap  27225  xrge0tsmsd  27435  ornglmullt  27457  orngrmullt  27458  ofldlt1  27463  isarchiofld  27467  metider  27506  qqhval2lem  27595  qqhcn  27605  pwsiga  27767  prsiga  27768  measle0  27816  mbfmcst  27867  1stmbfm  27868  2ndmbfm  27869  imambfm  27870  cnmbfm  27871  mbfmco  27872  mbfmco2  27873  oddpwdc  27930  eulerpartlemgs2  27956  0rrv  28027  ballotlemfc0  28068  ballotlemfcc  28069  lgamgulmlem5  28212  lgambdd  28216  derangen  28253  subfacval3  28270  cvmseu  28358  cvmliftmolem2  28364  cvmliftlem7  28373  cvmliftlem15  28380  cvmlift2lem9a  28385  cvmlift2lem9  28393  cvmlift2lem10  28394  cvmlift2lem11  28395  cvmlift2lem12  28396  cvmlift3lem6  28406  cvmlift3lem8  28408  wsuclem  28955  supaddc  29615  supadd  29616  mblfinlem2  29627  ovoliunnfl  29631  volsupnfl  29634  mbfresfi  29636  dvtanlem  29639  itg2addnclem2  29642  iblabsnc  29654  iblmulc2nc  29655  ftc1cnnclem  29663  ftc1cnnc  29664  ftc1anc  29673  fness  29752  ssref  29753  fnetr  29756  reftr  29759  fnessref  29763  refssfne  29764  neibastop1  29778  neibastop2  29780  tailfb  29796  filnetlem3  29799  fzadd2  29835  sdclem2  29836  metf1o  29849  ismtyhmeolem  29901  ismtyres  29905  heibor1lem  29906  bfplem2  29920  bfp  29921  rrncmslem  29929  iccbnd  29937  icccmpALT  29938  rngogrphom  29975  rngoisoco  29986  keridl  30030  fzsplit1nn0  30289  icodiamlt  30358  irrapxlem3  30362  irrapxlem4  30363  pell1234qrdich  30399  pell1qr1  30409  pell14qrgap  30413  pellqrexplicit  30415  rmspecfund  30447  fzmaxdif  30521  acongeq  30523  jm2.23  30542  jm3.1  30566  lmhmlnmsplit  30637  hbt  30683  dgrsub2  30688  proot1ex  30766  lcmneg  30809  hashnzfz2  30826  dvconstbi  30839  ubelsupr  30973  fmul01  31130  fmuldfeq  31133  climsuse  31150  stoweidlem7  31307  stoweidlem13  31313  stoweidlem26  31326  wallispilem3  31367  stirlinglem6  31379  stirlinglem10  31383  fourierdlem12  31419  fourierdlem52  31459  rmfsupp  32040  mndpfsupp  32042  scmfsupp  32044  mptcfsupp  32046  lcoel0  32102  lincsumcl  32105  lincscmcl  32106  lcoss  32110  lindsrng01  32142  lincreslvec3  32156  lindssnlvec  32160  mnd1  32161  bnj1452  33187  bj-finsumval0  33735  lsmcv2  33826  lsatcv0  33828  lcvexchlem4  33834  lcvexchlem5  33835  l1cvpat  33851  lfl0f  33866  lfladdcl  33868  lflnegcl  33872  lkrlss  33892  eqlkr  33896  lkrlsp  33899  lkrlsp2  33900  lshpkrcl  33913  lkrin  33961  1cvrjat  34271  llni  34304  llnle  34314  lplni  34328  lplnle  34336  llncvrlpln2  34353  2atmat  34357  lvoli  34371  lplncvrlvol2  34411  elpaddri  34598  paddclN  34638  pclclN  34687  pclfinN  34696  0psubclN  34739  1psubclN  34740  atpsubclN  34741  pmapsubclN  34742  osumclN  34763  pexmidN  34765  pexmidlem6N  34771  lhp2lt  34797  lautcnv  34886  idlaut  34892  lautco  34893  idldil  34910  ldilcnv  34911  ldilco  34912  ltrncnv  34942  idltrn  34946  cdleme16d  35077  cdleme50laut  35343  cdleme50ldil  35344  cdleme50ltrn  35353  ltrnco  35515  dian0  35836  dia0eldmN  35837  dia1eldmN  35838  dialss  35843  diaintclN  35855  docaclN  35921  doca2N  35923  djajN  35934  dibintclN  35964  diblss  35967  dicvaddcl  35987  dicvscacl  35988  dicn0  35989  cdlemn11a  36004  dihord2cN  36018  dihord11b  36019  dihord6apre  36053  dihmeetlem1N  36087  dihglblem5apreN  36088  dihpN  36133  dihjatcclem4  36218  dochkr1  36275  islpoldN  36281  lcfrlem31  36370  mapdpglem18  36486  mapdheq2  36526  mapdheq4  36529  mapdh6aN  36532  hdmap1l6a  36607  hdmap1neglem1N  36625  hdmap14lem4a  36671
  Copyright terms: Public domain W3C validator