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

Theorem mpbir2and 888
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 518 . 2  |-  ( ph  ->  ( ch  /\  th ) )
4 mpbir2and.3 . 2  |-  ( ph  ->  ( ps  <->  ( ch  /\ 
th ) ) )
53, 4mpbird 223 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  dffi3  7186  supmax  7218  suppr  7221  ordtypelem7  7241  cantnfle  7374  cantnf0  7378  cantnfp1lem1  7382  cantnfp1lem2  7383  cantnfp1lem3  7384  oemapvali  7388  cantnflem1a  7389  cantnflem1c  7391  cantnflem1d  7392  cantnflem1  7393  cantnf  7397  mapfien  7401  rankpwi  7497  carduni  7616  fin23lem32  7972  fpwwe2lem6  8259  fpwwe2lem9  8262  fpwwe2lem12  8265  fpwwe2lem13  8266  fpwwe2  8267  inttsk  8398  grutsk1  8445  add20  9288  supmul  9724  suprzcl  10093  uzwo3  10313  rpnnen1lem5  10348  xrre  10500  xrre3  10502  xleadd1a  10575  xlemul1a  10610  supxrre  10648  infmxrre  10656  ixxub  10679  ixxlb  10680  elioc2  10715  elico2  10716  elicc2  10717  elfz1eq  10809  fzctr  10856  fzoaddel  10908  flid  10941  flval3  10947  fladdz  10952  fldiv  10966  modid  10995  seqf1olem1  11087  bcval5  11332  hashf1lem1  11395  sqeqd  11653  sqrlem7  11736  max0add  11797  abs2difabs  11820  rddif  11826  fzomaxdiflem  11828  rexico  11839  limsupgre  11957  rlim3  11974  icco1  12016  rlimclim  12022  rlimuni  12026  rlimresb  12041  isercolllem2  12141  isercolllem3  12142  isercoll  12143  caucvgrlem  12147  caurcvgr  12148  iseraltlem3  12158  fsum00  12258  o1fsum  12273  dvdseq  12578  bitsfzolem  12627  bitsfzo  12628  bitsmod  12629  bitscmp  12631  gcd0id  12704  gcdneg  12707  bezoutlem4  12722  nn0seqcvgd  12742  prmind2  12771  qredeq  12787  isprm5  12793  hashdvds  12845  eulerthlem2  12852  pcpremul  12898  pcidlem  12926  pcgcd1  12931  pcadd2  12940  fldivp1  12947  pcfaclem  12948  prmreclem5  12969  4sqlem17  13010  vdwlem1  13030  vdwlem6  13035  vdwlem12  13041  vdwlem13  13042  0ram  13069  ram0  13071  ramub1lem1  13075  invco  13675  sectmon  13682  monsect  13683  ssctr  13704  ssceq  13705  issubc3  13725  fullsubc  13726  funcinv  13749  fthmon  13803  fuccocl  13840  fucidcl  13841  invfuc  13850  elhomai  13867  setcmon  13921  setcepi  13922  catcisolem  13940  curf2cl  14007  yonedalem4c  14053  yonedalem3  14056  yoniso  14061  isacs3lem  14271  tsrdir  14362  nmznsg  14663  ghmpreima  14706  ghmeql  14707  ghmnsgpreima  14709  cntzsubm  14813  cntzsubg  14814  cntzmhm  14816  odlem2  14856  gexlem2  14895  gexcl2  14902  sylow1lem5  14915  subgslw  14929  slwhash  14937  fislw  14938  sylow3lem1  14940  lsmsubg  14967  efgredlemd  15055  efgredlem  15058  efgcpbllemb  15066  frgpuplem  15083  cyggeninv  15172  iscygd  15176  iscygodd  15177  gsumconst  15211  gsumpt  15224  dprdfcntz  15252  eldprdi  15255  subgdmdprd  15271  subgdprd  15272  dprdpr  15287  ablfac1c  15308  ablfac1eu  15310  ablfaclem3  15324  issubdrg  15572  rhmeql  15577  rhmima  15578  cntzsubr  15579  isabvd  15587  abvdiv  15604  lsslsp  15774  lmhmima  15806  lmhmpreima  15807  lmhmeql  15814  lsmcl  15838  lspfixed  15883  issubassa  16066  issubassa2  16086  psrbaglesupp  16116  psrbaglecl  16117  psrbagaddcl  16118  psrbagcon  16119  psrbas  16126  psrlidm  16150  psrridm  16151  mvridlem  16166  mplsubglem  16181  mpllsslem  16182  mplassa  16200  subrgmpl  16206  mplcoe3  16212  mplcoe2  16213  mplbas2  16214  mplind  16245  ply1assa  16280  coe1tmmul2  16354  coe1tmmul  16355  qsssubdrg  16433  gzrngunit  16439  ocvpj  16619  distop  16735  indistopon  16740  ppttop  16746  epttop  16748  mretopd  16831  toponmre  16832  neiss  16848  opnneissb  16853  ssnei2  16855  innei  16864  ordtcld1  16929  ordtcld2  16930  lmconst  16993  cnpnei  16995  iscncl  17000  cnss1  17007  cnss2  17008  cncnpi  17009  cncnp  17011  cnconst2  17013  cnrest  17015  cnpresti  17018  cnpdis  17023  paste  17024  lmcnp  17034  cnhaus  17084  hauscmp  17136  2ndcomap  17186  1stcelcls  17189  1stccnp  17190  llyrest  17213  nllyrest  17214  llyidm  17216  nllyidm  17217  kgentopon  17235  kgenidm  17244  kgencn3  17255  txcld  17300  tx1cn  17305  tx2cn  17306  ptcld  17309  xkoccn  17315  txcnp  17316  ptcnp  17318  txcnmpt  17320  ptcn  17323  txdis1cn  17331  ptrescn  17335  txkgen  17348  xkoco1cn  17353  xkoco2cn  17354  xkococn  17356  xkoinjcn  17383  qtoptop2  17392  qtopuni  17395  qtopid  17398  qtopkgen  17403  basqtop  17404  tgqtop  17405  qtopss  17408  qtopeu  17409  qtoprest  17410  kqopn  17427  kqcld  17428  kqreglem2  17435  reghmph  17486  ordthmeolem  17494  qtopf1  17509  opnfbas  17539  isfil2  17553  fbasweak  17562  fsubbas  17564  filcon  17580  fbasrn  17581  rnelfmlem  17649  flimss2  17669  flimss1  17670  hausflim  17678  flimclslem  17681  flimsncls  17683  cnpflfi  17696  flfcnp2  17704  fclsfnflim  17724  symgtgp  17786  opnsubg  17792  ghmcnp  17799  divstgpopn  17804  divstgplem  17805  divstgphaus  17807  tsmsfbas  17812  isxmetd  17893  xmetsym  17914  imasdsf1olem  17939  imasf1oxmet  17941  xblss2  17960  xblcntr  17965  blcld  18053  ngptgp  18154  tngngpd  18171  tngnrg  18187  nlmvscn  18200  nrginvrcn  18204  nmo0  18246  nmoeq0  18247  nmoid  18253  nghmcn  18256  0nmhm  18266  blcvx  18306  zcld  18321  iccntr  18328  xrge0tsms  18341  xmetdcn2  18344  metdstri  18357  metdscn  18362  rescncf  18403  cncfco  18413  oprpiece1res2  18452  cnheibor  18455  cnllycmp  18456  bndth  18458  evth  18459  ishtpyd  18475  isphtpyd  18486  pcoval2  18516  nmhmcn  18603  ipcn  18675  lmnn  18691  cfilss  18698  iscfil3  18701  cfilfcls  18702  cmetcaulem  18716  iscmet3lem2  18720  cfilres  18724  lmcau  18740  flimcfil  18741  cncmet  18746  rlmbn  18780  minveclem3b  18794  pjthlem1  18803  pjth2  18806  ivthlem3  18815  ovolssnul  18848  ovolctb  18851  ovolunnul  18861  ovoliunnul  18868  ovolsca  18876  ovolicc  18884  ovolicopnf  18885  voliunlem2  18910  voliunlem3  18911  volsup  18915  uniioovol  18936  uniiccvol  18937  dyadmaxlem  18954  vitalilem5  18969  ismbfd  18997  mbfres  19001  mbfss  19003  mbfmulc2re  19005  mbfadd  19018  mbfmulc2  19020  mbflimsup  19023  mbflim  19025  i1faddlem  19050  i1fmullem  19051  mbfmul  19083  itg2itg1  19093  itg2seq  19099  itg2eqa  19102  itg2mulc  19104  itg2split  19106  itg2mono  19110  itg2cnlem1  19118  ibl0  19143  iblposlem  19148  itgreval  19153  iblneg  19159  iblss  19161  iblss2  19162  itgle  19166  iblconst  19174  iblabs  19185  iblabsr  19186  iblmulc2  19187  bddmulibl  19195  limciun  19246  limcun  19247  dvres2lem  19262  dvidlem  19267  dvcnp2  19271  dvcn  19272  cpnres  19288  dvaddbr  19289  dvmulbr  19290  dvcobr  19297  dvcjbr  19300  dvrec  19306  dvcnvlem  19325  dvferm  19337  dvlip2  19344  dveq0  19349  dv11cn  19350  dvivthlem1  19357  lhop1  19363  lhop2  19364  lhop  19365  dvcnvre  19368  dvfsumlem3  19377  dvfsumlem4  19378  dvfsumrlim  19380  dvfsum2  19383  ftc1a  19386  ftc1lem4  19388  ftc1lem6  19390  ftc1  19391  evlslem3  19400  mpfind  19430  coe1mul3  19487  deg1addle2  19490  deg1add  19491  deg1sublt  19498  deg1mul2  19502  deg1tm  19506  fta1blem  19556  drnguc1p  19558  ig1prsp  19565  plyco0  19576  plyeq0lem  19594  dgrub  19618  dgreq  19628  dgradd2  19651  dgrmul  19653  dgrcolem2  19657  dgrco  19658  plycpn  19671  plydivlem4  19678  plydiveu  19680  vieta1lem2  19693  vieta1  19694  aalioulem2  19715  aalioulem3  19716  aaliou3lem7  19731  tayl0  19743  ulmcn  19778  ulmdvlem3  19781  psercn  19804  abelth  19819  pilem3  19831  efif1olem1  19906  argregt0  19966  argrege0  19967  logf1o2  19999  cxpsqrlem  20051  cxpcn3  20090  abscxpbnd  20095  ang180lem2  20110  ang180lem3  20111  logreclem  20118  xrlimcnp  20265  harmonicbnd4  20306  fsumharmonic  20307  basellem3  20322  basellem4  20323  dvdsppwf1o  20428  dvdsflf1o  20429  fsumfldivdiaglem  20431  chpeq0  20449  chteq0  20450  chtub  20453  chpub  20461  dchrelbasd  20480  dchrmulcl  20490  dchrinv  20502  bcmono  20518  bposlem1  20525  bposlem2  20526  lgslem1  20537  lgsdirprm  20570  lgsqrlem2  20583  lgsqrlem3  20584  lgsdchr  20589  lgseisenlem1  20590  lgseisenlem2  20591  lgseisenlem3  20592  lgsquadlem1  20595  2sqlem8  20613  2sqblem  20618  chebbnd1lem1  20620  dchrisumlem1  20640  dchrisumlem2  20641  dchrisumlem3  20642  dchrisum0fno1  20662  pntrmax  20715  pntpbnd1a  20736  pntibndlem3  20743  pntlemn  20751  pntlemi  20755  pntlem3  20760  pntleml  20762  ostth1  20784  ostth2  20788  ostth3  20789  nvabs  21241  vacn  21269  nmcvcn  21270  nmblore  21366  0lno  21370  0blo  21372  nmlno0lem  21373  occl  21885  pjhthlem1  21972  pjpjpre  22000  nmopre  22452  nmlnop0iALT  22577  nmophmi  22613  leoprf2  22709  stlesi  22823  xrre3FL  23253  xrge0tsmsd  23384  mbfmcst  23566  imambfm  23569  mbfmco  23571  0rrv  23656  derangen  23705  subfacval3  23722  cvmseu  23809  cvmliftmolem2  23815  cvmliftlem7  23824  cvmliftlem15  23831  cvmlift2lem9a  23836  cvmlift2lem9  23844  cvmlift2lem10  23845  cvmlift2lem11  23846  cvmlift2lem12  23847  cvmlift3lem6  23857  cvmlift3lem8  23859  eupares  23901  eupap1  23902  fznatpl1  24095  brbtwn2  24535  axlowdimlem3  24574  axlowdimlem16  24587  axcontlem8  24601  supaddc  24927  supadd  24928  itg2addnclem2  24934  eqfnung2  25129  repfuntw  25171  prltub  25271  ubpar  25272  supaub  25284  geme2  25286  inttop2  25526  intopcoaconb  25551  intopcoaconc  25552  qusp  25553  prcnt  25562  cmptdst  25579  prdnei  25584  tcnvec  25701  aidm2  25761  dualalg  25793  idfisf  25852  idsubfun  25869  setiscat  25990  lppotos  26155  fness  26293  ssref  26294  fnetr  26297  reftr  26300  fnessref  26304  refssfne  26305  neibastop1  26319  neibastop2  26321  tailfb  26337  filnetlem3  26340  fzadd2  26455  sdclem2  26463  metf1o  26480  ismtyhmeolem  26539  ismtyres  26543  heibor1lem  26544  bfplem2  26558  bfp  26559  rrncmslem  26567  iccbnd  26575  icccmpALT  26576  rngogrphom  26613  rngoisoco  26624  keridl  26668  fzsplit1nn0  26844  icodiamlt  26916  irrapxlem3  26920  irrapxlem4  26921  pell1234qrdich  26957  pell1qr1  26967  pell14qrgap  26971  pellqrexplicit  26973  rmspecfund  27005  fzmaxdif  27079  acongeq  27081  jm2.23  27100  jm3.1  27124  lmhmlnmsplit  27196  dsmm0cl  27217  dsmmacl  27218  dsmmsubg  27220  dsmmlss  27221  uvcff  27251  frlmsplit2  27254  lindfrn  27302  f1lindf  27303  lindsss  27305  hbt  27345  dgrsub2  27350  proot1ex  27531  dvconstbi  27562  cusgra0v  28167  frgra0v  28185  frgra1v  28187  bnj1452  29155  lsmcv2  29292  lsatcv0  29294  lcvexchlem4  29300  lcvexchlem5  29301  l1cvpat  29317  lfl0f  29332  lfladdcl  29334  lflnegcl  29338  lkrlss  29358  eqlkr  29362  lkrlsp  29365  lkrlsp2  29366  lshpkrcl  29379  lkrin  29427  1cvrjat  29737  llni  29770  llnle  29780  lplni  29794  lplnle  29802  llncvrlpln2  29819  2atmat  29823  lvoli  29837  lplncvrlvol2  29877  elpaddri  30064  paddclN  30104  pclclN  30153  pclfinN  30162  0psubclN  30205  1psubclN  30206  atpsubclN  30207  pmapsubclN  30208  osumclN  30229  pexmidN  30231  pexmidlem6N  30237  lhp2lt  30263  lautcnv  30352  idlaut  30358  lautco  30359  idldil  30376  ldilcnv  30377  ldilco  30378  ltrncnv  30408  idltrn  30412  cdleme16d  30543  cdleme50laut  30809  cdleme50ldil  30810  cdleme50ltrn  30819  ltrnco  30981  dian0  31302  dia0eldmN  31303  dia1eldmN  31304  dialss  31309  diaintclN  31321  docaclN  31387  doca2N  31389  djajN  31400  dibintclN  31430  diblss  31433  dicvaddcl  31453  dicvscacl  31454  dicn0  31455  cdlemn11a  31470  dihord2cN  31484  dihord11b  31485  dihord6apre  31519  dihmeetlem1N  31553  dihglblem5apreN  31554  dihpN  31599  dihjatcclem4  31684  dochkr1  31741  islpoldN  31747  lcfrlem31  31836  mapdpglem18  31952  mapdheq2  31992  mapdheq4  31995  mapdh6aN  31998  hdmap1l6a  32073  hdmap1neglem1N  32091  hdmap14lem4a  32137
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 177  df-an 360
  Copyright terms: Public domain W3C validator