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  5999  fnprb  6035  fnprOLD  6036  fdmfifsupp  7731  fczfsuppd  7739  fsuppmptif  7750  fsuppco2  7753  fsuppcor  7754  dffi3  7782  supmax  7816  suppr  7819  ordtypelem7  7839  cantnf0  7984  cantnfp1lem1  7987  cantnfp1lem2  7988  cantnfp1lem3  7989  cantnflem1a  7994  cantnflem1d  7997  cantnflem1  7998  cantnf  8002  cantnfleOLD  8010  cantnfp1lem1OLD  8013  cantnfp1lem2OLD  8014  cantnfp1lem3OLD  8015  cantnflem1aOLD  8017  cantnflem1cOLD  8019  cantnflem1dOLD  8020  cantnflem1OLD  8021  cantnfOLD  8024  mapfienOLD  8028  rankpwi  8131  carduni  8252  fin23lem32  8614  fpwwe2lem6  8903  fpwwe2lem9  8906  fpwwe2lem12  8909  fpwwe2lem13  8910  fpwwe2  8911  inttsk  9042  grutsk1  9089  add20  9952  supmul  10399  suprzcl  10822  uzwo3  11049  rpnnen1lem5  11084  xrre  11242  xrre3  11244  xleadd1a  11317  xlemul1a  11352  supxrre  11391  infmxrre  11399  ixxub  11422  ixxlb  11423  elioc2  11459  elico2  11460  elicc2  11461  elfz1eq  11563  fznatpl1  11611  nn0fz0  11626  fzctr  11630  fzo1fzo0n0  11689  fzoaddel  11698  flid  11758  flval3  11764  fladdz  11771  fldiv  11800  modid  11833  seqf1olem1  11946  bcval5  12195  hashf1lem1  12310  sqeqd  12757  sqrlem7  12840  max0add  12901  abs2difabs  12924  rddif  12930  fzomaxdiflem  12932  rexico  12943  limsupgre  13061  rlim3  13078  icco1  13120  rlimclim  13126  rlimuni  13130  rlimresb  13145  isercolllem2  13245  isercolllem3  13246  isercoll  13247  caucvgrlem  13252  caurcvgr  13253  iseraltlem3  13263  fsum00  13363  o1fsum  13378  dvdseq  13682  bitsfzolem  13732  bitsfzo  13733  bitsmod  13734  bitscmp  13736  gcd0id  13809  gcdneg  13812  bezoutlem4  13827  nn0seqcvgd  13847  prmind2  13876  qredeq  13894  isprm5  13900  hashdvds  13952  eulerthlem2  13959  pcpremul  14012  pcidlem  14040  pcgcd1  14045  pcadd2  14054  fldivp1  14061  pcfaclem  14062  prmreclem5  14083  4sqlem17  14124  vdwlem1  14144  vdwlem6  14149  vdwlem12  14155  vdwlem13  14156  0ram  14183  ram0  14185  ramub1lem1  14189  invco  14811  sectmon  14818  monsect  14819  ssctr  14840  ssceq  14841  issubc3  14861  fullsubc  14862  funcinv  14885  fthmon  14939  fuccocl  14976  fucidcl  14977  invfuc  14986  elhomai  15003  setcmon  15057  setcepi  15058  catcisolem  15076  curf2cl  15143  yonedalem4c  15189  yonedalem3  15192  yoniso  15197  lublecl  15261  isacs3lem  15438  tsrdir  15510  nmznsg  15827  ghmpreima  15870  ghmeql  15871  ghmnsgpreima  15873  cntzsubm  15955  cntzsubg  15956  cntzmhm  15958  symgextfo  16029  symgfixf1  16045  symgfixfolem1  16046  odlem2  16146  gexlem2  16185  gexcl2  16192  sylow1lem5  16205  subgslw  16219  slwhash  16227  fislw  16228  sylow3lem1  16230  lsmsubg  16257  efgredlemd  16345  efgredlem  16348  efgcpbllemb  16356  frgpuplem  16373  cyggeninv  16464  iscygd  16468  iscygodd  16469  gsumzadd  16513  gsumconst  16532  gsumpt  16559  gsumptOLD  16560  gsum2dlem2  16567  gsum2d  16568  gsum2d2lem  16570  dprdfcntz  16604  dprdfcntzOLD  16610  eldprdi  16613  eldprdiOLD  16620  subgdmdprd  16636  subgdprd  16637  dprdpr  16654  ablfac1c  16677  ablfac1eu  16679  ablfaclem3  16693  kerf1hrm  16937  issubdrg  16996  rhmeql  17001  rhmima  17002  cntzsubr  17003  isabvd  17011  abvdiv  17028  lsslsp  17202  lmhmima  17234  lmhmpreima  17235  lmhmeql  17242  lsmcl  17270  lspfixed  17315  issubassa  17501  issubassa2  17521  snifpsrbag  17539  psrbaglesupp  17541  psrbaglesuppOLD  17542  psrbaglecl  17543  psrbagaddcl  17544  psrbagaddclOLD  17545  psrbagcon  17546  psrbasOLD  17555  psrlidmOLD  17581  psrridmOLD  17583  mvridlemOLD  17599  mplsubglem  17617  mpllsslem  17618  mplsubglemOLD  17619  mpllsslemOLD  17620  mplassa  17640  subrgmpl  17646  mplcoe3OLD  17653  mplcoe5  17655  mplcoe2OLD  17657  mplbas2  17658  mplbas2OLD  17659  mplind  17691  evlslem3  17707  mpfind  17729  ply1assa  17762  coe1tmmul2  17837  coe1tmmul  17838  qsssubdrg  17981  gzrngunit  17987  evpmodpmf1o  18135  ocvpj  18251  dsmm0cl  18274  dsmmacl  18275  dsmmsubg  18277  dsmmlss  18278  frlmsplit2  18306  uvcff  18325  lindfrn  18359  f1lindf  18360  lindsss  18362  mdet0pr  18514  distop  18716  indistopon  18721  ppttop  18727  epttop  18729  mretopd  18812  toponmre  18813  neiss  18829  opnneissb  18834  ssnei2  18836  innei  18845  neiptoptop  18851  ordtcld1  18917  ordtcld2  18918  lmconst  18981  cnpnei  18984  iscncl  18989  cnss1  18996  cnss2  18997  cncnpi  18998  cncnp  19000  cnconst2  19003  cnrest  19005  cnpresti  19008  cnpdis  19013  paste  19014  lmcnp  19024  cnhaus  19074  hauscmp  19126  2ndcomap  19178  1stcelcls  19181  1stccnp  19182  llyrest  19205  nllyrest  19206  llyidm  19208  nllyidm  19209  kgentopon  19227  kgenidm  19236  kgencn3  19247  txcld  19292  neitx  19296  tx1cn  19298  tx2cn  19299  ptcld  19302  xkoccn  19308  txcnp  19309  ptcnp  19311  txcnmpt  19313  ptcn  19316  txdis1cn  19324  ptrescn  19328  txkgen  19341  xkoco1cn  19346  xkoco2cn  19347  xkococn  19349  xkoinjcn  19376  qtoptop2  19388  qtopuni  19391  qtopid  19394  qtopkgen  19399  basqtop  19400  tgqtop  19401  qtopss  19404  qtopeu  19405  qtoprest  19406  kqopn  19423  kqcld  19424  kqreglem2  19431  reghmph  19482  ordthmeolem  19490  qtopf1  19505  opnfbas  19531  isfil2  19545  fbasweak  19554  fsubbas  19556  filcon  19572  fbasrn  19573  rnelfmlem  19641  flimss2  19661  flimss1  19662  hausflim  19670  flimclslem  19673  flimsncls  19675  cnpflfi  19688  flfcnp2  19696  fclsfnflim  19716  cnextfvval  19753  cnextfres  19756  symgtgp  19788  opnsubg  19794  ghmcnp  19801  divstgpopn  19806  divstgplem  19807  divstgphaus  19809  tsmsfbas  19814  ustfilxp  19903  utoptop  19925  utopbas  19926  restutopopn  19929  iducn  19974  cstucnd  19975  ucncn  19976  fmucnd  19983  cfilufg  19984  trcfilu  19985  cfiluweak  19986  neipcfilu  19987  psmetsym  20002  isxmetd  20017  xmetsym  20038  imasdsf1olem  20064  imasf1oxmet  20066  xblss2ps  20092  xblss2  20093  xblcntrps  20101  xblcntr  20102  blcld  20196  metustfbasOLD  20256  metustfbas  20257  cfilucfilOLD  20260  cfilucfil  20261  restmetu  20278  ngptgp  20338  tngngpd  20355  tngnrg  20371  nlmvscn  20384  nrginvrcn  20388  nmo0  20430  nmoeq0  20431  nmoid  20437  nghmcn  20440  0nmhm  20450  blcvx  20491  zcld  20506  iccntr  20514  xrge0tsms  20527  xmetdcn2  20530  metdstri  20543  metdscn  20548  rescncf  20589  cncfco  20599  oprpiece1res2  20640  cnheibor  20643  cnllycmp  20644  bndth  20646  evth  20647  ishtpyd  20663  isphtpyd  20674  pcoval2  20704  nmhmcn  20791  ipcn  20874  lmnn  20890  cfilss  20897  iscfil3  20900  cfilfcls  20901  cmetcaulem  20915  iscmet3lem2  20919  cfilres  20923  lmcau  20939  flimcfil  20940  cncmet  20949  rlmbn  20989  minveclem3b  21031  pjthlem1  21040  pjth2  21043  ivthlem3  21053  ovolssnul  21086  ovolctb  21089  ovolunnul  21099  ovoliunnul  21106  ovolsca  21114  ovolicc  21122  ovolicopnf  21123  voliunlem2  21148  voliunlem3  21149  volsup  21153  uniioovol  21175  uniiccvol  21176  dyadmaxlem  21193  vitalilem5  21208  ismbfd  21234  mbfres  21238  mbfss  21240  mbfmulc2re  21242  mbfadd  21255  mbfmulc2  21257  mbflimsup  21260  mbflim  21262  i1faddlem  21287  i1fmullem  21288  mbfmul  21320  itg2itg1  21330  itg2seq  21336  itg2eqa  21339  itg2mulc  21341  itg2split  21343  itg2mono  21347  itg2cnlem1  21355  ibl0  21380  iblposlem  21385  itgreval  21390  iblneg  21396  iblss  21398  iblss2  21399  itgle  21403  iblconst  21411  iblabs  21422  iblabsr  21423  iblmulc2  21424  bddmulibl  21432  limciun  21485  limcun  21486  dvres2lem  21501  dvidlem  21506  dvcnp2  21510  dvcn  21511  cpnres  21527  dvaddbr  21528  dvmulbr  21529  dvcobr  21536  dvcjbr  21539  dvrec  21545  dvcnvlem  21564  dvferm  21576  dvlip2  21583  dveq0  21588  dv11cn  21589  dvivthlem1  21596  lhop1  21602  lhop2  21603  lhop  21604  dvcnvre  21607  dvfsumlem3  21616  dvfsumlem4  21617  dvfsumrlim  21619  dvfsum2  21622  ftc1a  21625  ftc1lem4  21627  ftc1lem6  21629  ftc1  21630  coe1mul3  21687  deg1addle2  21690  deg1add  21691  deg1sublt  21698  deg1mul2  21702  deg1tm  21706  fta1blem  21756  drnguc1p  21758  ig1prsp  21765  plyco0  21776  plyeq0lem  21794  dgrub  21818  dgreq  21828  dgradd2  21851  dgrmul  21853  dgrcolem2  21857  dgrco  21858  plycpn  21871  plydivlem4  21878  plydiveu  21880  vieta1lem2  21893  vieta1  21894  aalioulem2  21915  aalioulem3  21916  aaliou3lem7  21931  tayl0  21943  ulmcn  21980  ulmdvlem3  21983  psercn  22007  abelth  22022  pilem3  22034  efif1olem1  22114  abslogimle  22141  argregt0  22175  argrege0  22176  logf1o2  22211  cxpsqrlem  22263  cxpcn3  22302  abscxpbnd  22307  ang180lem2  22322  ang180lem3  22323  logreclem  22330  xrlimcnp  22478  harmonicbnd4  22520  fsumharmonic  22521  basellem3  22536  basellem4  22537  dvdsppwf1o  22642  dvdsflf1o  22643  fsumfldivdiaglem  22645  chpeq0  22663  chteq0  22664  chtub  22667  chpub  22675  dchrelbasd  22694  dchrmulcl  22704  dchrinv  22716  bcmono  22732  bposlem1  22739  bposlem2  22740  lgslem1  22751  lgsdirprm  22784  lgsqrlem2  22797  lgsqrlem3  22798  lgsdchr  22803  lgseisenlem1  22804  lgseisenlem2  22805  lgseisenlem3  22806  lgsquadlem1  22809  2sqlem8  22827  2sqblem  22832  chebbnd1lem1  22834  dchrisumlem1  22854  dchrisumlem2  22855  dchrisumlem3  22856  dchrisum0fno1  22876  pntrmax  22929  pntpbnd1a  22950  pntibndlem3  22957  pntlemn  22965  pntlemi  22969  pntlem3  22974  pntleml  22976  ostth1  22998  ostth2  23002  ostth3  23003  ttgcontlem1  23266  brbtwn2  23286  axlowdimlem3  23325  axlowdimlem16  23338  axcontlem8  23352  cusgra0v  23503  cusgraexi  23511  cusgrares  23515  1pthon  23625  constr2spth  23634  2pthon  23636  constr3trllem3  23673  constr3cycl  23682  eupares  23731  eupap1  23732  nvabs  24196  vacn  24224  nmcvcn  24225  nmblore  24321  0lno  24325  0blo  24327  nmlno0lem  24328  occl  24842  pjhthlem1  24929  pjpjpre  24957  nmopre  25409  nmlnop0iALT  25534  nmophmi  25570  leoprf2  25666  stlesi  25780  disjdifprg  26053  fpwrelmap  26167  xrge0tsmsd  26387  ornglmullt  26409  orngrmullt  26410  ofldlt1  26415  isarchiofld  26419  metider  26455  qqhval2lem  26544  qqhcn  26554  pwsiga  26707  prsiga  26708  measle0  26756  mbfmcst  26808  1stmbfm  26809  2ndmbfm  26810  imambfm  26811  cnmbfm  26812  mbfmco  26813  mbfmco2  26814  oddpwdc  26871  eulerpartlemgs2  26897  0rrv  26968  ballotlemfc0  27009  ballotlemfcc  27010  lgamgulmlem5  27153  lgambdd  27157  derangen  27194  subfacval3  27211  cvmseu  27299  cvmliftmolem2  27305  cvmliftlem7  27314  cvmliftlem15  27321  cvmlift2lem9a  27326  cvmlift2lem9  27334  cvmlift2lem10  27335  cvmlift2lem11  27336  cvmlift2lem12  27337  cvmlift3lem6  27347  cvmlift3lem8  27349  wsuclem  27896  supaddc  28555  supadd  28556  mblfinlem2  28567  ovoliunnfl  28571  volsupnfl  28574  mbfresfi  28576  dvtanlem  28579  itg2addnclem2  28582  iblabsnc  28594  iblmulc2nc  28595  ftc1cnnclem  28603  ftc1cnnc  28604  ftc1anc  28613  fness  28692  ssref  28693  fnetr  28696  reftr  28699  fnessref  28703  refssfne  28704  neibastop1  28718  neibastop2  28720  tailfb  28736  filnetlem3  28739  fzadd2  28775  sdclem2  28776  metf1o  28789  ismtyhmeolem  28841  ismtyres  28845  heibor1lem  28846  bfplem2  28860  bfp  28861  rrncmslem  28869  iccbnd  28877  icccmpALT  28878  rngogrphom  28915  rngoisoco  28926  keridl  28970  fzsplit1nn0  29230  icodiamlt  29299  irrapxlem3  29303  irrapxlem4  29304  pell1234qrdich  29340  pell1qr1  29350  pell14qrgap  29354  pellqrexplicit  29356  rmspecfund  29388  fzmaxdif  29462  acongeq  29464  jm2.23  29483  jm3.1  29507  lmhmlnmsplit  29578  hbt  29624  dgrsub2  29629  proot1ex  29707  dvconstbi  29746  ubelsupr  29880  fmul01  29899  fmuldfeq  29902  climsuse  29919  stoweidlem7  29940  stoweidlem13  29946  stoweidlem26  29959  wallispilem3  30000  stirlinglem6  30012  stirlinglem10  30016  wwlktovf1  30390  uvtxnb  30416  usgra2wlkspth  30436  wlklniswwlkn1  30471  vfwlkniswwlkn  30478  usg2wlkeq2  30479  wwlknred  30493  wwlknredwwlkn0  30497  clwwlkel  30593  wwlkext2clwwlk  30603  clwwnisshclwwn  30611  clwlkf1clwwlk  30661  0egra0rgra  30687  0vgrargra  30688  frgra0v  30723  frgra1v  30728  fmptsnd  30860  rmfsupp  30926  mndpfsupp  30928  scmfsupp  30930  mptcfsupp  30932  lcoel0  31069  lincsumcl  31072  lincscmcl  31073  lcoss  31077  lindsrng01  31109  lincreslvec3  31123  lindssnlvec  31127  mnd1  31128  m2cpmrngiso  31217  pmattomply1rngiso  31277  fvmptnn04if  31303  bnj1452  32343  bj-finsumval0  32889  lsmcv2  32980  lsatcv0  32982  lcvexchlem4  32988  lcvexchlem5  32989  l1cvpat  33005  lfl0f  33020  lfladdcl  33022  lflnegcl  33026  lkrlss  33046  eqlkr  33050  lkrlsp  33053  lkrlsp2  33054  lshpkrcl  33067  lkrin  33115  1cvrjat  33425  llni  33458  llnle  33468  lplni  33482  lplnle  33490  llncvrlpln2  33507  2atmat  33511  lvoli  33525  lplncvrlvol2  33565  elpaddri  33752  paddclN  33792  pclclN  33841  pclfinN  33850  0psubclN  33893  1psubclN  33894  atpsubclN  33895  pmapsubclN  33896  osumclN  33917  pexmidN  33919  pexmidlem6N  33925  lhp2lt  33951  lautcnv  34040  idlaut  34046  lautco  34047  idldil  34064  ldilcnv  34065  ldilco  34066  ltrncnv  34096  idltrn  34100  cdleme16d  34231  cdleme50laut  34497  cdleme50ldil  34498  cdleme50ltrn  34507  ltrnco  34669  dian0  34990  dia0eldmN  34991  dia1eldmN  34992  dialss  34997  diaintclN  35009  docaclN  35075  doca2N  35077  djajN  35088  dibintclN  35118  diblss  35121  dicvaddcl  35141  dicvscacl  35142  dicn0  35143  cdlemn11a  35158  dihord2cN  35172  dihord11b  35173  dihord6apre  35207  dihmeetlem1N  35241  dihglblem5apreN  35242  dihpN  35287  dihjatcclem4  35372  dochkr1  35429  islpoldN  35435  lcfrlem31  35524  mapdpglem18  35640  mapdheq2  35680  mapdheq4  35683  mapdh6aN  35686  hdmap1l6a  35761  hdmap1neglem1N  35779  hdmap14lem4a  35825
  Copyright terms: Public domain W3C validator