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

Theorem mpbir2and 913
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  5895  fnprb  5931  fnprOLD  5932  fdmfifsupp  7622  fczfsuppd  7630  fsuppmptif  7641  fsuppco2  7644  fsuppcor  7645  dffi3  7673  supmax  7707  suppr  7710  ordtypelem7  7730  cantnf0  7875  cantnfp1lem1  7878  cantnfp1lem2  7879  cantnfp1lem3  7880  cantnflem1a  7885  cantnflem1d  7888  cantnflem1  7889  cantnf  7893  cantnfleOLD  7901  cantnfp1lem1OLD  7904  cantnfp1lem2OLD  7905  cantnfp1lem3OLD  7906  cantnflem1aOLD  7908  cantnflem1cOLD  7910  cantnflem1dOLD  7911  cantnflem1OLD  7912  cantnfOLD  7915  mapfienOLD  7919  rankpwi  8022  carduni  8143  fin23lem32  8505  fpwwe2lem6  8794  fpwwe2lem9  8797  fpwwe2lem12  8800  fpwwe2lem13  8801  fpwwe2  8802  inttsk  8933  grutsk1  8980  add20  9843  supmul  10290  suprzcl  10713  uzwo3  10940  rpnnen1lem5  10975  xrre  11133  xrre3  11135  xleadd1a  11208  xlemul1a  11243  supxrre  11282  infmxrre  11290  ixxub  11313  ixxlb  11314  elioc2  11350  elico2  11351  elicc2  11352  elfz1eq  11454  fznatpl1  11502  nn0fz0  11517  fzctr  11521  fzo1fzo0n0  11580  fzoaddel  11589  flid  11649  flval3  11655  fladdz  11662  fldiv  11691  modid  11724  seqf1olem1  11837  bcval5  12086  hashf1lem1  12200  sqeqd  12647  sqrlem7  12730  max0add  12791  abs2difabs  12814  rddif  12820  fzomaxdiflem  12822  rexico  12833  limsupgre  12951  rlim3  12968  icco1  13010  rlimclim  13016  rlimuni  13020  rlimresb  13035  isercolllem2  13135  isercolllem3  13136  isercoll  13137  caucvgrlem  13142  caurcvgr  13143  iseraltlem3  13153  fsum00  13253  o1fsum  13268  dvdseq  13572  bitsfzolem  13622  bitsfzo  13623  bitsmod  13624  bitscmp  13626  gcd0id  13699  gcdneg  13702  bezoutlem4  13717  nn0seqcvgd  13737  prmind2  13766  qredeq  13784  isprm5  13790  hashdvds  13842  eulerthlem2  13849  pcpremul  13902  pcidlem  13930  pcgcd1  13935  pcadd2  13944  fldivp1  13951  pcfaclem  13952  prmreclem5  13973  4sqlem17  14014  vdwlem1  14034  vdwlem6  14039  vdwlem12  14045  vdwlem13  14046  0ram  14073  ram0  14075  ramub1lem1  14079  invco  14701  sectmon  14708  monsect  14709  ssctr  14730  ssceq  14731  issubc3  14751  fullsubc  14752  funcinv  14775  fthmon  14829  fuccocl  14866  fucidcl  14867  invfuc  14876  elhomai  14893  setcmon  14947  setcepi  14948  catcisolem  14966  curf2cl  15033  yonedalem4c  15079  yonedalem3  15082  yoniso  15087  lublecl  15151  isacs3lem  15328  tsrdir  15400  nmznsg  15716  ghmpreima  15759  ghmeql  15760  ghmnsgpreima  15762  cntzsubm  15844  cntzsubg  15845  cntzmhm  15847  symgextfo  15918  symgfixf1  15934  symgfixfolem1  15935  odlem2  16033  gexlem2  16072  gexcl2  16079  sylow1lem5  16092  subgslw  16106  slwhash  16114  fislw  16115  sylow3lem1  16117  lsmsubg  16144  efgredlemd  16232  efgredlem  16235  efgcpbllemb  16243  frgpuplem  16260  cyggeninv  16351  iscygd  16355  iscygodd  16356  gsumzadd  16400  gsumconst  16417  gsumpt  16443  gsumptOLD  16444  gsum2dlem2  16450  gsum2d  16451  gsum2d2lem  16453  dprdfcntz  16487  dprdfcntzOLD  16493  eldprdi  16496  eldprdiOLD  16503  subgdmdprd  16519  subgdprd  16520  dprdpr  16537  ablfac1c  16560  ablfac1eu  16562  ablfaclem3  16576  issubdrg  16868  rhmeql  16873  rhmima  16874  cntzsubr  16875  isabvd  16883  abvdiv  16900  lsslsp  17073  lmhmima  17105  lmhmpreima  17106  lmhmeql  17113  lsmcl  17141  lspfixed  17186  issubassa  17372  issubassa2  17392  snifpsrbag  17410  psrbaglesupp  17412  psrbaglesuppOLD  17413  psrbaglecl  17414  psrbagaddcl  17415  psrbagaddclOLD  17416  psrbagcon  17417  psrbasOLD  17426  psrlidmOLD  17452  psrridmOLD  17454  mvridlemOLD  17469  mplsubglem  17487  mpllsslem  17488  mplsubglemOLD  17489  mpllsslemOLD  17490  mplassa  17510  subrgmpl  17516  mplcoe3OLD  17523  mplcoe2  17524  mplcoe2OLD  17525  mplbas2  17526  mplbas2OLD  17527  mplind  17559  evlslem3  17575  mpfind  17597  ply1assa  17630  coe1tmmul2  17704  coe1tmmul  17705  qsssubdrg  17847  gzrngunit  17853  evpmodpmf1o  18001  ocvpj  18117  dsmm0cl  18140  dsmmacl  18141  dsmmsubg  18143  dsmmlss  18144  frlmsplit2  18172  uvcff  18191  lindfrn  18225  f1lindf  18226  lindsss  18228  mdet0pr  18378  distop  18575  indistopon  18580  ppttop  18586  epttop  18588  mretopd  18671  toponmre  18672  neiss  18688  opnneissb  18693  ssnei2  18695  innei  18704  neiptoptop  18710  ordtcld1  18776  ordtcld2  18777  lmconst  18840  cnpnei  18843  iscncl  18848  cnss1  18855  cnss2  18856  cncnpi  18857  cncnp  18859  cnconst2  18862  cnrest  18864  cnpresti  18867  cnpdis  18872  paste  18873  lmcnp  18883  cnhaus  18933  hauscmp  18985  2ndcomap  19037  1stcelcls  19040  1stccnp  19041  llyrest  19064  nllyrest  19065  llyidm  19067  nllyidm  19068  kgentopon  19086  kgenidm  19095  kgencn3  19106  txcld  19151  neitx  19155  tx1cn  19157  tx2cn  19158  ptcld  19161  xkoccn  19167  txcnp  19168  ptcnp  19170  txcnmpt  19172  ptcn  19175  txdis1cn  19183  ptrescn  19187  txkgen  19200  xkoco1cn  19205  xkoco2cn  19206  xkococn  19208  xkoinjcn  19235  qtoptop2  19247  qtopuni  19250  qtopid  19253  qtopkgen  19258  basqtop  19259  tgqtop  19260  qtopss  19263  qtopeu  19264  qtoprest  19265  kqopn  19282  kqcld  19283  kqreglem2  19290  reghmph  19341  ordthmeolem  19349  qtopf1  19364  opnfbas  19390  isfil2  19404  fbasweak  19413  fsubbas  19415  filcon  19431  fbasrn  19432  rnelfmlem  19500  flimss2  19520  flimss1  19521  hausflim  19529  flimclslem  19532  flimsncls  19534  cnpflfi  19547  flfcnp2  19555  fclsfnflim  19575  cnextfvval  19612  cnextfres  19615  symgtgp  19647  opnsubg  19653  ghmcnp  19660  divstgpopn  19665  divstgplem  19666  divstgphaus  19668  tsmsfbas  19673  ustfilxp  19762  utoptop  19784  utopbas  19785  restutopopn  19788  iducn  19833  cstucnd  19834  ucncn  19835  fmucnd  19842  cfilufg  19843  trcfilu  19844  cfiluweak  19845  neipcfilu  19846  psmetsym  19861  isxmetd  19876  xmetsym  19897  imasdsf1olem  19923  imasf1oxmet  19925  xblss2ps  19951  xblss2  19952  xblcntrps  19960  xblcntr  19961  blcld  20055  metustfbasOLD  20115  metustfbas  20116  cfilucfilOLD  20119  cfilucfil  20120  restmetu  20137  ngptgp  20197  tngngpd  20214  tngnrg  20230  nlmvscn  20243  nrginvrcn  20247  nmo0  20289  nmoeq0  20290  nmoid  20296  nghmcn  20299  0nmhm  20309  blcvx  20350  zcld  20365  iccntr  20373  xrge0tsms  20386  xmetdcn2  20389  metdstri  20402  metdscn  20407  rescncf  20448  cncfco  20458  oprpiece1res2  20499  cnheibor  20502  cnllycmp  20503  bndth  20505  evth  20506  ishtpyd  20522  isphtpyd  20533  pcoval2  20563  nmhmcn  20650  ipcn  20733  lmnn  20749  cfilss  20756  iscfil3  20759  cfilfcls  20760  cmetcaulem  20774  iscmet3lem2  20778  cfilres  20782  lmcau  20798  flimcfil  20799  cncmet  20808  rlmbn  20848  minveclem3b  20890  pjthlem1  20899  pjth2  20902  ivthlem3  20912  ovolssnul  20945  ovolctb  20948  ovolunnul  20958  ovoliunnul  20965  ovolsca  20973  ovolicc  20981  ovolicopnf  20982  voliunlem2  21007  voliunlem3  21008  volsup  21012  uniioovol  21034  uniiccvol  21035  dyadmaxlem  21052  vitalilem5  21067  ismbfd  21093  mbfres  21097  mbfss  21099  mbfmulc2re  21101  mbfadd  21114  mbfmulc2  21116  mbflimsup  21119  mbflim  21121  i1faddlem  21146  i1fmullem  21147  mbfmul  21179  itg2itg1  21189  itg2seq  21195  itg2eqa  21198  itg2mulc  21200  itg2split  21202  itg2mono  21206  itg2cnlem1  21214  ibl0  21239  iblposlem  21244  itgreval  21249  iblneg  21255  iblss  21257  iblss2  21258  itgle  21262  iblconst  21270  iblabs  21281  iblabsr  21282  iblmulc2  21283  bddmulibl  21291  limciun  21344  limcun  21345  dvres2lem  21360  dvidlem  21365  dvcnp2  21369  dvcn  21370  cpnres  21386  dvaddbr  21387  dvmulbr  21388  dvcobr  21395  dvcjbr  21398  dvrec  21404  dvcnvlem  21423  dvferm  21435  dvlip2  21442  dveq0  21447  dv11cn  21448  dvivthlem1  21455  lhop1  21461  lhop2  21462  lhop  21463  dvcnvre  21466  dvfsumlem3  21475  dvfsumlem4  21476  dvfsumrlim  21478  dvfsum2  21481  ftc1a  21484  ftc1lem4  21486  ftc1lem6  21488  ftc1  21489  coe1mul3  21546  deg1addle2  21549  deg1add  21550  deg1sublt  21557  deg1mul2  21561  deg1tm  21565  fta1blem  21615  drnguc1p  21617  ig1prsp  21624  plyco0  21635  plyeq0lem  21653  dgrub  21677  dgreq  21687  dgradd2  21710  dgrmul  21712  dgrcolem2  21716  dgrco  21717  plycpn  21730  plydivlem4  21737  plydiveu  21739  vieta1lem2  21752  vieta1  21753  aalioulem2  21774  aalioulem3  21775  aaliou3lem7  21790  tayl0  21802  ulmcn  21839  ulmdvlem3  21842  psercn  21866  abelth  21881  pilem3  21893  efif1olem1  21973  abslogimle  22000  argregt0  22034  argrege0  22035  logf1o2  22070  cxpsqrlem  22122  cxpcn3  22161  abscxpbnd  22166  ang180lem2  22181  ang180lem3  22182  logreclem  22189  xrlimcnp  22337  harmonicbnd4  22379  fsumharmonic  22380  basellem3  22395  basellem4  22396  dvdsppwf1o  22501  dvdsflf1o  22502  fsumfldivdiaglem  22504  chpeq0  22522  chteq0  22523  chtub  22526  chpub  22534  dchrelbasd  22553  dchrmulcl  22563  dchrinv  22575  bcmono  22591  bposlem1  22598  bposlem2  22599  lgslem1  22610  lgsdirprm  22643  lgsqrlem2  22656  lgsqrlem3  22657  lgsdchr  22662  lgseisenlem1  22663  lgseisenlem2  22664  lgseisenlem3  22665  lgsquadlem1  22668  2sqlem8  22686  2sqblem  22691  chebbnd1lem1  22693  dchrisumlem1  22713  dchrisumlem2  22714  dchrisumlem3  22715  dchrisum0fno1  22735  pntrmax  22788  pntpbnd1a  22809  pntibndlem3  22816  pntlemn  22824  pntlemi  22828  pntlem3  22833  pntleml  22835  ostth1  22857  ostth2  22861  ostth3  22862  ttgcontlem1  23082  brbtwn2  23102  axlowdimlem3  23141  axlowdimlem16  23154  axcontlem8  23168  cusgra0v  23319  cusgraexi  23327  cusgrares  23331  1pthon  23441  constr2spth  23450  2pthon  23452  constr3trllem3  23489  constr3cycl  23498  eupares  23547  eupap1  23548  nvabs  24012  vacn  24040  nmcvcn  24041  nmblore  24137  0lno  24141  0blo  24143  nmlno0lem  24144  occl  24658  pjhthlem1  24745  pjpjpre  24773  nmopre  25225  nmlnop0iALT  25350  nmophmi  25386  leoprf2  25482  stlesi  25596  disjdifprg  25870  fpwrelmap  25984  xrge0tsmsd  26204  ornglmullt  26226  orngrmullt  26227  ofldlt1  26232  isarchiofld  26236  kerf1hrm  26243  metider  26273  qqhval2lem  26362  qqhcn  26372  pwsiga  26525  prsiga  26526  measle0  26574  mbfmcst  26626  1stmbfm  26627  2ndmbfm  26628  imambfm  26629  cnmbfm  26630  mbfmco  26631  mbfmco2  26632  oddpwdc  26689  eulerpartlemgs2  26715  0rrv  26786  ballotlemfc0  26827  ballotlemfcc  26828  lgamgulmlem5  26971  lgambdd  26975  derangen  27012  subfacval3  27029  cvmseu  27117  cvmliftmolem2  27123  cvmliftlem7  27132  cvmliftlem15  27139  cvmlift2lem9a  27144  cvmlift2lem9  27152  cvmlift2lem10  27153  cvmlift2lem11  27154  cvmlift2lem12  27155  cvmlift3lem6  27165  cvmlift3lem8  27167  wsuclem  27713  supaddc  28370  supadd  28371  mblfinlem2  28382  ovoliunnfl  28386  volsupnfl  28389  mbfresfi  28391  dvtanlem  28394  itg2addnclem2  28397  iblabsnc  28409  iblmulc2nc  28410  ftc1cnnclem  28418  ftc1cnnc  28419  ftc1anc  28428  fness  28507  ssref  28508  fnetr  28511  reftr  28514  fnessref  28518  refssfne  28519  neibastop1  28533  neibastop2  28535  tailfb  28551  filnetlem3  28554  fzadd2  28590  sdclem2  28591  metf1o  28604  ismtyhmeolem  28656  ismtyres  28660  heibor1lem  28661  bfplem2  28675  bfp  28676  rrncmslem  28684  iccbnd  28692  icccmpALT  28693  rngogrphom  28730  rngoisoco  28741  keridl  28785  fzsplit1nn0  29045  icodiamlt  29114  irrapxlem3  29118  irrapxlem4  29119  pell1234qrdich  29155  pell1qr1  29165  pell14qrgap  29169  pellqrexplicit  29171  rmspecfund  29203  fzmaxdif  29277  acongeq  29279  jm2.23  29298  jm3.1  29322  lmhmlnmsplit  29393  hbt  29439  dgrsub2  29444  proot1ex  29522  dvconstbi  29561  ubelsupr  29695  fmul01  29714  fmuldfeq  29717  climsuse  29734  stoweidlem7  29755  stoweidlem13  29761  stoweidlem26  29774  wallispilem3  29815  stirlinglem6  29827  stirlinglem10  29831  wwlktovf1  30205  uvtxnb  30231  usgra2wlkspth  30251  wlklniswwlkn1  30286  vfwlkniswwlkn  30293  usg2wlkeq2  30294  wwlknred  30308  wwlknredwwlkn0  30312  clwwlkel  30408  wwlkext2clwwlk  30418  clwwnisshclwwn  30426  clwlkf1clwwlk  30476  0egra0rgra  30502  0vgrargra  30503  frgra0v  30538  frgra1v  30543  fmptsnd  30674  rmfsupp  30738  mndpfsupp  30740  scmfsupp  30742  mptcfsupp  30744  lcoel0  30851  lincsumcl  30854  lincscmcl  30855  lcoss  30859  lindsrng01  30891  lincreslvec3  30905  lindssnlvec  30909  mnd1  30910  bnj1452  31930  bj-finsumval0  32426  lsmcv2  32514  lsatcv0  32516  lcvexchlem4  32522  lcvexchlem5  32523  l1cvpat  32539  lfl0f  32554  lfladdcl  32556  lflnegcl  32560  lkrlss  32580  eqlkr  32584  lkrlsp  32587  lkrlsp2  32588  lshpkrcl  32601  lkrin  32649  1cvrjat  32959  llni  32992  llnle  33002  lplni  33016  lplnle  33024  llncvrlpln2  33041  2atmat  33045  lvoli  33059  lplncvrlvol2  33099  elpaddri  33286  paddclN  33326  pclclN  33375  pclfinN  33384  0psubclN  33427  1psubclN  33428  atpsubclN  33429  pmapsubclN  33430  osumclN  33451  pexmidN  33453  pexmidlem6N  33459  lhp2lt  33485  lautcnv  33574  idlaut  33580  lautco  33581  idldil  33598  ldilcnv  33599  ldilco  33600  ltrncnv  33630  idltrn  33634  cdleme16d  33765  cdleme50laut  34031  cdleme50ldil  34032  cdleme50ltrn  34041  ltrnco  34203  dian0  34524  dia0eldmN  34525  dia1eldmN  34526  dialss  34531  diaintclN  34543  docaclN  34609  doca2N  34611  djajN  34622  dibintclN  34652  diblss  34655  dicvaddcl  34675  dicvscacl  34676  dicn0  34677  cdlemn11a  34692  dihord2cN  34706  dihord11b  34707  dihord6apre  34741  dihmeetlem1N  34775  dihglblem5apreN  34776  dihpN  34821  dihjatcclem4  34906  dochkr1  34963  islpoldN  34969  lcfrlem31  35058  mapdpglem18  35174  mapdheq2  35214  mapdheq4  35217  mapdh6aN  35220  hdmap1l6a  35295  hdmap1neglem1N  35313  hdmap14lem4a  35359
  Copyright terms: Public domain W3C validator