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

Theorem mpbir2and 889
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 519 . 2  |-  ( ph  ->  ( ch  /\  th ) )
4 mpbir2and.3 . 2  |-  ( ph  ->  ( ps  <->  ( ch  /\ 
th ) ) )
53, 4mpbird 224 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  fnpr  5913  fnprOLD  5914  dffi3  7398  supmax  7430  suppr  7433  ordtypelem7  7453  cantnfle  7586  cantnf0  7590  cantnfp1lem1  7594  cantnfp1lem2  7595  cantnfp1lem3  7596  oemapvali  7600  cantnflem1a  7601  cantnflem1c  7603  cantnflem1d  7604  cantnflem1  7605  cantnf  7609  mapfien  7613  rankpwi  7709  carduni  7828  fin23lem32  8184  fpwwe2lem6  8470  fpwwe2lem9  8473  fpwwe2lem12  8476  fpwwe2lem13  8477  fpwwe2  8478  inttsk  8609  grutsk1  8656  add20  9500  supmul  9936  suprzcl  10309  uzwo3  10529  rpnnen1lem5  10564  xrre  10717  xrre3  10719  xleadd1a  10792  xlemul1a  10827  supxrre  10866  infmxrre  10874  ixxub  10897  ixxlb  10898  elioc2  10933  elico2  10934  elicc2  10935  elfz1eq  11028  fzctr  11076  fzoaddel  11134  flid  11175  flval3  11181  fladdz  11186  fldiv  11200  modid  11229  seqf1olem1  11321  bcval5  11568  hashf1lem1  11663  sqeqd  11930  sqrlem7  12013  max0add  12074  abs2difabs  12097  rddif  12103  fzomaxdiflem  12105  rexico  12116  limsupgre  12234  rlim3  12251  icco1  12293  rlimclim  12299  rlimuni  12303  rlimresb  12318  isercolllem2  12418  isercolllem3  12419  isercoll  12420  caucvgrlem  12425  caurcvgr  12426  iseraltlem3  12436  fsum00  12536  o1fsum  12551  dvdseq  12856  bitsfzolem  12905  bitsfzo  12906  bitsmod  12907  bitscmp  12909  gcd0id  12982  gcdneg  12985  bezoutlem4  13000  nn0seqcvgd  13020  prmind2  13049  qredeq  13065  isprm5  13071  hashdvds  13123  eulerthlem2  13130  pcpremul  13176  pcidlem  13204  pcgcd1  13209  pcadd2  13218  fldivp1  13225  pcfaclem  13226  prmreclem5  13247  4sqlem17  13288  vdwlem1  13308  vdwlem6  13313  vdwlem12  13319  vdwlem13  13320  0ram  13347  ram0  13349  ramub1lem1  13353  invco  13955  sectmon  13962  monsect  13963  ssctr  13984  ssceq  13985  issubc3  14005  fullsubc  14006  funcinv  14029  fthmon  14083  fuccocl  14120  fucidcl  14121  invfuc  14130  elhomai  14147  setcmon  14201  setcepi  14202  catcisolem  14220  curf2cl  14287  yonedalem4c  14333  yonedalem3  14336  yoniso  14341  isacs3lem  14551  tsrdir  14642  nmznsg  14943  ghmpreima  14986  ghmeql  14987  ghmnsgpreima  14989  cntzsubm  15093  cntzsubg  15094  cntzmhm  15096  odlem2  15136  gexlem2  15175  gexcl2  15182  sylow1lem5  15195  subgslw  15209  slwhash  15217  fislw  15218  sylow3lem1  15220  lsmsubg  15247  efgredlemd  15335  efgredlem  15338  efgcpbllemb  15346  frgpuplem  15363  cyggeninv  15452  iscygd  15456  iscygodd  15457  gsumconst  15491  gsumpt  15504  dprdfcntz  15532  eldprdi  15535  subgdmdprd  15551  subgdprd  15552  dprdpr  15567  ablfac1c  15588  ablfac1eu  15590  ablfaclem3  15604  issubdrg  15852  rhmeql  15857  rhmima  15858  cntzsubr  15859  isabvd  15867  abvdiv  15884  lsslsp  16050  lmhmima  16082  lmhmpreima  16083  lmhmeql  16090  lsmcl  16114  lspfixed  16159  issubassa  16342  issubassa2  16362  psrbaglesupp  16392  psrbaglecl  16393  psrbagaddcl  16394  psrbagcon  16395  psrbas  16402  psrlidm  16426  psrridm  16427  mvridlem  16442  mplsubglem  16457  mpllsslem  16458  mplassa  16476  subrgmpl  16482  mplcoe3  16488  mplcoe2  16489  mplbas2  16490  mplind  16521  ply1assa  16556  coe1tmmul2  16627  coe1tmmul  16628  qsssubdrg  16717  gzrngunit  16723  ocvpj  16903  distop  17019  indistopon  17024  ppttop  17030  epttop  17032  mretopd  17115  toponmre  17116  neiss  17132  opnneissb  17137  ssnei2  17139  innei  17148  neiptoptop  17154  ordtcld1  17219  ordtcld2  17220  lmconst  17283  cnpnei  17286  iscncl  17291  cnss1  17298  cnss2  17299  cncnpi  17300  cncnp  17302  cnconst2  17305  cnrest  17307  cnpresti  17310  cnpdis  17315  paste  17316  lmcnp  17326  cnhaus  17376  hauscmp  17428  2ndcomap  17478  1stcelcls  17481  1stccnp  17482  llyrest  17505  nllyrest  17506  llyidm  17508  nllyidm  17509  kgentopon  17527  kgenidm  17536  kgencn3  17547  txcld  17592  neitx  17596  tx1cn  17598  tx2cn  17599  ptcld  17602  xkoccn  17608  txcnp  17609  ptcnp  17611  txcnmpt  17613  ptcn  17616  txdis1cn  17624  ptrescn  17628  txkgen  17641  xkoco1cn  17646  xkoco2cn  17647  xkococn  17649  xkoinjcn  17676  qtoptop2  17688  qtopuni  17691  qtopid  17694  qtopkgen  17699  basqtop  17700  tgqtop  17701  qtopss  17704  qtopeu  17705  qtoprest  17706  kqopn  17723  kqcld  17724  kqreglem2  17731  reghmph  17782  ordthmeolem  17790  qtopf1  17805  opnfbas  17831  isfil2  17845  fbasweak  17854  fsubbas  17856  filcon  17872  fbasrn  17873  rnelfmlem  17941  flimss2  17961  flimss1  17962  hausflim  17970  flimclslem  17973  flimsncls  17975  cnpflfi  17988  flfcnp2  17996  fclsfnflim  18016  cnextfvval  18053  cnextfres  18056  symgtgp  18088  opnsubg  18094  ghmcnp  18101  divstgpopn  18106  divstgplem  18107  divstgphaus  18109  tsmsfbas  18114  ustfilxp  18199  utoptop  18221  utopbas  18222  restutopopn  18225  iducn  18270  cstucnd  18271  ucncn  18272  fmucnd  18279  cfilufg  18280  trcfilu  18281  cfiluweak  18282  neipcfilu  18283  psmetsym  18298  isxmetd  18313  xmetsym  18334  imasdsf1olem  18360  imasf1oxmet  18362  xblss2ps  18388  xblss2  18389  xblcntrps  18397  xblcntr  18398  blcld  18492  metustfbasOLD  18552  metustfbas  18553  cfilucfilOLD  18556  cfilucfil  18557  restmetu  18574  ngptgp  18634  tngngpd  18651  tngnrg  18667  nlmvscn  18680  nrginvrcn  18684  nmo0  18726  nmoeq0  18727  nmoid  18733  nghmcn  18736  0nmhm  18746  blcvx  18786  zcld  18801  iccntr  18809  xrge0tsms  18822  xmetdcn2  18825  metdstri  18838  metdscn  18843  rescncf  18884  cncfco  18894  oprpiece1res2  18934  cnheibor  18937  cnllycmp  18938  bndth  18940  evth  18941  ishtpyd  18957  isphtpyd  18968  pcoval2  18998  nmhmcn  19085  ipcn  19157  lmnn  19173  cfilss  19180  iscfil3  19183  cfilfcls  19184  cmetcaulem  19198  iscmet3lem2  19202  cfilres  19206  lmcau  19222  flimcfil  19223  cncmet  19232  rlmbn  19272  minveclem3b  19286  pjthlem1  19295  pjth2  19298  ivthlem3  19307  ovolssnul  19340  ovolctb  19343  ovolunnul  19353  ovoliunnul  19360  ovolsca  19368  ovolicc  19376  ovolicopnf  19377  voliunlem2  19402  voliunlem3  19403  volsup  19407  uniioovol  19428  uniiccvol  19429  dyadmaxlem  19446  vitalilem5  19461  ismbfd  19489  mbfres  19493  mbfss  19495  mbfmulc2re  19497  mbfadd  19510  mbfmulc2  19512  mbflimsup  19515  mbflim  19517  i1faddlem  19542  i1fmullem  19543  mbfmul  19575  itg2itg1  19585  itg2seq  19591  itg2eqa  19594  itg2mulc  19596  itg2split  19598  itg2mono  19602  itg2cnlem1  19610  ibl0  19635  iblposlem  19640  itgreval  19645  iblneg  19651  iblss  19653  iblss2  19654  itgle  19658  iblconst  19666  iblabs  19677  iblabsr  19678  iblmulc2  19679  bddmulibl  19687  limciun  19738  limcun  19739  dvres2lem  19754  dvidlem  19759  dvcnp2  19763  dvcn  19764  cpnres  19780  dvaddbr  19781  dvmulbr  19782  dvcobr  19789  dvcjbr  19792  dvrec  19798  dvcnvlem  19817  dvferm  19829  dvlip2  19836  dveq0  19841  dv11cn  19842  dvivthlem1  19849  lhop1  19855  lhop2  19856  lhop  19857  dvcnvre  19860  dvfsumlem3  19869  dvfsumlem4  19870  dvfsumrlim  19872  dvfsum2  19875  ftc1a  19878  ftc1lem4  19880  ftc1lem6  19882  ftc1  19883  evlslem3  19892  mpfind  19922  coe1mul3  19979  deg1addle2  19982  deg1add  19983  deg1sublt  19990  deg1mul2  19994  deg1tm  19998  fta1blem  20048  drnguc1p  20050  ig1prsp  20057  plyco0  20068  plyeq0lem  20086  dgrub  20110  dgreq  20120  dgradd2  20143  dgrmul  20145  dgrcolem2  20149  dgrco  20150  plycpn  20163  plydivlem4  20170  plydiveu  20172  vieta1lem2  20185  vieta1  20186  aalioulem2  20207  aalioulem3  20208  aaliou3lem7  20223  tayl0  20235  ulmcn  20272  ulmdvlem3  20275  psercn  20299  abelth  20314  pilem3  20326  efif1olem1  20401  abslogimle  20428  argregt0  20462  argrege0  20463  logf1o2  20498  cxpsqrlem  20550  cxpcn3  20589  abscxpbnd  20594  ang180lem2  20609  ang180lem3  20610  logreclem  20617  xrlimcnp  20764  harmonicbnd4  20806  fsumharmonic  20807  basellem3  20822  basellem4  20823  dvdsppwf1o  20928  dvdsflf1o  20929  fsumfldivdiaglem  20931  chpeq0  20949  chteq0  20950  chtub  20953  chpub  20961  dchrelbasd  20980  dchrmulcl  20990  dchrinv  21002  bcmono  21018  bposlem1  21025  bposlem2  21026  lgslem1  21037  lgsdirprm  21070  lgsqrlem2  21083  lgsqrlem3  21084  lgsdchr  21089  lgseisenlem1  21090  lgseisenlem2  21091  lgseisenlem3  21092  lgsquadlem1  21095  2sqlem8  21113  2sqblem  21118  chebbnd1lem1  21120  dchrisumlem1  21140  dchrisumlem2  21141  dchrisumlem3  21142  dchrisum0fno1  21162  pntrmax  21215  pntpbnd1a  21236  pntibndlem3  21243  pntlemn  21251  pntlemi  21255  pntlem3  21260  pntleml  21262  ostth1  21284  ostth2  21288  ostth3  21289  cusgra0v  21426  cusgraexi  21434  cusgrares  21438  1pthon  21548  constr2spth  21557  2pthon  21559  constr3trllem3  21596  constr3cycl  21605  eupares  21654  eupap1  21655  nvabs  22119  vacn  22147  nmcvcn  22148  nmblore  22244  0lno  22248  0blo  22250  nmlno0lem  22251  occl  22763  pjhthlem1  22850  pjpjpre  22878  nmopre  23330  nmlnop0iALT  23455  nmophmi  23491  leoprf2  23587  stlesi  23701  disjdifprg  23974  fzspl  24106  xrge0tsmsd  24180  ofldaddlt  24198  ofldlt1  24200  kerf1hrm  24219  metider  24246  qqhval2lem  24322  qqhcn  24332  pwsiga  24470  prsiga  24471  measle0  24519  mbfmcst  24566  1stmbfm  24567  2ndmbfm  24568  imambfm  24569  cnmbfm  24570  mbfmco  24571  mbfmco2  24572  0rrv  24666  ballotlemfc0  24707  ballotlemfcc  24708  lgamgulmlem5  24774  lgambdd  24778  derangen  24815  subfacval3  24832  cvmseu  24920  cvmliftmolem2  24926  cvmliftlem7  24935  cvmliftlem15  24942  cvmlift2lem9a  24947  cvmlift2lem9  24955  cvmlift2lem10  24956  cvmlift2lem11  24957  cvmlift2lem12  24958  cvmlift3lem6  24968  cvmlift3lem8  24970  fznatpl1  25155  brbtwn2  25752  axlowdimlem3  25791  axlowdimlem16  25804  axcontlem8  25818  supaddc  26141  supadd  26142  mblfinlem  26147  ovoliunnfl  26151  volsupnfl  26154  mbfresfi  26156  itg2addnclem2  26160  iblabsnc  26172  iblmulc2nc  26173  ftc1cnnclem  26181  ftc1cnnc  26182  fness  26256  ssref  26257  fnetr  26260  reftr  26263  fnessref  26267  refssfne  26268  neibastop1  26282  neibastop2  26284  tailfb  26300  filnetlem3  26303  fzadd2  26339  sdclem2  26340  metf1o  26355  ismtyhmeolem  26407  ismtyres  26411  heibor1lem  26412  bfplem2  26426  bfp  26427  rrncmslem  26435  iccbnd  26443  icccmpALT  26444  rngogrphom  26481  rngoisoco  26492  keridl  26536  fzsplit1nn0  26706  icodiamlt  26777  irrapxlem3  26781  irrapxlem4  26782  pell1234qrdich  26818  pell1qr1  26828  pell14qrgap  26832  pellqrexplicit  26834  rmspecfund  26866  fzmaxdif  26940  acongeq  26942  jm2.23  26961  jm3.1  26985  lmhmlnmsplit  27057  dsmm0cl  27078  dsmmacl  27079  dsmmsubg  27081  dsmmlss  27082  uvcff  27112  frlmsplit2  27115  lindfrn  27163  f1lindf  27164  lindsss  27166  hbt  27206  dgrsub2  27211  proot1ex  27392  dvconstbi  27423  ubelsupr  27562  fmul01  27581  fmuldfeq  27584  climsuse  27605  stoweidlem7  27627  stoweidlem13  27633  stoweidlem26  27646  wallispilem3  27687  stirlinglem6  27699  stirlinglem10  27703  ubmelfzo  27990  fzo1fzo0n0  27992  usgra2wlkspth  28042  frgra0v  28101  frgra1v  28106  bnj1452  29131  lsmcv2  29516  lsatcv0  29518  lcvexchlem4  29524  lcvexchlem5  29525  l1cvpat  29541  lfl0f  29556  lfladdcl  29558  lflnegcl  29562  lkrlss  29582  eqlkr  29586  lkrlsp  29589  lkrlsp2  29590  lshpkrcl  29603  lkrin  29651  1cvrjat  29961  llni  29994  llnle  30004  lplni  30018  lplnle  30026  llncvrlpln2  30043  2atmat  30047  lvoli  30061  lplncvrlvol2  30101  elpaddri  30288  paddclN  30328  pclclN  30377  pclfinN  30386  0psubclN  30429  1psubclN  30430  atpsubclN  30431  pmapsubclN  30432  osumclN  30453  pexmidN  30455  pexmidlem6N  30461  lhp2lt  30487  lautcnv  30576  idlaut  30582  lautco  30583  idldil  30600  ldilcnv  30601  ldilco  30602  ltrncnv  30632  idltrn  30636  cdleme16d  30767  cdleme50laut  31033  cdleme50ldil  31034  cdleme50ltrn  31043  ltrnco  31205  dian0  31526  dia0eldmN  31527  dia1eldmN  31528  dialss  31533  diaintclN  31545  docaclN  31611  doca2N  31613  djajN  31624  dibintclN  31654  diblss  31657  dicvaddcl  31677  dicvscacl  31678  dicn0  31679  cdlemn11a  31694  dihord2cN  31708  dihord11b  31709  dihord6apre  31743  dihmeetlem1N  31777  dihglblem5apreN  31778  dihpN  31823  dihjatcclem4  31908  dochkr1  31965  islpoldN  31971  lcfrlem31  32060  mapdpglem18  32176  mapdheq2  32216  mapdheq4  32219  mapdh6aN  32222  hdmap1l6a  32297  hdmap1neglem1N  32315  hdmap14lem4a  32361
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator