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  5909  fnprOLD  5910  dffi3  7394  supmax  7426  suppr  7429  ordtypelem7  7449  cantnfle  7582  cantnf0  7586  cantnfp1lem1  7590  cantnfp1lem2  7591  cantnfp1lem3  7592  oemapvali  7596  cantnflem1a  7597  cantnflem1c  7599  cantnflem1d  7600  cantnflem1  7601  cantnf  7605  mapfien  7609  rankpwi  7705  carduni  7824  fin23lem32  8180  fpwwe2lem6  8466  fpwwe2lem9  8469  fpwwe2lem12  8472  fpwwe2lem13  8473  fpwwe2  8474  inttsk  8605  grutsk1  8652  add20  9496  supmul  9932  suprzcl  10305  uzwo3  10525  rpnnen1lem5  10560  xrre  10713  xrre3  10715  xleadd1a  10788  xlemul1a  10823  supxrre  10862  infmxrre  10870  ixxub  10893  ixxlb  10894  elioc2  10929  elico2  10930  elicc2  10931  elfz1eq  11024  fzctr  11072  fzoaddel  11130  flid  11171  flval3  11177  fladdz  11182  fldiv  11196  modid  11225  seqf1olem1  11317  bcval5  11564  hashf1lem1  11659  sqeqd  11926  sqrlem7  12009  max0add  12070  abs2difabs  12093  rddif  12099  fzomaxdiflem  12101  rexico  12112  limsupgre  12230  rlim3  12247  icco1  12289  rlimclim  12295  rlimuni  12299  rlimresb  12314  isercolllem2  12414  isercolllem3  12415  isercoll  12416  caucvgrlem  12421  caurcvgr  12422  iseraltlem3  12432  fsum00  12532  o1fsum  12547  dvdseq  12852  bitsfzolem  12901  bitsfzo  12902  bitsmod  12903  bitscmp  12905  gcd0id  12978  gcdneg  12981  bezoutlem4  12996  nn0seqcvgd  13016  prmind2  13045  qredeq  13061  isprm5  13067  hashdvds  13119  eulerthlem2  13126  pcpremul  13172  pcidlem  13200  pcgcd1  13205  pcadd2  13214  fldivp1  13221  pcfaclem  13222  prmreclem5  13243  4sqlem17  13284  vdwlem1  13304  vdwlem6  13309  vdwlem12  13315  vdwlem13  13316  0ram  13343  ram0  13345  ramub1lem1  13349  invco  13951  sectmon  13958  monsect  13959  ssctr  13980  ssceq  13981  issubc3  14001  fullsubc  14002  funcinv  14025  fthmon  14079  fuccocl  14116  fucidcl  14117  invfuc  14126  elhomai  14143  setcmon  14197  setcepi  14198  catcisolem  14216  curf2cl  14283  yonedalem4c  14329  yonedalem3  14332  yoniso  14337  isacs3lem  14547  tsrdir  14638  nmznsg  14939  ghmpreima  14982  ghmeql  14983  ghmnsgpreima  14985  cntzsubm  15089  cntzsubg  15090  cntzmhm  15092  odlem2  15132  gexlem2  15171  gexcl2  15178  sylow1lem5  15191  subgslw  15205  slwhash  15213  fislw  15214  sylow3lem1  15216  lsmsubg  15243  efgredlemd  15331  efgredlem  15334  efgcpbllemb  15342  frgpuplem  15359  cyggeninv  15448  iscygd  15452  iscygodd  15453  gsumconst  15487  gsumpt  15500  dprdfcntz  15528  eldprdi  15531  subgdmdprd  15547  subgdprd  15548  dprdpr  15563  ablfac1c  15584  ablfac1eu  15586  ablfaclem3  15600  issubdrg  15848  rhmeql  15853  rhmima  15854  cntzsubr  15855  isabvd  15863  abvdiv  15880  lsslsp  16046  lmhmima  16078  lmhmpreima  16079  lmhmeql  16086  lsmcl  16110  lspfixed  16155  issubassa  16338  issubassa2  16358  psrbaglesupp  16388  psrbaglecl  16389  psrbagaddcl  16390  psrbagcon  16391  psrbas  16398  psrlidm  16422  psrridm  16423  mvridlem  16438  mplsubglem  16453  mpllsslem  16454  mplassa  16472  subrgmpl  16478  mplcoe3  16484  mplcoe2  16485  mplbas2  16486  mplind  16517  ply1assa  16552  coe1tmmul2  16623  coe1tmmul  16624  qsssubdrg  16713  gzrngunit  16719  ocvpj  16899  distop  17015  indistopon  17020  ppttop  17026  epttop  17028  mretopd  17111  toponmre  17112  neiss  17128  opnneissb  17133  ssnei2  17135  innei  17144  neiptoptop  17150  ordtcld1  17215  ordtcld2  17216  lmconst  17279  cnpnei  17282  iscncl  17287  cnss1  17294  cnss2  17295  cncnpi  17296  cncnp  17298  cnconst2  17301  cnrest  17303  cnpresti  17306  cnpdis  17311  paste  17312  lmcnp  17322  cnhaus  17372  hauscmp  17424  2ndcomap  17474  1stcelcls  17477  1stccnp  17478  llyrest  17501  nllyrest  17502  llyidm  17504  nllyidm  17505  kgentopon  17523  kgenidm  17532  kgencn3  17543  txcld  17588  neitx  17592  tx1cn  17594  tx2cn  17595  ptcld  17598  xkoccn  17604  txcnp  17605  ptcnp  17607  txcnmpt  17609  ptcn  17612  txdis1cn  17620  ptrescn  17624  txkgen  17637  xkoco1cn  17642  xkoco2cn  17643  xkococn  17645  xkoinjcn  17672  qtoptop2  17684  qtopuni  17687  qtopid  17690  qtopkgen  17695  basqtop  17696  tgqtop  17697  qtopss  17700  qtopeu  17701  qtoprest  17702  kqopn  17719  kqcld  17720  kqreglem2  17727  reghmph  17778  ordthmeolem  17786  qtopf1  17801  opnfbas  17827  isfil2  17841  fbasweak  17850  fsubbas  17852  filcon  17868  fbasrn  17869  rnelfmlem  17937  flimss2  17957  flimss1  17958  hausflim  17966  flimclslem  17969  flimsncls  17971  cnpflfi  17984  flfcnp2  17992  fclsfnflim  18012  cnextfvval  18049  cnextfres  18052  symgtgp  18084  opnsubg  18090  ghmcnp  18097  divstgpopn  18102  divstgplem  18103  divstgphaus  18105  tsmsfbas  18110  ustfilxp  18195  utoptop  18217  utopbas  18218  restutopopn  18221  iducn  18266  cstucnd  18267  ucncn  18268  fmucnd  18275  cfilufg  18276  trcfilu  18277  cfiluweak  18278  neipcfilu  18279  psmetsym  18294  isxmetd  18309  xmetsym  18330  imasdsf1olem  18356  imasf1oxmet  18358  xblss2ps  18384  xblss2  18385  xblcntrps  18393  xblcntr  18394  blcld  18488  metustfbasOLD  18548  metustfbas  18549  cfilucfilOLD  18552  cfilucfil  18553  restmetu  18570  ngptgp  18630  tngngpd  18647  tngnrg  18663  nlmvscn  18676  nrginvrcn  18680  nmo0  18722  nmoeq0  18723  nmoid  18729  nghmcn  18732  0nmhm  18742  blcvx  18782  zcld  18797  iccntr  18805  xrge0tsms  18818  xmetdcn2  18821  metdstri  18834  metdscn  18839  rescncf  18880  cncfco  18890  oprpiece1res2  18930  cnheibor  18933  cnllycmp  18934  bndth  18936  evth  18937  ishtpyd  18953  isphtpyd  18964  pcoval2  18994  nmhmcn  19081  ipcn  19153  lmnn  19169  cfilss  19176  iscfil3  19179  cfilfcls  19180  cmetcaulem  19194  iscmet3lem2  19198  cfilres  19202  lmcau  19218  flimcfil  19219  cncmet  19228  rlmbn  19268  minveclem3b  19282  pjthlem1  19291  pjth2  19294  ivthlem3  19303  ovolssnul  19336  ovolctb  19339  ovolunnul  19349  ovoliunnul  19356  ovolsca  19364  ovolicc  19372  ovolicopnf  19373  voliunlem2  19398  voliunlem3  19399  volsup  19403  uniioovol  19424  uniiccvol  19425  dyadmaxlem  19442  vitalilem5  19457  ismbfd  19485  mbfres  19489  mbfss  19491  mbfmulc2re  19493  mbfadd  19506  mbfmulc2  19508  mbflimsup  19511  mbflim  19513  i1faddlem  19538  i1fmullem  19539  mbfmul  19571  itg2itg1  19581  itg2seq  19587  itg2eqa  19590  itg2mulc  19592  itg2split  19594  itg2mono  19598  itg2cnlem1  19606  ibl0  19631  iblposlem  19636  itgreval  19641  iblneg  19647  iblss  19649  iblss2  19650  itgle  19654  iblconst  19662  iblabs  19673  iblabsr  19674  iblmulc2  19675  bddmulibl  19683  limciun  19734  limcun  19735  dvres2lem  19750  dvidlem  19755  dvcnp2  19759  dvcn  19760  cpnres  19776  dvaddbr  19777  dvmulbr  19778  dvcobr  19785  dvcjbr  19788  dvrec  19794  dvcnvlem  19813  dvferm  19825  dvlip2  19832  dveq0  19837  dv11cn  19838  dvivthlem1  19845  lhop1  19851  lhop2  19852  lhop  19853  dvcnvre  19856  dvfsumlem3  19865  dvfsumlem4  19866  dvfsumrlim  19868  dvfsum2  19871  ftc1a  19874  ftc1lem4  19876  ftc1lem6  19878  ftc1  19879  evlslem3  19888  mpfind  19918  coe1mul3  19975  deg1addle2  19978  deg1add  19979  deg1sublt  19986  deg1mul2  19990  deg1tm  19994  fta1blem  20044  drnguc1p  20046  ig1prsp  20053  plyco0  20064  plyeq0lem  20082  dgrub  20106  dgreq  20116  dgradd2  20139  dgrmul  20141  dgrcolem2  20145  dgrco  20146  plycpn  20159  plydivlem4  20166  plydiveu  20168  vieta1lem2  20181  vieta1  20182  aalioulem2  20203  aalioulem3  20204  aaliou3lem7  20219  tayl0  20231  ulmcn  20268  ulmdvlem3  20271  psercn  20295  abelth  20310  pilem3  20322  efif1olem1  20397  abslogimle  20424  argregt0  20458  argrege0  20459  logf1o2  20494  cxpsqrlem  20546  cxpcn3  20585  abscxpbnd  20590  ang180lem2  20605  ang180lem3  20606  logreclem  20613  xrlimcnp  20760  harmonicbnd4  20802  fsumharmonic  20803  basellem3  20818  basellem4  20819  dvdsppwf1o  20924  dvdsflf1o  20925  fsumfldivdiaglem  20927  chpeq0  20945  chteq0  20946  chtub  20949  chpub  20957  dchrelbasd  20976  dchrmulcl  20986  dchrinv  20998  bcmono  21014  bposlem1  21021  bposlem2  21022  lgslem1  21033  lgsdirprm  21066  lgsqrlem2  21079  lgsqrlem3  21080  lgsdchr  21085  lgseisenlem1  21086  lgseisenlem2  21087  lgseisenlem3  21088  lgsquadlem1  21091  2sqlem8  21109  2sqblem  21114  chebbnd1lem1  21116  dchrisumlem1  21136  dchrisumlem2  21137  dchrisumlem3  21138  dchrisum0fno1  21158  pntrmax  21211  pntpbnd1a  21232  pntibndlem3  21239  pntlemn  21247  pntlemi  21251  pntlem3  21256  pntleml  21258  ostth1  21280  ostth2  21284  ostth3  21285  cusgra0v  21422  cusgraexi  21430  cusgrares  21434  1pthon  21544  constr2spth  21553  2pthon  21555  constr3trllem3  21592  constr3cycl  21601  eupares  21650  eupap1  21651  nvabs  22115  vacn  22143  nmcvcn  22144  nmblore  22240  0lno  22244  0blo  22246  nmlno0lem  22247  occl  22759  pjhthlem1  22846  pjpjpre  22874  nmopre  23326  nmlnop0iALT  23451  nmophmi  23487  leoprf2  23583  stlesi  23697  disjdifprg  23970  fzspl  24102  xrge0tsmsd  24176  ofldaddlt  24194  ofldlt1  24196  kerf1hrm  24215  metider  24242  qqhval2lem  24318  qqhcn  24328  pwsiga  24466  prsiga  24467  measle0  24515  mbfmcst  24562  1stmbfm  24563  2ndmbfm  24564  imambfm  24565  cnmbfm  24566  mbfmco  24567  mbfmco2  24568  0rrv  24662  ballotlemfc0  24703  ballotlemfcc  24704  lgamgulmlem5  24770  lgambdd  24774  derangen  24811  subfacval3  24828  cvmseu  24916  cvmliftmolem2  24922  cvmliftlem7  24931  cvmliftlem15  24938  cvmlift2lem9a  24943  cvmlift2lem9  24951  cvmlift2lem10  24952  cvmlift2lem11  24953  cvmlift2lem12  24954  cvmlift3lem6  24964  cvmlift3lem8  24966  fznatpl1  25151  brbtwn2  25748  axlowdimlem3  25787  axlowdimlem16  25800  axcontlem8  25814  supaddc  26137  supadd  26138  mblfinlem  26143  ovoliunnfl  26147  volsupnfl  26150  mbfresfi  26152  itg2addnclem2  26156  iblabsnc  26168  iblmulc2nc  26169  ftc1cnnclem  26177  ftc1cnnc  26178  fness  26252  ssref  26253  fnetr  26256  reftr  26259  fnessref  26263  refssfne  26264  neibastop1  26278  neibastop2  26280  tailfb  26296  filnetlem3  26299  fzadd2  26335  sdclem2  26336  metf1o  26351  ismtyhmeolem  26403  ismtyres  26407  heibor1lem  26408  bfplem2  26422  bfp  26423  rrncmslem  26431  iccbnd  26439  icccmpALT  26440  rngogrphom  26477  rngoisoco  26488  keridl  26532  fzsplit1nn0  26702  icodiamlt  26773  irrapxlem3  26777  irrapxlem4  26778  pell1234qrdich  26814  pell1qr1  26824  pell14qrgap  26828  pellqrexplicit  26830  rmspecfund  26862  fzmaxdif  26936  acongeq  26938  jm2.23  26957  jm3.1  26981  lmhmlnmsplit  27053  dsmm0cl  27074  dsmmacl  27075  dsmmsubg  27077  dsmmlss  27078  uvcff  27108  frlmsplit2  27111  lindfrn  27159  f1lindf  27160  lindsss  27162  hbt  27202  dgrsub2  27207  proot1ex  27388  dvconstbi  27419  ubelsupr  27558  fmul01  27577  fmuldfeq  27580  climsuse  27601  stoweidlem7  27623  stoweidlem13  27629  stoweidlem26  27642  wallispilem3  27683  stirlinglem6  27695  stirlinglem10  27699  ubmelfzo  27986  fzo1fzo0n0  27988  usgra2wlkspth  28038  frgra0v  28097  frgra1v  28102  bnj1452  29127  lsmcv2  29512  lsatcv0  29514  lcvexchlem4  29520  lcvexchlem5  29521  l1cvpat  29537  lfl0f  29552  lfladdcl  29554  lflnegcl  29558  lkrlss  29578  eqlkr  29582  lkrlsp  29585  lkrlsp2  29586  lshpkrcl  29599  lkrin  29647  1cvrjat  29957  llni  29990  llnle  30000  lplni  30014  lplnle  30022  llncvrlpln2  30039  2atmat  30043  lvoli  30057  lplncvrlvol2  30097  elpaddri  30284  paddclN  30324  pclclN  30373  pclfinN  30382  0psubclN  30425  1psubclN  30426  atpsubclN  30427  pmapsubclN  30428  osumclN  30449  pexmidN  30451  pexmidlem6N  30457  lhp2lt  30483  lautcnv  30572  idlaut  30578  lautco  30579  idldil  30596  ldilcnv  30597  ldilco  30598  ltrncnv  30628  idltrn  30632  cdleme16d  30763  cdleme50laut  31029  cdleme50ldil  31030  cdleme50ltrn  31039  ltrnco  31201  dian0  31522  dia0eldmN  31523  dia1eldmN  31524  dialss  31529  diaintclN  31541  docaclN  31607  doca2N  31609  djajN  31620  dibintclN  31650  diblss  31653  dicvaddcl  31673  dicvscacl  31674  dicn0  31675  cdlemn11a  31690  dihord2cN  31704  dihord11b  31705  dihord6apre  31739  dihmeetlem1N  31773  dihglblem5apreN  31774  dihpN  31819  dihjatcclem4  31904  dochkr1  31961  islpoldN  31967  lcfrlem31  32056  mapdpglem18  32172  mapdheq2  32212  mapdheq4  32215  mapdh6aN  32218  hdmap1l6a  32293  hdmap1neglem1N  32311  hdmap14lem4a  32357
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