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

Theorem mpbir2and 890
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 520 . 2  |-  ( ph  ->  ( ch  /\  th ) )
4 mpbir2and.3 . 2  |-  ( ph  ->  ( ps  <->  ( ch  /\ 
th ) ) )
53, 4mpbird 225 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360
This theorem is referenced by:  fnpr  5952  fnprOLD  5953  dffi3  7438  supmax  7472  suppr  7475  ordtypelem7  7495  cantnfle  7628  cantnf0  7632  cantnfp1lem1  7636  cantnfp1lem2  7637  cantnfp1lem3  7638  oemapvali  7642  cantnflem1a  7643  cantnflem1c  7645  cantnflem1d  7646  cantnflem1  7647  cantnf  7651  mapfien  7655  rankpwi  7751  carduni  7870  fin23lem32  8226  fpwwe2lem6  8512  fpwwe2lem9  8515  fpwwe2lem12  8518  fpwwe2lem13  8519  fpwwe2  8520  inttsk  8651  grutsk1  8698  add20  9542  supmul  9978  suprzcl  10351  uzwo3  10571  rpnnen1lem5  10606  xrre  10759  xrre3  10761  xleadd1a  10834  xlemul1a  10869  supxrre  10908  infmxrre  10916  ixxub  10939  ixxlb  10940  elioc2  10975  elico2  10976  elicc2  10977  elfz1eq  11070  nn0fz0  11116  fzctr  11119  fzoaddel  11177  flid  11218  flval3  11224  fladdz  11229  fldiv  11243  modid  11272  seqf1olem1  11364  bcval5  11611  hashf1lem1  11706  sqeqd  11973  sqrlem7  12056  max0add  12117  abs2difabs  12140  rddif  12146  fzomaxdiflem  12148  rexico  12159  limsupgre  12277  rlim3  12294  icco1  12336  rlimclim  12342  rlimuni  12346  rlimresb  12361  isercolllem2  12461  isercolllem3  12462  isercoll  12463  caucvgrlem  12468  caurcvgr  12469  iseraltlem3  12479  fsum00  12579  o1fsum  12594  dvdseq  12899  bitsfzolem  12948  bitsfzo  12949  bitsmod  12950  bitscmp  12952  gcd0id  13025  gcdneg  13028  bezoutlem4  13043  nn0seqcvgd  13063  prmind2  13092  qredeq  13108  isprm5  13114  hashdvds  13166  eulerthlem2  13173  pcpremul  13219  pcidlem  13247  pcgcd1  13252  pcadd2  13261  fldivp1  13268  pcfaclem  13269  prmreclem5  13290  4sqlem17  13331  vdwlem1  13351  vdwlem6  13356  vdwlem12  13362  vdwlem13  13363  0ram  13390  ram0  13392  ramub1lem1  13396  invco  13998  sectmon  14005  monsect  14006  ssctr  14027  ssceq  14028  issubc3  14048  fullsubc  14049  funcinv  14072  fthmon  14126  fuccocl  14163  fucidcl  14164  invfuc  14173  elhomai  14190  setcmon  14244  setcepi  14245  catcisolem  14263  curf2cl  14330  yonedalem4c  14376  yonedalem3  14379  yoniso  14384  isacs3lem  14594  tsrdir  14685  nmznsg  14986  ghmpreima  15029  ghmeql  15030  ghmnsgpreima  15032  cntzsubm  15136  cntzsubg  15137  cntzmhm  15139  odlem2  15179  gexlem2  15218  gexcl2  15225  sylow1lem5  15238  subgslw  15252  slwhash  15260  fislw  15261  sylow3lem1  15263  lsmsubg  15290  efgredlemd  15378  efgredlem  15381  efgcpbllemb  15389  frgpuplem  15406  cyggeninv  15495  iscygd  15499  iscygodd  15500  gsumconst  15534  gsumpt  15547  dprdfcntz  15575  eldprdi  15578  subgdmdprd  15594  subgdprd  15595  dprdpr  15610  ablfac1c  15631  ablfac1eu  15633  ablfaclem3  15647  issubdrg  15895  rhmeql  15900  rhmima  15901  cntzsubr  15902  isabvd  15910  abvdiv  15927  lsslsp  16093  lmhmima  16125  lmhmpreima  16126  lmhmeql  16133  lsmcl  16157  lspfixed  16202  issubassa  16385  issubassa2  16405  psrbaglesupp  16435  psrbaglecl  16436  psrbagaddcl  16437  psrbagcon  16438  psrbas  16445  psrlidm  16469  psrridm  16470  mvridlem  16485  mplsubglem  16500  mpllsslem  16501  mplassa  16519  subrgmpl  16525  mplcoe3  16531  mplcoe2  16532  mplbas2  16533  mplind  16564  ply1assa  16599  coe1tmmul2  16670  coe1tmmul  16671  qsssubdrg  16760  gzrngunit  16766  ocvpj  16946  distop  17062  indistopon  17067  ppttop  17073  epttop  17075  mretopd  17158  toponmre  17159  neiss  17175  opnneissb  17180  ssnei2  17182  innei  17191  neiptoptop  17197  ordtcld1  17263  ordtcld2  17264  lmconst  17327  cnpnei  17330  iscncl  17335  cnss1  17342  cnss2  17343  cncnpi  17344  cncnp  17346  cnconst2  17349  cnrest  17351  cnpresti  17354  cnpdis  17359  paste  17360  lmcnp  17370  cnhaus  17420  hauscmp  17472  2ndcomap  17523  1stcelcls  17526  1stccnp  17527  llyrest  17550  nllyrest  17551  llyidm  17553  nllyidm  17554  kgentopon  17572  kgenidm  17581  kgencn3  17592  txcld  17637  neitx  17641  tx1cn  17643  tx2cn  17644  ptcld  17647  xkoccn  17653  txcnp  17654  ptcnp  17656  txcnmpt  17658  ptcn  17661  txdis1cn  17669  ptrescn  17673  txkgen  17686  xkoco1cn  17691  xkoco2cn  17692  xkococn  17694  xkoinjcn  17721  qtoptop2  17733  qtopuni  17736  qtopid  17739  qtopkgen  17744  basqtop  17745  tgqtop  17746  qtopss  17749  qtopeu  17750  qtoprest  17751  kqopn  17768  kqcld  17769  kqreglem2  17776  reghmph  17827  ordthmeolem  17835  qtopf1  17850  opnfbas  17876  isfil2  17890  fbasweak  17899  fsubbas  17901  filcon  17917  fbasrn  17918  rnelfmlem  17986  flimss2  18006  flimss1  18007  hausflim  18015  flimclslem  18018  flimsncls  18020  cnpflfi  18033  flfcnp2  18041  fclsfnflim  18061  cnextfvval  18098  cnextfres  18101  symgtgp  18133  opnsubg  18139  ghmcnp  18146  divstgpopn  18151  divstgplem  18152  divstgphaus  18154  tsmsfbas  18159  ustfilxp  18244  utoptop  18266  utopbas  18267  restutopopn  18270  iducn  18315  cstucnd  18316  ucncn  18317  fmucnd  18324  cfilufg  18325  trcfilu  18326  cfiluweak  18327  neipcfilu  18328  psmetsym  18343  isxmetd  18358  xmetsym  18379  imasdsf1olem  18405  imasf1oxmet  18407  xblss2ps  18433  xblss2  18434  xblcntrps  18442  xblcntr  18443  blcld  18537  metustfbasOLD  18597  metustfbas  18598  cfilucfilOLD  18601  cfilucfil  18602  restmetu  18619  ngptgp  18679  tngngpd  18696  tngnrg  18712  nlmvscn  18725  nrginvrcn  18729  nmo0  18771  nmoeq0  18772  nmoid  18778  nghmcn  18781  0nmhm  18791  blcvx  18831  zcld  18846  iccntr  18854  xrge0tsms  18867  xmetdcn2  18870  metdstri  18883  metdscn  18888  rescncf  18929  cncfco  18939  oprpiece1res2  18979  cnheibor  18982  cnllycmp  18983  bndth  18985  evth  18986  ishtpyd  19002  isphtpyd  19013  pcoval2  19043  nmhmcn  19130  ipcn  19202  lmnn  19218  cfilss  19225  iscfil3  19228  cfilfcls  19229  cmetcaulem  19243  iscmet3lem2  19247  cfilres  19251  lmcau  19267  flimcfil  19268  cncmet  19277  rlmbn  19317  minveclem3b  19331  pjthlem1  19340  pjth2  19343  ivthlem3  19352  ovolssnul  19385  ovolctb  19388  ovolunnul  19398  ovoliunnul  19405  ovolsca  19413  ovolicc  19421  ovolicopnf  19422  voliunlem2  19447  voliunlem3  19448  volsup  19452  uniioovol  19473  uniiccvol  19474  dyadmaxlem  19491  vitalilem5  19506  ismbfd  19534  mbfres  19538  mbfss  19540  mbfmulc2re  19542  mbfadd  19555  mbfmulc2  19557  mbflimsup  19560  mbflim  19562  i1faddlem  19587  i1fmullem  19588  mbfmul  19620  itg2itg1  19630  itg2seq  19636  itg2eqa  19639  itg2mulc  19641  itg2split  19643  itg2mono  19647  itg2cnlem1  19655  ibl0  19680  iblposlem  19685  itgreval  19690  iblneg  19696  iblss  19698  iblss2  19699  itgle  19703  iblconst  19711  iblabs  19722  iblabsr  19723  iblmulc2  19724  bddmulibl  19732  limciun  19783  limcun  19784  dvres2lem  19799  dvidlem  19804  dvcnp2  19808  dvcn  19809  cpnres  19825  dvaddbr  19826  dvmulbr  19827  dvcobr  19834  dvcjbr  19837  dvrec  19843  dvcnvlem  19862  dvferm  19874  dvlip2  19881  dveq0  19886  dv11cn  19887  dvivthlem1  19894  lhop1  19900  lhop2  19901  lhop  19902  dvcnvre  19905  dvfsumlem3  19914  dvfsumlem4  19915  dvfsumrlim  19917  dvfsum2  19920  ftc1a  19923  ftc1lem4  19925  ftc1lem6  19927  ftc1  19928  evlslem3  19937  mpfind  19967  coe1mul3  20024  deg1addle2  20027  deg1add  20028  deg1sublt  20035  deg1mul2  20039  deg1tm  20043  fta1blem  20093  drnguc1p  20095  ig1prsp  20102  plyco0  20113  plyeq0lem  20131  dgrub  20155  dgreq  20165  dgradd2  20188  dgrmul  20190  dgrcolem2  20194  dgrco  20195  plycpn  20208  plydivlem4  20215  plydiveu  20217  vieta1lem2  20230  vieta1  20231  aalioulem2  20252  aalioulem3  20253  aaliou3lem7  20268  tayl0  20280  ulmcn  20317  ulmdvlem3  20320  psercn  20344  abelth  20359  pilem3  20371  efif1olem1  20446  abslogimle  20473  argregt0  20507  argrege0  20508  logf1o2  20543  cxpsqrlem  20595  cxpcn3  20634  abscxpbnd  20639  ang180lem2  20654  ang180lem3  20655  logreclem  20662  xrlimcnp  20809  harmonicbnd4  20851  fsumharmonic  20852  basellem3  20867  basellem4  20868  dvdsppwf1o  20973  dvdsflf1o  20974  fsumfldivdiaglem  20976  chpeq0  20994  chteq0  20995  chtub  20998  chpub  21006  dchrelbasd  21025  dchrmulcl  21035  dchrinv  21047  bcmono  21063  bposlem1  21070  bposlem2  21071  lgslem1  21082  lgsdirprm  21115  lgsqrlem2  21128  lgsqrlem3  21129  lgsdchr  21134  lgseisenlem1  21135  lgseisenlem2  21136  lgseisenlem3  21137  lgsquadlem1  21140  2sqlem8  21158  2sqblem  21163  chebbnd1lem1  21165  dchrisumlem1  21185  dchrisumlem2  21186  dchrisumlem3  21187  dchrisum0fno1  21207  pntrmax  21260  pntpbnd1a  21281  pntibndlem3  21288  pntlemn  21296  pntlemi  21300  pntlem3  21305  pntleml  21307  ostth1  21329  ostth2  21333  ostth3  21334  cusgra0v  21471  cusgraexi  21479  cusgrares  21483  1pthon  21593  constr2spth  21602  2pthon  21604  constr3trllem3  21641  constr3cycl  21650  eupares  21699  eupap1  21700  nvabs  22164  vacn  22192  nmcvcn  22193  nmblore  22289  0lno  22293  0blo  22295  nmlno0lem  22296  occl  22808  pjhthlem1  22895  pjpjpre  22923  nmopre  23375  nmlnop0iALT  23500  nmophmi  23536  leoprf2  23632  stlesi  23746  disjdifprg  24019  fzspl  24151  xrge0tsmsd  24225  ofldaddlt  24243  ofldlt1  24245  kerf1hrm  24264  metider  24291  qqhval2lem  24367  qqhcn  24377  pwsiga  24515  prsiga  24516  measle0  24564  mbfmcst  24611  1stmbfm  24612  2ndmbfm  24613  imambfm  24614  cnmbfm  24615  mbfmco  24616  mbfmco2  24617  0rrv  24711  ballotlemfc0  24752  ballotlemfcc  24753  lgamgulmlem5  24819  lgambdd  24823  derangen  24860  subfacval3  24877  cvmseu  24965  cvmliftmolem2  24971  cvmliftlem7  24980  cvmliftlem15  24987  cvmlift2lem9a  24992  cvmlift2lem9  25000  cvmlift2lem10  25001  cvmlift2lem11  25002  cvmlift2lem12  25003  cvmlift3lem6  25013  cvmlift3lem8  25015  fznatpl1  25200  wsuclem  25578  brbtwn2  25846  axlowdimlem3  25885  axlowdimlem16  25898  axcontlem8  25912  supaddc  26239  supadd  26240  mblfinlem2  26246  ovoliunnfl  26250  volsupnfl  26253  mbfresfi  26255  itg2addnclem2  26259  iblabsnc  26271  iblmulc2nc  26272  ftc1cnnclem  26280  ftc1cnnc  26281  ftc1anc  26290  fness  26364  ssref  26365  fnetr  26368  reftr  26371  fnessref  26375  refssfne  26376  neibastop1  26390  neibastop2  26392  tailfb  26408  filnetlem3  26411  fzadd2  26447  sdclem2  26448  metf1o  26463  ismtyhmeolem  26515  ismtyres  26519  heibor1lem  26520  bfplem2  26534  bfp  26535  rrncmslem  26543  iccbnd  26551  icccmpALT  26552  rngogrphom  26589  rngoisoco  26600  keridl  26644  fzsplit1nn0  26814  icodiamlt  26885  irrapxlem3  26889  irrapxlem4  26890  pell1234qrdich  26926  pell1qr1  26936  pell14qrgap  26940  pellqrexplicit  26942  rmspecfund  26974  fzmaxdif  27048  acongeq  27050  jm2.23  27069  jm3.1  27093  lmhmlnmsplit  27164  dsmm0cl  27185  dsmmacl  27186  dsmmsubg  27188  dsmmlss  27189  uvcff  27219  frlmsplit2  27222  lindfrn  27270  f1lindf  27271  lindsss  27273  hbt  27313  dgrsub2  27318  proot1ex  27499  dvconstbi  27530  ubelsupr  27669  fmul01  27688  fmuldfeq  27691  climsuse  27712  stoweidlem7  27734  stoweidlem13  27740  stoweidlem26  27753  wallispilem3  27794  stirlinglem6  27806  stirlinglem10  27810  ubmelfzo  28137  fzo1fzo0n0  28139  cshwlen  28263  2cshw1lem1  28270  3cshw  28291  cshwssizelem1  28302  uvtxnb  28319  usgra2wlkspth  28334  wlklniswwlkn1  28369  0egra0rgra  28435  0vgrargra  28436  frgra0v  28445  frgra1v  28450  bnj1452  29483  lsmcv2  29889  lsatcv0  29891  lcvexchlem4  29897  lcvexchlem5  29898  l1cvpat  29914  lfl0f  29929  lfladdcl  29931  lflnegcl  29935  lkrlss  29955  eqlkr  29959  lkrlsp  29962  lkrlsp2  29963  lshpkrcl  29976  lkrin  30024  1cvrjat  30334  llni  30367  llnle  30377  lplni  30391  lplnle  30399  llncvrlpln2  30416  2atmat  30420  lvoli  30434  lplncvrlvol2  30474  elpaddri  30661  paddclN  30701  pclclN  30750  pclfinN  30759  0psubclN  30802  1psubclN  30803  atpsubclN  30804  pmapsubclN  30805  osumclN  30826  pexmidN  30828  pexmidlem6N  30834  lhp2lt  30860  lautcnv  30949  idlaut  30955  lautco  30956  idldil  30973  ldilcnv  30974  ldilco  30975  ltrncnv  31005  idltrn  31009  cdleme16d  31140  cdleme50laut  31406  cdleme50ldil  31407  cdleme50ltrn  31416  ltrnco  31578  dian0  31899  dia0eldmN  31900  dia1eldmN  31901  dialss  31906  diaintclN  31918  docaclN  31984  doca2N  31986  djajN  31997  dibintclN  32027  diblss  32030  dicvaddcl  32050  dicvscacl  32051  dicn0  32052  cdlemn11a  32067  dihord2cN  32081  dihord11b  32082  dihord6apre  32116  dihmeetlem1N  32150  dihglblem5apreN  32151  dihpN  32196  dihjatcclem4  32281  dochkr1  32338  islpoldN  32344  lcfrlem31  32433  mapdpglem18  32549  mapdheq2  32589  mapdheq4  32592  mapdh6aN  32595  hdmap1l6a  32670  hdmap1neglem1N  32688  hdmap14lem4a  32734
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 179  df-an 362
  Copyright terms: Public domain W3C validator