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

Theorem mpbir2and 922
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:  fveqressseq  6012  fmptsng  6077  fmptsnd  6078  fnprb  6114  fnprOLD  6115  fdmfifsupp  7841  fczfsuppd  7849  fsuppmptif  7861  fsuppco2  7864  fsuppcor  7865  dffi3  7893  supmaxOLD  7928  suppr  7932  ordtypelem7  7952  cantnf0  8097  cantnfp1lem1  8100  cantnfp1lem2  8101  cantnfp1lem3  8102  cantnflem1a  8107  cantnflem1d  8110  cantnflem1  8111  cantnf  8115  cantnfleOLD  8123  cantnfp1lem1OLD  8126  cantnfp1lem2OLD  8127  cantnfp1lem3OLD  8128  cantnflem1aOLD  8130  cantnflem1cOLD  8132  cantnflem1dOLD  8133  cantnflem1OLD  8134  cantnfOLD  8137  mapfienOLD  8141  rankpwi  8244  carduni  8365  fin23lem32  8727  fpwwe2lem6  9016  fpwwe2lem9  9019  fpwwe2lem12  9022  fpwwe2lem13  9023  fpwwe2  9024  inttsk  9155  grutsk1  9202  add20  10071  supmul  10518  suprzcl  10949  uzwo3  11188  rpnnen1lem5  11223  xrre  11381  xrre3  11383  xleadd1a  11456  xlemul1a  11491  supxrre  11530  infmxrre  11538  ixxub  11561  ixxlb  11562  elioc2  11598  elico2  11599  elicc2  11600  elfz1eq  11708  fznatpl1  11745  nn0fz0  11785  fzctr  11798  fzo1fzo0n0  11846  fzoaddel  11855  flid  11927  flval3  11933  fladdz  11940  fldiv  11969  modid  12002  seqf1olem1  12128  bcval5  12378  hashf1lem1  12486  ccat2s1fvw  12624  wwlktovf1  12877  sqeqd  12981  sqrlem7  13064  max0add  13125  abs2difabs  13149  rddif  13155  fzomaxdiflem  13157  rexico  13168  limsupgre  13286  rlim3  13303  icco1  13345  rlimclim  13351  rlimuni  13355  rlimresb  13370  isercolllem2  13470  isercolllem3  13471  isercoll  13472  caucvgrlem  13477  caurcvgr  13478  iseraltlem3  13488  fsum00  13594  o1fsum  13609  dvdseq  14015  bitsfzolem  14066  bitsfzo  14067  bitsmod  14068  bitscmp  14070  gcd0id  14143  gcdneg  14146  bezoutlem4  14161  nn0seqcvgd  14181  prmind2  14210  qredeq  14229  isprm5  14235  hashdvds  14287  eulerthlem2  14294  pcpremul  14349  pcidlem  14377  pcgcd1  14382  pcadd2  14391  fldivp1  14398  pcfaclem  14399  prmreclem5  14420  4sqlem17  14461  vdwlem1  14481  vdwlem6  14486  vdwlem12  14492  vdwlem13  14493  0ram  14520  ram0  14522  ramub1lem1  14526  invco  15147  sectmon  15154  monsect  15155  ssctr  15176  ssceq  15177  issubc3  15197  fullsubc  15198  funcinv  15221  fthmon  15275  fuccocl  15312  fucidcl  15313  invfuc  15322  elhomai  15339  setcmon  15393  setcepi  15394  catcisolem  15412  curf2cl  15479  yonedalem4c  15525  yonedalem3  15528  yoniso  15533  lublecl  15598  isacs3lem  15775  tsrdir  15847  mnd1  15940  mnd1OLD  15941  sgrp2nmndlem4  16025  sgrp2nmndlem5  16026  nmznsg  16224  ghmpreima  16267  ghmeql  16268  ghmnsgpreima  16270  cntzsubm  16352  cntzsubg  16353  cntzmhm  16355  symgextfo  16426  symgfixf1  16441  symgfixfolem1  16442  odlem2  16542  gexlem2  16581  gexcl2  16588  sylow1lem5  16601  subgslw  16615  slwhash  16623  fislw  16624  sylow3lem1  16626  lsmsubg  16653  efgredlemd  16741  efgredlem  16744  efgcpbllemb  16752  frgpuplem  16769  cyggeninv  16865  iscygd  16869  iscygodd  16870  gsumzadd  16914  gsumconst  16933  gsumpt  16967  gsumptOLD  16968  gsum2dlem2  16977  gsum2d  16978  gsum2d2lem  16980  dprdfcntz  17028  dprdfcntzOLD  17034  eldprdi  17037  eldprdiOLD  17044  subgdmdprd  17060  subgdprd  17061  dprdpr  17078  ablfac1c  17101  ablfac1eu  17103  ablfaclem3  17117  ring1  17227  kerf1hrm  17371  issubdrg  17433  rhmeql  17438  rhmima  17439  cntzsubr  17440  isabvd  17448  abvdiv  17465  lsslsp  17640  lmhmima  17672  lmhmpreima  17673  lmhmeql  17680  lsmcl  17708  lspfixed  17753  issubassa  17952  issubassa2  17973  snifpsrbag  17994  psrbaglesupp  17996  psrbaglesuppOLD  17997  psrbaglecl  17998  psrbagaddcl  17999  psrbagaddclOLD  18000  psrbagcon  18001  psrbasOLD  18010  psrlidmOLD  18036  psrridmOLD  18038  mvridlemOLD  18054  mplsubglem  18072  mpllsslem  18073  mplsubglemOLD  18074  mpllsslemOLD  18075  mplassa  18095  subrgmpl  18101  mplcoe3OLD  18108  mplcoe5  18110  mplcoe2OLD  18112  mplbas2  18113  mplbas2OLD  18114  mplind  18146  evlslem3  18162  mpfind  18184  ply1assa  18217  coe1tmmul2  18296  coe1tmmul  18297  cply1coe0bi  18321  qsssubdrg  18456  gzrngunit  18462  evpmodpmf1o  18610  ocvpj  18726  dsmm0cl  18749  dsmmacl  18750  dsmmsubg  18752  dsmmlss  18753  frlmsplit2  18781  uvcff  18800  lindfrn  18834  f1lindf  18835  lindsss  18837  mat1rngiso  18966  dmatid  18975  dmatsubcl  18978  dmatscmcl  18983  scmatid  18994  scmataddcl  18996  scmatsubcl  18997  scmatmulcl  18998  smatvscl  19004  scmatrhmcl  19008  scmatrngiso  19016  mat0scmat  19018  mat1scmat  19019  mdet0pr  19072  m2cpmrngiso  19237  pm2mprngiso  19301  chmaidscmat  19327  fvmptnn04if  19328  distop  19475  indistopon  19480  ppttop  19486  epttop  19488  mretopd  19571  toponmre  19572  neiss  19588  opnneissb  19593  ssnei2  19595  innei  19604  neiptoptop  19610  ordtcld1  19676  ordtcld2  19677  lmconst  19740  cnpnei  19743  iscncl  19748  cnss1  19755  cnss2  19756  cncnpi  19757  cncnp  19759  cnconst2  19762  cnrest  19764  cnpresti  19767  cnpdis  19772  paste  19773  lmcnp  19783  cnhaus  19833  hauscmp  19885  2ndcomap  19937  1stcelcls  19940  1stccnp  19941  llyrest  19964  nllyrest  19965  llyidm  19967  nllyidm  19968  ssref  19991  reftr  19993  refun0  19994  dissnref  20007  kgentopon  20017  kgenidm  20026  kgencn3  20037  txcld  20082  neitx  20086  tx1cn  20088  tx2cn  20089  ptcld  20092  xkoccn  20098  txcnp  20099  ptcnp  20101  txcnmpt  20103  ptcn  20106  txdis1cn  20114  ptrescn  20118  txkgen  20131  xkoco1cn  20136  xkoco2cn  20137  xkococn  20139  xkoinjcn  20166  qtoptop2  20178  qtopuni  20181  qtopid  20184  qtopkgen  20189  basqtop  20190  tgqtop  20191  qtopss  20194  qtopeu  20195  qtoprest  20196  kqopn  20213  kqcld  20214  kqreglem2  20221  reghmph  20272  ordthmeolem  20280  qtopf1  20295  opnfbas  20321  isfil2  20335  fbasweak  20344  fsubbas  20346  filcon  20362  fbasrn  20363  rnelfmlem  20431  flimss2  20451  flimss1  20452  hausflim  20460  flimclslem  20463  flimsncls  20465  cnpflfi  20478  flfcnp2  20486  fclsfnflim  20506  cnextfvval  20543  cnextfres  20546  symgtgp  20578  opnsubg  20584  ghmcnp  20591  qustgpopn  20596  qustgplem  20597  qustgphaus  20599  tsmsfbas  20604  ustfilxp  20693  utoptop  20715  utopbas  20716  restutopopn  20719  iducn  20764  cstucnd  20765  ucncn  20766  fmucnd  20773  cfilufg  20774  trcfilu  20775  cfiluweak  20776  neipcfilu  20777  psmetsym  20792  psmetres2  20796  isxmetd  20807  xmetsym  20828  xmetpsmet  20829  imasdsf1olem  20854  imasf1oxmet  20856  xblss2ps  20882  xblss2  20883  xblcntrps  20891  xblcntr  20892  blcld  20986  metustfbasOLD  21046  metustfbas  21047  cfilucfilOLD  21050  cfilucfil  21051  restmetu  21068  ngptgp  21128  tngngpd  21145  tngnrg  21161  nlmvscn  21174  nrginvrcn  21178  nmo0  21220  nmoeq0  21221  nmoid  21227  nghmcn  21230  0nmhm  21240  blcvx  21281  zcld  21296  iccntr  21304  xrge0tsms  21317  xmetdcn2  21320  metdstri  21333  metdscn  21338  rescncf  21379  cncfco  21389  oprpiece1res2  21430  cnheibor  21433  cnllycmp  21434  bndth  21436  evth  21437  ishtpyd  21453  isphtpyd  21464  pcoval2  21494  nmhmcn  21581  ipcn  21664  lmnn  21680  cfilss  21687  iscfil3  21690  cfilfcls  21691  cmetcaulem  21705  iscmet3lem2  21709  cfilres  21713  lmcau  21729  flimcfil  21730  cncmet  21739  rlmbn  21779  minveclem3b  21821  pjthlem1  21830  pjth2  21833  ivthlem3  21843  ovolssnul  21876  ovolctb  21879  ovolunnul  21889  ovoliunnul  21896  ovolsca  21904  ovolicc  21912  ovolicopnf  21913  voliunlem2  21939  voliunlem3  21940  volsup  21944  uniioovol  21966  uniiccvol  21967  dyadmaxlem  21984  vitalilem5  21999  ismbfd  22025  mbfres  22029  mbfss  22031  mbfmulc2re  22033  mbfadd  22046  mbfmulc2  22048  mbflimsup  22051  mbflim  22053  i1faddlem  22078  i1fmullem  22079  mbfmul  22111  itg2itg1  22121  itg2seq  22127  itg2eqa  22130  itg2mulc  22132  itg2split  22134  itg2mono  22138  itg2cnlem1  22146  ibl0  22171  iblposlem  22176  itgreval  22181  iblneg  22187  iblss  22189  iblss2  22190  itgle  22194  iblconst  22202  iblabs  22213  iblabsr  22214  iblmulc2  22215  bddmulibl  22223  limciun  22276  limcun  22277  dvres2lem  22292  dvidlem  22297  dvcnp2  22301  dvcn  22302  cpnres  22318  dvaddbr  22319  dvmulbr  22320  dvcobr  22327  dvcjbr  22330  dvrec  22336  dvcnvlem  22355  dvferm  22367  dvlip2  22374  dveq0  22379  dv11cn  22380  dvivthlem1  22387  lhop1  22393  lhop2  22394  lhop  22395  dvcnvre  22398  dvfsumlem3  22407  dvfsumlem4  22408  dvfsumrlim  22410  dvfsum2  22413  ftc1a  22416  ftc1lem4  22418  ftc1lem6  22420  ftc1  22421  coe1mul3  22478  deg1addle2  22481  deg1add  22482  deg1sublt  22489  deg1mul2  22493  deg1tm  22497  fta1blem  22547  drnguc1p  22549  ig1prsp  22556  plyco0  22567  plyeq0lem  22585  dgrub  22609  dgreq  22619  dgradd2  22643  dgrmul  22645  dgrcolem2  22649  dgrco  22650  plycpn  22663  plydivlem4  22670  plydiveu  22672  vieta1lem2  22685  vieta1  22686  aalioulem2  22707  aalioulem3  22708  aaliou3lem7  22723  tayl0  22735  ulmcn  22772  ulmdvlem3  22775  psercn  22799  abelth  22814  pilem3  22826  efif1olem1  22907  abslogimle  22939  argregt0  22973  argrege0  22974  logf1o2  23009  cxpsqrtlem  23061  cxpcn3  23100  abscxpbnd  23105  ang180lem2  23120  ang180lem3  23121  logreclem  23128  xrlimcnp  23276  harmonicbnd4  23318  fsumharmonic  23319  basellem3  23334  basellem4  23335  dvdsppwf1o  23440  dvdsflf1o  23441  fsumfldivdiaglem  23443  chpeq0  23461  chteq0  23462  chtub  23465  chpub  23473  dchrelbasd  23492  dchrmulcl  23502  dchrinv  23514  bcmono  23530  bposlem1  23537  bposlem2  23538  lgslem1  23549  lgsdirprm  23582  lgsqrlem2  23595  lgsqrlem3  23596  lgsdchr  23601  lgseisenlem1  23602  lgseisenlem2  23603  lgseisenlem3  23604  lgsquadlem1  23607  2sqlem8  23625  2sqblem  23630  chebbnd1lem1  23632  dchrisumlem1  23652  dchrisumlem2  23653  dchrisumlem3  23654  dchrisum0fno1  23674  pntrmax  23727  pntpbnd1a  23748  pntibndlem3  23755  pntlemn  23763  pntlemi  23767  pntlem3  23772  pntleml  23774  ostth1  23796  ostth2  23800  ostth3  23801  ercgrg  23886  motco  23905  cnvmot  23906  legso  23963  mirmot  24033  lmicom  24132  lmimid  24137  lmimot  24141  hypcgrlem1  24142  hypcgrlem2  24143  ttgcontlem1  24166  brbtwn2  24186  axlowdimlem3  24225  axlowdimlem16  24238  axcontlem8  24252  cusgra0v  24438  cusgraexi  24446  cusgrares  24450  uvtxnb  24475  1pthon  24571  constr2spth  24580  2pthon  24582  usgra2wlkspthlem2  24598  usgra2wlkspth  24599  constr3trllem3  24630  constr3cycl  24639  wlklniswwlkn1  24677  vfwlkniswwlkn  24684  usg2wlkeq2  24687  wwlknred  24701  wwlknredwwlkn0  24705  clwlkisclwwlklem2a1  24757  clwwlkel  24771  wwlkext2clwwlk  24781  clwwnisshclwwn  24787  clwlkf1clwwlk  24828  0egra0rgra  24914  0vgrargra  24915  eupares  24953  eupap1  24954  frgra0v  24971  frgra1v  24976  nvabs  25554  vacn  25582  nmcvcn  25583  nmblore  25679  0lno  25683  0blo  25685  nmlno0lem  25686  occl  26200  pjhthlem1  26287  pjpjpre  26315  nmopre  26767  nmlnop0iALT  26892  nmophmi  26928  leoprf2  27024  stlesi  27138  disjdifprg  27414  fpwrelmap  27534  fzspl  27576  2sqmod  27614  ogrpaddlt  27686  ogrpsublt  27690  pnfinf  27705  xrge0tsmsd  27753  ornglmullt  27775  orngrmullt  27776  orngmullt  27777  ofldlt1  27781  isarchiofld  27785  qtopt1  27816  reff  27820  locfinreflem  27821  metideq  27850  metider  27851  pstmxmet  27854  qqhval2lem  27940  qqhcn  27950  qqhucn  27951  pwsiga  28108  prsiga  28109  measle0  28157  mbfmcst  28208  1stmbfm  28209  2ndmbfm  28210  imambfm  28211  cnmbfm  28212  mbfmco  28213  mbfmco2  28214  sibfof  28260  oddpwdc  28271  eulerpartlemmf  28292  eulerpartlemgs2  28297  0rrv  28368  ballotlemfc0  28409  ballotlemfcc  28410  signstfveq0  28512  lgamgulmlem5  28553  lgambdd  28557  derangen  28594  subfacval3  28611  cvmseu  28699  cvmliftmolem2  28705  cvmliftlem7  28714  cvmliftlem15  28721  cvmlift2lem9a  28726  cvmlift2lem9  28734  cvmlift2lem10  28735  cvmlift2lem11  28736  cvmlift2lem12  28737  cvmlift3lem6  28747  cvmlift3lem8  28749  mclsppslem  28921  mclspps  28922  wsuclem  29357  supaddc  30017  supadd  30018  mblfinlem2  30028  ovoliunnfl  30032  volsupnfl  30035  mbfresfi  30037  dvtanlem  30040  itg2addnclem2  30043  iblabsnc  30055  iblmulc2nc  30056  ftc1cnnclem  30064  ftc1cnnc  30065  ftc1anc  30074  fness  30143  fnetr  30145  fnessref  30151  refssfne  30152  neibastop1  30153  neibastop2  30155  tailfb  30171  filnetlem3  30174  fzadd2  30210  sdclem2  30211  metf1o  30224  ismtyhmeolem  30276  ismtyres  30280  heibor1lem  30281  bfplem2  30295  bfp  30296  rrncmslem  30304  iccbnd  30312  icccmpALT  30313  rngogrphom  30350  rngoisoco  30361  keridl  30405  fzsplit1nn0  30663  icodiamlt  30732  irrapxlem3  30736  irrapxlem4  30737  pell1234qrdich  30773  pell1qr1  30783  pell14qrgap  30787  pellqrexplicit  30789  rmspecfund  30821  fzmaxdif  30895  acongeq  30897  jm2.23  30914  jm3.1  30938  lmhmlnmsplit  31009  hbt  31055  dgrsub2  31060  proot1ex  31137  lcmneg  31185  hashnzfz2  31202  dvconstbi  31215  ubelsupr  31349  lefldiveq  31436  iccintsng  31517  fmul01  31528  fmuldfeq  31531  climsuse  31568  mullimc  31576  limcdm0  31578  limccog  31580  mullimcf  31583  constlimc  31584  idlimc  31586  limcperiod  31588  limsupre  31601  limcleqr  31604  neglimc  31607  addlimc  31608  0ellimcdiv  31609  cncfshift  31630  cncfperiod  31635  cncfuni  31643  icccncfext  31644  cncfiooicclem1  31650  fperdvper  31669  ioodvbdlimc1lem2  31683  ioodvbdlimc2lem  31685  mbfres2cn  31711  iblsplit  31719  stoweidlem7  31743  stoweidlem13  31749  stoweidlem26  31762  wallispilem3  31803  stirlinglem6  31815  stirlinglem10  31819  dirkercncf  31843  fourierdlem6  31849  fourierdlem11  31854  fourierdlem12  31855  fourierdlem15  31858  fourierdlem26  31869  fourierdlem42  31885  fourierdlem50  31893  fourierdlem51  31894  fourierdlem52  31895  fourierdlem54  31897  fourierdlem62  31905  fourierdlem79  31922  fourierdlem102  31945  fourierdlem114  31957  rabsubmgmd  32433  submgmid  32435  subsubmgm  32439  mgmhmima  32444  mgmhmeql  32445  isassintop  32487  rnghmsscmap2  32656  rnghmsscmap  32657  rnghmsubcsetc  32660  rhmsscmap2  32699  rhmsscmap  32700  rhmsubcsetc  32703  rhmsscrnghm  32706  rhmsubcrngc  32709  srhmsubc  32752  fldhmsubc  32760  rhmsubc  32766  srhmsubcOLD  32771  fldhmsubcOLD  32779  rhmsubcOLD  32785  rmfsupp  32837  mndpfsupp  32839  scmfsupp  32841  mptcfsupp  32843  lcoel0  32899  lincsumcl  32902  lincscmcl  32903  lcoss  32907  lindsrng01  32939  lincreslvec3  32953  lindssnlvec  32957  bnj1452  33976  bj-finsumval0  34538  lsmcv2  34629  lsatcv0  34631  lcvexchlem4  34637  lcvexchlem5  34638  l1cvpat  34654  lfl0f  34669  lfladdcl  34671  lflnegcl  34675  lkrlss  34695  eqlkr  34699  lkrlsp  34702  lkrlsp2  34703  lshpkrcl  34716  lkrin  34764  1cvrjat  35074  llni  35107  llnle  35117  lplni  35131  lplnle  35139  llncvrlpln2  35156  2atmat  35160  lvoli  35174  lplncvrlvol2  35214  elpaddri  35401  paddclN  35441  pclclN  35490  pclfinN  35499  0psubclN  35542  1psubclN  35543  atpsubclN  35544  pmapsubclN  35545  osumclN  35566  pexmidN  35568  pexmidlem6N  35574  lhp2lt  35600  lautcnv  35689  idlaut  35695  lautco  35696  idldil  35713  ldilcnv  35714  ldilco  35715  ltrncnv  35745  idltrn  35749  cdleme16d  35881  cdleme50laut  36148  cdleme50ldil  36149  cdleme50ltrn  36158  ltrnco  36320  dian0  36641  dia0eldmN  36642  dia1eldmN  36643  dialss  36648  diaintclN  36660  docaclN  36726  doca2N  36728  djajN  36739  dibintclN  36769  diblss  36772  dicvaddcl  36792  dicvscacl  36793  dicn0  36794  cdlemn11a  36809  dihord2cN  36823  dihord11b  36824  dihord6apre  36858  dihmeetlem1N  36892  dihglblem5apreN  36893  dihpN  36938  dihjatcclem4  37023  dochkr1  37080  islpoldN  37086  lcfrlem31  37175  mapdpglem18  37291  mapdheq2  37331  mapdheq4  37334  mapdh6aN  37337  hdmap1l6a  37412  hdmap1neglem1N  37430  hdmap14lem4a  37476
  Copyright terms: Public domain W3C validator