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

Theorem mpbir2and 930
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 534 . 2  |-  ( ph  ->  ( ch  /\  th ) )
4 mpbir2and.3 . 2  |-  ( ph  ->  ( ps  <->  ( ch  /\ 
th ) ) )
53, 4mpbird 235 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  fveqressseq  6033  fmptsng  6100  fmptsnd  6101  fnprb  6138  fdmfifsupp  7899  fczfsuppd  7907  fsuppmptif  7919  fsuppco2  7922  fsuppcor  7923  dffi3  7951  supmaxOLD  7989  suppr  7993  infpr  8019  ordtypelem7  8039  cantnf0  8179  cantnfp1lem1  8182  cantnfp1lem2  8183  cantnfp1lem3  8184  cantnflem1a  8189  cantnflem1d  8192  cantnflem1  8193  cantnf  8197  rankpwi  8293  carduni  8414  fin23lem32  8772  fpwwe2lem6  9059  fpwwe2lem9  9062  fpwwe2lem12  9065  fpwwe2lem13  9066  fpwwe2  9067  inttsk  9198  grutsk1  9245  add20  10125  supaddc  10574  supadd  10575  supmul  10579  suprzcl  11015  uzwo3  11259  rpnnen1lem5  11294  xrre  11464  xrre3  11466  xleadd1a  11539  xlemul1a  11574  supxrre  11613  infmxrreOLD  11626  ixxub  11656  ixxlbOLD  11658  elioc2  11697  elico2  11698  elicc2  11699  elfz1eq  11808  fznatpl1  11848  nn0fz0  11888  fzctr  11901  fzo1fzo0n0  11955  fzoaddel  11964  elincfzoext  11969  flid  12041  flval3  12047  fladdz  12055  fldiv  12084  modid  12118  seqf1olem1  12249  bcval5  12500  hashf1lem1  12613  eqs1  12735  wwlktovf1  13011  sqeqd  13208  sqrlem7  13291  max0add  13352  abs2difabs  13376  rddif  13382  fzomaxdiflem  13384  rexico  13395  limsupgre  13520  limsupgreOLD  13521  rlim3  13540  icco1  13582  rlimclim  13588  rlimuni  13592  rlimresb  13607  isercolllem2  13707  isercolllem3  13708  isercoll  13709  caucvgrlem  13714  caucvgrlemOLD  13715  caurcvgr  13716  caurcvgrOLD  13717  iseraltlem3  13728  fsum00  13836  o1fsum  13851  dvdseq  14330  bitsfzolem  14382  bitsfzo  14383  bitsmod  14384  bitscmp  14386  gcd0id  14461  gcdneg  14464  bezoutlem4  14480  nn0seqcvgd  14500  lcmneg  14533  prmind2  14597  isprm5  14613  qredeq  14625  hashdvds  14683  eulerthlem2  14690  pcpremul  14747  pcidlem  14775  pcgcd1  14780  pcadd2  14789  fldivp1  14796  pcfaclem  14797  prmreclem5  14818  4sqlem17OLD  14859  4sqlem17  14865  vdwlem1  14885  vdwlem6  14890  vdwlem12  14896  vdwlem13  14897  0ram  14932  ram0  14934  ramub1lem1  14938  invco  15618  sectmon  15629  monsect  15630  invid  15634  cicref  15648  ssctr  15672  ssceq  15673  0ssc  15684  0subcat  15685  catsubcat  15686  issubc3  15696  fullsubc  15697  funcinv  15720  fthmon  15774  fuccocl  15811  fucidcl  15812  invfuc  15821  2initoinv  15847  2termoinv  15854  elhomai  15870  setcmon  15924  setcepi  15925  catcisolem  15943  curf2cl  16058  yonedalem4c  16104  yonedalem3  16107  yoniso  16112  lublecl  16177  isacs3lem  16354  tsrdir  16426  mnd1  16519  mnd1OLD  16520  sgrp2nmndlem4  16604  sgrp2nmndlem5  16605  nmznsg  16803  ghmpreima  16846  ghmeql  16847  ghmnsgpreima  16849  cntzsubm  16931  cntzsubg  16932  cntzmhm  16934  symgextfo  17005  symgfixf1  17020  symgfixfolem1  17021  odlem2  17121  gexlem2  17160  gexcl2  17167  sylow1lem5  17180  subgslw  17194  slwhash  17202  fislw  17203  sylow3lem1  17205  lsmsubg  17232  efgredlemd  17320  efgredlem  17323  efgcpbllemb  17331  frgpuplem  17348  cyggeninv  17444  iscygd  17448  iscygodd  17449  gsumzadd  17481  gsumconst  17493  gsumpt  17520  gsum2dlem2  17529  gsum2d  17530  gsum2d2lem  17531  dprdfcntz  17574  eldprdi  17577  subgdmdprd  17593  subgdprd  17594  dprdpr  17609  ablfac1c  17630  ablfac1eu  17632  ablfaclem3  17646  ring1  17756  kerf1hrm  17897  issubdrg  17959  rhmeql  17964  rhmima  17965  cntzsubr  17966  isabvd  17974  abvdiv  17991  lsslsp  18164  lmhmima  18196  lmhmpreima  18197  lmhmeql  18204  lsmcl  18232  lspfixed  18277  issubassa  18474  issubassa2  18495  snifpsrbag  18516  psrbaglesupp  18518  psrbaglecl  18519  psrbagaddcl  18520  psrbagcon  18521  mplsubglem  18584  mpllsslem  18585  mplassa  18604  subrgmpl  18610  mplcoe5  18618  mplbas2  18620  mplind  18651  evlslem3  18663  mpfind  18685  ply1assa  18718  coe1tmmul2  18795  coe1tmmul  18796  cply1coe0bi  18820  qsssubdrg  18953  gzrngunit  18959  evpmodpmf1o  19086  ocvpj  19202  dsmm0cl  19225  dsmmacl  19226  dsmmsubg  19228  dsmmlss  19229  frlmsplit2  19253  uvcff  19271  lindfrn  19301  f1lindf  19302  lindsss  19304  mat1rngiso  19433  dmatid  19442  dmatsubcl  19445  dmatscmcl  19450  scmatid  19461  scmataddcl  19463  scmatsubcl  19464  scmatmulcl  19465  smatvscl  19471  scmatrhmcl  19475  scmatrngiso  19483  mat0scmat  19485  mat1scmat  19486  mdet0pr  19539  m2cpmrngiso  19704  pm2mprngiso  19768  chmaidscmat  19794  fvmptnn04if  19795  distop  19933  indistopon  19938  ppttop  19944  epttop  19946  mretopd  20030  toponmre  20031  neiss  20047  opnneissb  20052  ssnei2  20054  innei  20063  neiptoptop  20069  ordtcld1  20135  ordtcld2  20136  lmconst  20199  cnpnei  20202  iscncl  20207  cnss1  20214  cnss2  20215  cncnpi  20216  cncnp  20218  cnconst2  20221  cnrest  20223  cnpresti  20226  cnpdis  20231  paste  20232  lmcnp  20242  cnhaus  20292  hauscmp  20344  2ndcomap  20395  1stcelcls  20398  1stccnp  20399  llyrest  20422  nllyrest  20423  llyidm  20425  nllyidm  20426  ssref  20449  reftr  20451  refun0  20452  dissnref  20465  kgentopon  20475  kgenidm  20484  kgencn3  20495  txcld  20540  neitx  20544  tx1cn  20546  tx2cn  20547  ptcld  20550  xkoccn  20556  txcnp  20557  ptcnp  20559  txcnmpt  20561  ptcn  20564  txdis1cn  20572  ptrescn  20576  txkgen  20589  xkoco1cn  20594  xkoco2cn  20595  xkococn  20597  xkoinjcn  20624  qtoptop2  20636  qtopuni  20639  qtopid  20642  qtopkgen  20647  basqtop  20648  tgqtop  20649  qtopss  20652  qtopeu  20653  qtoprest  20654  kqopn  20671  kqcld  20672  kqreglem2  20679  reghmph  20730  ordthmeolem  20738  qtopf1  20753  opnfbas  20779  isfil2  20793  fbasweak  20802  fsubbas  20804  filcon  20820  fbasrn  20821  rnelfmlem  20889  flimss2  20909  flimss1  20910  hausflim  20918  flimclslem  20921  flimsncls  20923  cnpflfi  20936  flfcnp2  20944  fclsfnflim  20964  cnextfvval  21002  cnextfres1  21005  symgtgp  21038  opnsubg  21044  ghmcnp  21051  qustgpopn  21056  qustgplem  21057  qustgphaus  21059  tsmsfbas  21064  ustfilxp  21149  utoptop  21171  utopbas  21172  restutopopn  21175  iducn  21220  cstucnd  21221  ucncn  21222  fmucnd  21229  cfilufg  21230  trcfilu  21231  cfiluweak  21232  neipcfilu  21233  psmetsym  21248  psmetres2  21252  isxmetd  21263  xmetsym  21284  xmetpsmet  21285  imasdsf1olem  21310  imasf1oxmet  21312  xblss2ps  21338  xblss2  21339  xblcntrps  21347  xblcntr  21348  blcld  21442  metustfbas  21494  cfilucfil  21496  restmetu  21507  ngptgp  21566  tngngpd  21583  tngnrg  21599  nlmvscn  21612  nrginvrcn  21616  nmo0  21658  nmoeq0  21659  nmoid  21665  nghmcn  21668  0nmhm  21678  blcvx  21718  zcld  21733  iccntr  21741  xrge0tsms  21754  xmetdcn2  21757  metdstri  21770  metdscn  21775  rescncf  21816  cncfco  21826  oprpiece1res2  21867  cnheibor  21870  cnllycmp  21871  bndth  21873  evth  21874  ishtpyd  21890  isphtpyd  21901  pcoval2  21931  nmhmcn  22018  ipcn  22101  lmnn  22117  cfilss  22124  iscfil3  22127  cfilfcls  22128  cmetcaulem  22142  iscmet3lem2  22146  cfilres  22150  lmcau  22166  flimcfil  22167  cncmet  22174  rlmbn  22212  minveclem3b  22254  pjthlem1  22263  pjth2  22266  ivthlem3  22276  ovolssnul  22309  ovolctb  22312  ovolunnul  22322  ovoliunnul  22329  ovolsca  22337  ovolicc  22345  ovolicopnf  22346  voliunlem2  22372  voliunlem3  22373  volsup  22377  uniioovol  22404  uniiccvol  22405  dyadmaxlem  22423  vitalilem5  22438  ismbfd  22464  mbfres  22468  mbfss  22470  mbfmulc2re  22472  mbfadd  22485  mbfmulc2  22487  mbflimsupOLD  22492  mbflim  22494  i1faddlem  22519  i1fmullem  22520  mbfmul  22552  itg2itg1  22562  itg2seq  22568  itg2eqa  22571  itg2mulc  22573  itg2split  22575  itg2mono  22579  itg2cnlem1  22587  ibl0  22612  iblposlem  22617  itgreval  22622  iblneg  22628  iblss  22630  iblss2  22631  itgle  22635  iblconst  22643  iblabs  22654  iblabsr  22655  iblmulc2  22656  bddmulibl  22664  limciun  22717  limcun  22718  dvres2lem  22733  dvidlem  22738  dvcnp2  22742  dvcn  22743  cpnres  22759  dvaddbr  22760  dvmulbr  22761  dvcobr  22768  dvcjbr  22771  dvrec  22777  dvcnvlem  22796  dvferm  22808  dvlip2  22815  dveq0  22820  dv11cn  22821  dvivthlem1  22828  lhop1  22834  lhop2  22835  lhop  22836  dvcnvre  22839  dvfsumlem3  22848  dvfsumlem4  22849  dvfsumrlim  22851  dvfsum2  22854  ftc1a  22857  ftc1lem4  22859  ftc1lem6  22861  ftc1  22862  coe1mul3  22916  deg1addle2  22919  deg1add  22920  deg1sublt  22927  deg1mul2  22931  deg1tm  22935  fta1blem  22985  drnguc1p  22987  ig1prsp  22994  plyco0  23005  plyeq0lem  23023  dgrub  23047  dgreq  23057  dgradd2  23081  dgrmul  23083  dgrcolem2  23087  dgrco  23088  plycpn  23101  plydivlem4  23108  plydiveu  23110  vieta1lem2  23123  vieta1  23124  aalioulem2  23145  aalioulem3  23146  aaliou3lem7  23161  tayl0  23173  ulmcn  23210  ulmdvlem3  23213  psercn  23237  abelth  23252  pilem3  23265  pilem3OLD  23266  efif1olem1  23347  abslogimle  23379  argregt0  23415  argrege0  23416  logf1o2  23451  cxpsqrtlem  23503  cxpcn3  23544  abscxpbnd  23549  logreclem  23555  ang180lem2  23595  ang180lem3  23596  xrlimcnp  23750  harmonicbnd4  23792  fsumharmonic  23793  lgamgulmlem5  23814  lgambdd  23818  basellem3  23863  basellem4  23864  dvdsppwf1o  23969  dvdsflf1o  23970  fsumfldivdiaglem  23972  chpeq0  23990  chteq0  23991  chtub  23994  chpub  24002  dchrelbasd  24021  dchrmulcl  24031  dchrinv  24043  bcmono  24059  bposlem1  24066  bposlem2  24067  lgslem1  24078  lgsdirprm  24111  lgsqrlem2  24124  lgsqrlem3  24125  lgsdchr  24130  lgseisenlem1  24131  lgseisenlem2  24132  lgseisenlem3  24133  lgsquadlem1  24136  2sqlem8  24154  2sqblem  24159  chebbnd1lem1  24161  dchrisumlem1  24181  dchrisumlem2  24182  dchrisumlem3  24183  dchrisum0fno1  24203  pntrmax  24256  pntpbnd1a  24277  pntibndlem3  24284  pntlemn  24292  pntlemi  24296  pntlem3  24301  pntleml  24303  ostth1  24325  ostth2  24329  ostth3  24330  ercgrg  24415  motco  24436  cnvmot  24437  legso  24495  mirmot  24570  lmicom  24677  lmimid  24683  lmimot  24687  hypcgrlem1  24688  hypcgrlem2  24689  ttgcontlem1  24752  brbtwn2  24772  axlowdimlem3  24811  axlowdimlem16  24824  axcontlem8  24838  cusgra0v  25024  cusgraexi  25032  cusgrares  25036  uvtxnb  25061  1pthon  25157  constr2spth  25166  2pthon  25168  usgra2wlkspthlem2  25184  usgra2wlkspth  25185  constr3trllem3  25216  constr3cycl  25225  wlklniswwlkn1  25263  vfwlkniswwlkn  25270  usg2wlkeq2  25273  wwlknred  25287  wwlknredwwlkn0  25291  clwlkisclwwlklem2a1  25343  clwwlkel  25357  wwlkext2clwwlk  25367  clwwnisshclwwn  25373  clwlkf1clwwlk  25414  0egra0rgra  25500  0vgrargra  25501  eupares  25539  eupap1  25540  frgra0v  25557  frgra1v  25562  nvabs  26138  vacn  26166  nmcvcn  26167  nmblore  26263  0lno  26267  0blo  26269  nmlno0lem  26270  occl  26783  pjhthlem1  26870  pjpjpre  26898  nmopre  27349  nmlnop0iALT  27474  nmophmi  27510  leoprf2  27606  stlesi  27720  disjdifprg  28015  fpwrelmap  28152  fzspl  28195  2sqmod  28238  ogrpaddlt  28310  ogrpsublt  28314  pnfinf  28329  xrge0tsmsd  28378  ornglmullt  28400  orngrmullt  28401  orngmullt  28402  ofldlt1  28406  isarchiofld  28410  psgnfzto1stlem  28443  fzto1st1  28445  qtopt1  28492  reff  28496  locfinreflem  28497  metideq  28526  metider  28527  pstmxmet  28530  qqhval2lem  28615  qqhcn  28625  qqhucn  28626  pwsiga  28782  prsiga  28783  measle0  28860  mbfmcst  28911  1stmbfm  28912  2ndmbfm  28913  imambfm  28914  cnmbfm  28915  mbfmco  28916  mbfmco2  28917  carsgclctun  28973  sibfof  28992  oddpwdc  29004  eulerpartlemmf  29025  eulerpartlemgs2  29030  0rrv  29101  ballotlemfc0  29142  ballotlemfcc  29143  signstfveq0  29245  bnj1452  29640  derangen  29674  subfacval3  29691  cvmseu  29778  cvmliftmolem2  29784  cvmliftlem7  29793  cvmliftlem15  29800  cvmlift2lem9a  29805  cvmlift2lem9  29813  cvmlift2lem10  29814  cvmlift2lem11  29815  cvmlift2lem12  29816  cvmlift3lem6  29826  cvmlift3lem8  29828  mclsppslem  30000  mclspps  30001  wsuclem  30286  fness  30781  fnetr  30783  fnessref  30789  refssfne  30790  neibastop1  30791  neibastop2  30793  tailfb  30809  filnetlem3  30812  bj-finsumval0  31438  poimirlem13  31647  poimirlem15  31649  poimirlem17  31651  poimirlem24  31658  poimirlem28  31662  mblfinlem2  31672  ovoliunnfl  31676  volsupnfl  31679  mbfresfi  31681  dvtanlemOLD  31685  itg2addnclem2  31688  iblabsnc  31700  iblmulc2nc  31701  ftc1cnnclem  31709  ftc1cnnc  31710  ftc1anc  31719  fzadd2  31764  sdclem2  31765  metf1o  31778  ismtyhmeolem  31830  ismtyres  31834  heibor1lem  31835  bfplem2  31849  bfp  31850  rrncmslem  31858  iccbnd  31866  icccmpALT  31867  rngogrphom  31904  rngoisoco  31915  keridl  31959  lsmcv2  32294  lsatcv0  32296  lcvexchlem4  32302  lcvexchlem5  32303  l1cvpat  32319  lfl0f  32334  lfladdcl  32336  lflnegcl  32340  lkrlss  32360  eqlkr  32364  lkrlsp  32367  lkrlsp2  32368  lshpkrcl  32381  lkrin  32429  1cvrjat  32739  llni  32772  llnle  32782  lplni  32796  lplnle  32804  llncvrlpln2  32821  2atmat  32825  lvoli  32839  lplncvrlvol2  32879  elpaddri  33066  paddclN  33106  pclclN  33155  pclfinN  33164  0psubclN  33207  1psubclN  33208  atpsubclN  33209  pmapsubclN  33210  osumclN  33231  pexmidN  33233  pexmidlem6N  33239  lhp2lt  33265  lautcnv  33354  idlaut  33360  lautco  33361  idldil  33378  ldilcnv  33379  ldilco  33380  ltrncnv  33410  idltrn  33414  cdleme16d  33546  cdleme50laut  33813  cdleme50ldil  33814  cdleme50ltrn  33823  ltrnco  33985  dian0  34306  dia0eldmN  34307  dia1eldmN  34308  dialss  34313  diaintclN  34325  docaclN  34391  doca2N  34393  djajN  34404  dibintclN  34434  diblss  34437  dicvaddcl  34457  dicvscacl  34458  dicn0  34459  cdlemn11a  34474  dihord2cN  34488  dihord11b  34489  dihord6apre  34523  dihmeetlem1N  34557  dihglblem5apreN  34558  dihpN  34603  dihjatcclem4  34688  dochkr1  34745  islpoldN  34751  lcfrlem31  34840  mapdpglem18  34956  mapdheq2  34996  mapdheq4  34999  mapdh6aN  35002  hdmap1l6a  35077  hdmap1neglem1N  35095  hdmap14lem4a  35141  fzsplit1nn0  35295  icodiamlt  35364  irrapxlem3  35368  irrapxlem4  35369  pell1234qrdich  35405  pell1qr1  35415  pell14qrgap  35419  pellqrexplicit  35421  rmspecfund  35453  fzmaxdif  35527  acongeq  35529  jm2.23  35547  jm3.1  35571  lmhmlnmsplit  35641  hbt  35685  dgrsub2  35690  proot1ex  35767  dftrcl3  35941  hashnzfz2  36297  dvconstbi  36310  ubelsupr  36971  lefldiveq  37105  iccintsng  37199  fmul01  37220  fmuldfeq  37223  climsuse  37249  mullimc  37258  limcdm0  37260  limccog  37262  mullimcf  37265  constlimc  37266  idlimc  37268  limcperiod  37270  limsupre  37283  limsupreOLD  37284  limcleqr  37287  neglimc  37290  addlimc  37291  0ellimcdiv  37292  cncfshift  37313  cncfperiod  37318  cncfuni  37326  icccncfext  37327  cncfiooicclem1  37333  fperdvper  37352  ioodvbdlimc1lem2  37366  ioodvbdlimc2lem  37368  mbfres2cn  37394  iblsplit  37402  stoweidlem7  37426  stoweidlem13  37432  stoweidlem26  37445  wallispilem3  37488  stirlinglem6  37500  stirlinglem10  37504  dirkercncf  37528  fourierdlem6  37534  fourierdlem11  37539  fourierdlem12  37540  fourierdlem15  37543  fourierdlem26  37554  fourierdlem42  37570  fourierdlem50  37578  fourierdlem51  37579  fourierdlem52  37580  fourierdlem54  37582  fourierdlem62  37590  fourierdlem79  37607  fourierdlem102  37630  fourierdlem114  37642  etransclem23  37679  zgeltp1eq  38097  iccpartres  38112  pfx2  38333  pfxccatin12d  38353  repswpfx  38357  rabsubmgmd  38539  submgmid  38541  subsubmgm  38545  mgmhmima  38550  mgmhmeql  38551  isassintop  38594  rnghmsscmap2  38723  rnghmsscmap  38724  rnghmsubcsetc  38727  zrzeroorngc  38752  rhmsscmap2  38769  rhmsscmap  38770  rhmsubcsetc  38773  rhmsscrnghm  38776  rhmsubcrngc  38779  srhmsubc  38826  fldhmsubc  38834  rhmsubc  38840  srhmsubcALTV  38845  fldhmsubcALTV  38853  rhmsubcALTV  38859  rmfsupp  38909  mndpfsupp  38911  scmfsupp  38913  mptcfsupp  38915  lcoel0  38971  lincsumcl  38974  lincscmcl  38975  lcoss  38979  lindsrng01  39011  lincreslvec3  39025  lindssnlvec  39029  zgtp1leeq  39070
  Copyright terms: Public domain W3C validator