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  7200  supmax  7232  suppr  7235  ordtypelem7  7255  cantnfle  7388  cantnf0  7392  cantnfp1lem1  7396  cantnfp1lem2  7397  cantnfp1lem3  7398  oemapvali  7402  cantnflem1a  7403  cantnflem1c  7405  cantnflem1d  7406  cantnflem1  7407  cantnf  7411  mapfien  7415  rankpwi  7511  carduni  7630  fin23lem32  7986  fpwwe2lem6  8273  fpwwe2lem9  8276  fpwwe2lem12  8279  fpwwe2lem13  8280  fpwwe2  8281  inttsk  8412  grutsk1  8459  add20  9302  supmul  9738  suprzcl  10107  uzwo3  10327  rpnnen1lem5  10362  xrre  10514  xrre3  10516  xleadd1a  10589  xlemul1a  10624  supxrre  10662  infmxrre  10670  ixxub  10693  ixxlb  10694  elioc2  10729  elico2  10730  elicc2  10731  elfz1eq  10823  fzctr  10870  fzoaddel  10922  flid  10955  flval3  10961  fladdz  10966  fldiv  10980  modid  11009  seqf1olem1  11101  bcval5  11346  hashf1lem1  11409  sqeqd  11667  sqrlem7  11750  max0add  11811  abs2difabs  11834  rddif  11840  fzomaxdiflem  11842  rexico  11853  limsupgre  11971  rlim3  11988  icco1  12030  rlimclim  12036  rlimuni  12040  rlimresb  12055  isercolllem2  12155  isercolllem3  12156  isercoll  12157  caucvgrlem  12161  caurcvgr  12162  iseraltlem3  12172  fsum00  12272  o1fsum  12287  dvdseq  12592  bitsfzolem  12641  bitsfzo  12642  bitsmod  12643  bitscmp  12645  gcd0id  12718  gcdneg  12721  bezoutlem4  12736  nn0seqcvgd  12756  prmind2  12785  qredeq  12801  isprm5  12807  hashdvds  12859  eulerthlem2  12866  pcpremul  12912  pcidlem  12940  pcgcd1  12945  pcadd2  12954  fldivp1  12961  pcfaclem  12962  prmreclem5  12983  4sqlem17  13024  vdwlem1  13044  vdwlem6  13049  vdwlem12  13055  vdwlem13  13056  0ram  13083  ram0  13085  ramub1lem1  13089  invco  13689  sectmon  13696  monsect  13697  ssctr  13718  ssceq  13719  issubc3  13739  fullsubc  13740  funcinv  13763  fthmon  13817  fuccocl  13854  fucidcl  13855  invfuc  13864  elhomai  13881  setcmon  13935  setcepi  13936  catcisolem  13954  curf2cl  14021  yonedalem4c  14067  yonedalem3  14070  yoniso  14075  isacs3lem  14285  tsrdir  14376  nmznsg  14677  ghmpreima  14720  ghmeql  14721  ghmnsgpreima  14723  cntzsubm  14827  cntzsubg  14828  cntzmhm  14830  odlem2  14870  gexlem2  14909  gexcl2  14916  sylow1lem5  14929  subgslw  14943  slwhash  14951  fislw  14952  sylow3lem1  14954  lsmsubg  14981  efgredlemd  15069  efgredlem  15072  efgcpbllemb  15080  frgpuplem  15097  cyggeninv  15186  iscygd  15190  iscygodd  15191  gsumconst  15225  gsumpt  15238  dprdfcntz  15266  eldprdi  15269  subgdmdprd  15285  subgdprd  15286  dprdpr  15301  ablfac1c  15322  ablfac1eu  15324  ablfaclem3  15338  issubdrg  15586  rhmeql  15591  rhmima  15592  cntzsubr  15593  isabvd  15601  abvdiv  15618  lsslsp  15788  lmhmima  15820  lmhmpreima  15821  lmhmeql  15828  lsmcl  15852  lspfixed  15897  issubassa  16080  issubassa2  16100  psrbaglesupp  16130  psrbaglecl  16131  psrbagaddcl  16132  psrbagcon  16133  psrbas  16140  psrlidm  16164  psrridm  16165  mvridlem  16180  mplsubglem  16195  mpllsslem  16196  mplassa  16214  subrgmpl  16220  mplcoe3  16226  mplcoe2  16227  mplbas2  16228  mplind  16259  ply1assa  16294  coe1tmmul2  16368  coe1tmmul  16369  qsssubdrg  16447  gzrngunit  16453  ocvpj  16633  distop  16749  indistopon  16754  ppttop  16760  epttop  16762  mretopd  16845  toponmre  16846  neiss  16862  opnneissb  16867  ssnei2  16869  innei  16878  ordtcld1  16943  ordtcld2  16944  lmconst  17007  cnpnei  17009  iscncl  17014  cnss1  17021  cnss2  17022  cncnpi  17023  cncnp  17025  cnconst2  17027  cnrest  17029  cnpresti  17032  cnpdis  17037  paste  17038  lmcnp  17048  cnhaus  17098  hauscmp  17150  2ndcomap  17200  1stcelcls  17203  1stccnp  17204  llyrest  17227  nllyrest  17228  llyidm  17230  nllyidm  17231  kgentopon  17249  kgenidm  17258  kgencn3  17269  txcld  17314  tx1cn  17319  tx2cn  17320  ptcld  17323  xkoccn  17329  txcnp  17330  ptcnp  17332  txcnmpt  17334  ptcn  17337  txdis1cn  17345  ptrescn  17349  txkgen  17362  xkoco1cn  17367  xkoco2cn  17368  xkococn  17370  xkoinjcn  17397  qtoptop2  17406  qtopuni  17409  qtopid  17412  qtopkgen  17417  basqtop  17418  tgqtop  17419  qtopss  17422  qtopeu  17423  qtoprest  17424  kqopn  17441  kqcld  17442  kqreglem2  17449  reghmph  17500  ordthmeolem  17508  qtopf1  17523  opnfbas  17553  isfil2  17567  fbasweak  17576  fsubbas  17578  filcon  17594  fbasrn  17595  rnelfmlem  17663  flimss2  17683  flimss1  17684  hausflim  17692  flimclslem  17695  flimsncls  17697  cnpflfi  17710  flfcnp2  17718  fclsfnflim  17738  symgtgp  17800  opnsubg  17806  ghmcnp  17813  divstgpopn  17818  divstgplem  17819  divstgphaus  17821  tsmsfbas  17826  isxmetd  17907  xmetsym  17928  imasdsf1olem  17953  imasf1oxmet  17955  xblss2  17974  xblcntr  17979  blcld  18067  ngptgp  18168  tngngpd  18185  tngnrg  18201  nlmvscn  18214  nrginvrcn  18218  nmo0  18260  nmoeq0  18261  nmoid  18267  nghmcn  18270  0nmhm  18280  blcvx  18320  zcld  18335  iccntr  18342  xrge0tsms  18355  xmetdcn2  18358  metdstri  18371  metdscn  18376  rescncf  18417  cncfco  18427  oprpiece1res2  18466  cnheibor  18469  cnllycmp  18470  bndth  18472  evth  18473  ishtpyd  18489  isphtpyd  18500  pcoval2  18530  nmhmcn  18617  ipcn  18689  lmnn  18705  cfilss  18712  iscfil3  18715  cfilfcls  18716  cmetcaulem  18730  iscmet3lem2  18734  cfilres  18738  lmcau  18754  flimcfil  18755  cncmet  18760  rlmbn  18794  minveclem3b  18808  pjthlem1  18817  pjth2  18820  ivthlem3  18829  ovolssnul  18862  ovolctb  18865  ovolunnul  18875  ovoliunnul  18882  ovolsca  18890  ovolicc  18898  ovolicopnf  18899  voliunlem2  18924  voliunlem3  18925  volsup  18929  uniioovol  18950  uniiccvol  18951  dyadmaxlem  18968  vitalilem5  18983  ismbfd  19011  mbfres  19015  mbfss  19017  mbfmulc2re  19019  mbfadd  19032  mbfmulc2  19034  mbflimsup  19037  mbflim  19039  i1faddlem  19064  i1fmullem  19065  mbfmul  19097  itg2itg1  19107  itg2seq  19113  itg2eqa  19116  itg2mulc  19118  itg2split  19120  itg2mono  19124  itg2cnlem1  19132  ibl0  19157  iblposlem  19162  itgreval  19167  iblneg  19173  iblss  19175  iblss2  19176  itgle  19180  iblconst  19188  iblabs  19199  iblabsr  19200  iblmulc2  19201  bddmulibl  19209  limciun  19260  limcun  19261  dvres2lem  19276  dvidlem  19281  dvcnp2  19285  dvcn  19286  cpnres  19302  dvaddbr  19303  dvmulbr  19304  dvcobr  19311  dvcjbr  19314  dvrec  19320  dvcnvlem  19339  dvferm  19351  dvlip2  19358  dveq0  19363  dv11cn  19364  dvivthlem1  19371  lhop1  19377  lhop2  19378  lhop  19379  dvcnvre  19382  dvfsumlem3  19391  dvfsumlem4  19392  dvfsumrlim  19394  dvfsum2  19397  ftc1a  19400  ftc1lem4  19402  ftc1lem6  19404  ftc1  19405  evlslem3  19414  mpfind  19444  coe1mul3  19501  deg1addle2  19504  deg1add  19505  deg1sublt  19512  deg1mul2  19516  deg1tm  19520  fta1blem  19570  drnguc1p  19572  ig1prsp  19579  plyco0  19590  plyeq0lem  19608  dgrub  19632  dgreq  19642  dgradd2  19665  dgrmul  19667  dgrcolem2  19671  dgrco  19672  plycpn  19685  plydivlem4  19692  plydiveu  19694  vieta1lem2  19707  vieta1  19708  aalioulem2  19729  aalioulem3  19730  aaliou3lem7  19745  tayl0  19757  ulmcn  19792  ulmdvlem3  19795  psercn  19818  abelth  19833  pilem3  19845  efif1olem1  19920  argregt0  19980  argrege0  19981  logf1o2  20013  cxpsqrlem  20065  cxpcn3  20104  abscxpbnd  20109  ang180lem2  20124  ang180lem3  20125  logreclem  20132  xrlimcnp  20279  harmonicbnd4  20320  fsumharmonic  20321  basellem3  20336  basellem4  20337  dvdsppwf1o  20442  dvdsflf1o  20443  fsumfldivdiaglem  20445  chpeq0  20463  chteq0  20464  chtub  20467  chpub  20475  dchrelbasd  20494  dchrmulcl  20504  dchrinv  20516  bcmono  20532  bposlem1  20539  bposlem2  20540  lgslem1  20551  lgsdirprm  20584  lgsqrlem2  20597  lgsqrlem3  20598  lgsdchr  20603  lgseisenlem1  20604  lgseisenlem2  20605  lgseisenlem3  20606  lgsquadlem1  20609  2sqlem8  20627  2sqblem  20632  chebbnd1lem1  20634  dchrisumlem1  20654  dchrisumlem2  20655  dchrisumlem3  20656  dchrisum0fno1  20676  pntrmax  20729  pntpbnd1a  20750  pntibndlem3  20757  pntlemn  20765  pntlemi  20769  pntlem3  20774  pntleml  20776  ostth1  20798  ostth2  20802  ostth3  20803  nvabs  21255  vacn  21283  nmcvcn  21284  nmblore  21380  0lno  21384  0blo  21386  nmlno0lem  21387  occl  21899  pjhthlem1  21986  pjpjpre  22014  nmopre  22466  nmlnop0iALT  22591  nmophmi  22627  leoprf2  22723  stlesi  22837  xrre3FL  23266  xrge0tsmsd  23397  mbfmcst  23579  imambfm  23582  mbfmco  23584  0rrv  23669  derangen  23718  subfacval3  23735  cvmseu  23822  cvmliftmolem2  23828  cvmliftlem7  23837  cvmliftlem15  23844  cvmlift2lem9a  23849  cvmlift2lem9  23857  cvmlift2lem10  23858  cvmlift2lem11  23859  cvmlift2lem12  23860  cvmlift3lem6  23870  cvmlift3lem8  23872  eupares  23914  eupap1  23915  fznatpl1  24108  brbtwn2  24605  axlowdimlem3  24644  axlowdimlem16  24657  axcontlem8  24671  supaddc  24995  supadd  24996  ovoliunnfl  25001  itg2addnclem2  25004  iblabsnc  25015  iblmulc2nc  25016  ftc1cnnclem  25024  ftc1cnnc  25025  eqfnung2  25221  repfuntw  25263  prltub  25363  ubpar  25364  supaub  25376  geme2  25378  inttop2  25618  intopcoaconb  25643  intopcoaconc  25644  qusp  25645  prcnt  25654  cmptdst  25671  prdnei  25676  tcnvec  25793  aidm2  25853  dualalg  25885  idfisf  25944  idsubfun  25961  setiscat  26082  lppotos  26247  fness  26385  ssref  26386  fnetr  26389  reftr  26392  fnessref  26396  refssfne  26397  neibastop1  26411  neibastop2  26413  tailfb  26429  filnetlem3  26432  fzadd2  26547  sdclem2  26555  metf1o  26572  ismtyhmeolem  26631  ismtyres  26635  heibor1lem  26636  bfplem2  26650  bfp  26651  rrncmslem  26659  iccbnd  26667  icccmpALT  26668  rngogrphom  26705  rngoisoco  26716  keridl  26760  fzsplit1nn0  26936  icodiamlt  27008  irrapxlem3  27012  irrapxlem4  27013  pell1234qrdich  27049  pell1qr1  27059  pell14qrgap  27063  pellqrexplicit  27065  rmspecfund  27097  fzmaxdif  27171  acongeq  27173  jm2.23  27192  jm3.1  27216  lmhmlnmsplit  27288  dsmm0cl  27309  dsmmacl  27310  dsmmsubg  27312  dsmmlss  27313  uvcff  27343  frlmsplit2  27346  lindfrn  27394  f1lindf  27395  lindsss  27397  hbt  27437  dgrsub2  27442  proot1ex  27623  dvconstbi  27654  cusgra0v  28295  constr3trllem3  28398  constr3cycl  28407  frgra0v  28420  frgra1v  28422  bnj1452  29398  lsmcv2  29841  lsatcv0  29843  lcvexchlem4  29849  lcvexchlem5  29850  l1cvpat  29866  lfl0f  29881  lfladdcl  29883  lflnegcl  29887  lkrlss  29907  eqlkr  29911  lkrlsp  29914  lkrlsp2  29915  lshpkrcl  29928  lkrin  29976  1cvrjat  30286  llni  30319  llnle  30329  lplni  30343  lplnle  30351  llncvrlpln2  30368  2atmat  30372  lvoli  30386  lplncvrlvol2  30426  elpaddri  30613  paddclN  30653  pclclN  30702  pclfinN  30711  0psubclN  30754  1psubclN  30755  atpsubclN  30756  pmapsubclN  30757  osumclN  30778  pexmidN  30780  pexmidlem6N  30786  lhp2lt  30812  lautcnv  30901  idlaut  30907  lautco  30908  idldil  30925  ldilcnv  30926  ldilco  30927  ltrncnv  30957  idltrn  30961  cdleme16d  31092  cdleme50laut  31358  cdleme50ldil  31359  cdleme50ltrn  31368  ltrnco  31530  dian0  31851  dia0eldmN  31852  dia1eldmN  31853  dialss  31858  diaintclN  31870  docaclN  31936  doca2N  31938  djajN  31949  dibintclN  31979  diblss  31982  dicvaddcl  32002  dicvscacl  32003  dicn0  32004  cdlemn11a  32019  dihord2cN  32033  dihord11b  32034  dihord6apre  32068  dihmeetlem1N  32102  dihglblem5apreN  32103  dihpN  32148  dihjatcclem4  32233  dochkr1  32290  islpoldN  32296  lcfrlem31  32385  mapdpglem18  32501  mapdheq2  32541  mapdheq4  32544  mapdh6aN  32547  hdmap1l6a  32622  hdmap1neglem1N  32640  hdmap14lem4a  32686
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