Theorem mpbir2and 957

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

Step	Hyp	Ref	Expression
1		mpbir2and.1	. . 3 |- ( ph -> ch )
2		mpbir2and.2	. . 3 |- ( ph -> th )
3	1, 2	jca 554	. 2 |- ( ph -> ( ch /\ th ) )
4		mpbir2and.3	. 2 |- ( ph -> ( ps <-> ( ch /\ th ) ) )
5	3, 4	mpbird 247	1 |- ( ph -> ps )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  fveqressseq  6355  fmptsng  6434  fmptsnd  6435  fnprb  6472  fntpb  6473  fdmfifsupp  8285  fczfsuppd  8293  fsuppmptif  8305  fsuppco2  8308  fsuppcor  8309  dffi3  8337  suppr  8377  infpr  8409  ordtypelem7  8429  cantnf0  8572  cantnfp1lem1  8575  cantnfp1lem2  8576  cantnfp1lem3  8577  cantnflem1a  8582  cantnflem1d  8585  cantnflem1  8586  cantnf  8590  rankpwi  8686  carduni  8807  fin23lem32  9166  fpwwe2lem6  9457  fpwwe2lem9  9460  fpwwe2lem12  9463  fpwwe2lem13  9464  fpwwe2  9465  inttsk  9596  grutsk1  9643  add20  10540  supaddc  10990  supadd  10991  supmul  10995  suprzcl  11457  uzwo3  11783  rpnnen1lem5  11818  rpnnen1lem5OLD  11824  xrre  12000  xrre3  12002  xleadd1a  12083  xlemul1a  12118  supxrre  12157  ixxub  12196  elioc2  12236  elico2  12237  elicc2  12238  elfz1eq  12352  fzadd2  12376  fznatpl1  12395  elfz1uz  12410  nn0fz0  12437  fzctr  12451  fzo1fzo0n0  12518  fzoaddel  12520  elincfzoext  12525  flid  12609  flval3  12616  fladdz  12626  fldiv  12659  modid  12695  seqf1olem1  12840  bcval5  13105  hashf1lem1  13239  eqs1  13392  wwlktovf1  13700  sqeqd  13906  sqrlem7  13989  max0add  14050  abs2difabs  14074  rddif  14080  fzomaxdiflem  14082  rexico  14093  icodiamlt  14174  limsupgre  14212  rlim3  14229  icco1  14271  rlimclim  14277  rlimuni  14281  rlimresb  14296  isercolllem2  14396  isercolllem3  14397  isercoll  14398  caucvgrlem  14403  caurcvgr  14404  iseraltlem3  14414  fsum00  14530  o1fsum  14545  bitsfzolem  15156  bitsfzo  15157  bitsmod  15158  bitscmp  15160  gcd0id  15240  gcdneg  15243  bezoutlem4  15259  nn0seqcvgd  15283  lcmneg  15316  qredeq  15371  prmind2  15398  isprm5  15419  hashdvds  15480  eulerthlem2  15487  pcpremul  15548  pcidlem  15576  pcgcd1  15581  pcadd2  15594  fldivp1  15601  pcfaclem  15602  prmreclem5  15624  4sqlem17  15665  vdwlem1  15685  vdwlem6  15690  vdwlem12  15696  vdwlem13  15697  0ram  15724  ram0  15726  ramub1lem1  15730  invco  16431  sectmon  16442  monsect  16443  invid  16447  cicref  16461  ssctr  16485  ssceq  16486  0ssc  16497  0subcat  16498  catsubcat  16499  issubc3  16509  fullsubc  16510  funcinv  16533  fthmon  16587  fuccocl  16624  fucidcl  16625  invfuc  16634  2initoinv  16660  2termoinv  16667  elhomai  16683  setcmon  16737  setcepi  16738  catcisolem  16756  curf2cl  16871  yonedalem4c  16917  yonedalem3  16920  yoniso  16925  lublecl  16989  isacs3lem  17166  tsrdir  17238  mnd1  17331  sgrp2nmndlem4  17415  sgrp2nmndlem5  17416  nmznsg  17638  ghmpreima  17682  ghmeql  17683  ghmnsgpreima  17685  cntzsubm  17768  cntzsubg  17769  cntzmhm  17771  symgextfo  17842  symgfixf1  17857  symgfixfolem1  17858  odlem2  17958  gexlem2  17997  gexcl2  18004  sylow1lem5  18017  subgslw  18031  slwhash  18039  fislw  18040  sylow3lem1  18042  lsmsubg  18069  efgredlemd  18157  efgredlem  18160  efgcpbllemb  18168  frgpuplem  18185  cyggeninv  18285  iscygd  18289  iscygodd  18290  gsumzadd  18322  gsumconst  18334  gsumpt  18361  gsum2dlem2  18370  gsum2d  18371  gsum2d2lem  18372  dprdfcntz  18414  eldprdi  18417  subgdmdprd  18433  subgdprd  18434  dprdpr  18449  ablfac1c  18470  ablfac1eu  18472  ablfaclem3  18486  ring1  18602  kerf1hrm  18743  issubdrg  18805  rhmeql  18810  rhmima  18811  cntzsubr  18812  isabvd  18820  abvdiv  18837  lsslsp  19015  lmhmima  19047  lmhmpreima  19048  lmhmeql  19055  lsmcl  19083  lspfixed  19128  issubassa  19324  issubassa2  19345  snifpsrbag  19366  psrbaglesupp  19368  psrbaglecl  19369  psrbagaddcl  19370  psrbagcon  19371  mplsubglem  19434  mpllsslem  19435  mplassa  19454  subrgmpl  19460  mplcoe5  19468  mplbas2  19470  mplind  19502  evlslem3  19514  mpfind  19536  ply1assa  19569  coe1tmmul2  19646  coe1tmmul  19647  cply1coe0bi  19670  qsssubdrg  19805  gzrngunit  19812  evpmodpmf1o  19942  ocvpj  20061  dsmm0cl  20084  dsmmacl  20085  dsmmsubg  20087  dsmmlss  20088  frlmsplit2  20112  uvcff  20130  lindfrn  20160  f1lindf  20161  lindsss  20163  mat1rngiso  20292  dmatid  20301  dmatsubcl  20304  dmatscmcl  20309  scmatid  20320  scmataddcl  20322  scmatsubcl  20323  scmatmulcl  20324  smatvscl  20330  scmatrhmcl  20334  scmatrngiso  20342  mat0scmat  20344  mat1scmat  20345  mdet0pr  20398  m2cpmrngiso  20563  pm2mprngiso  20627  chmaidscmat  20653  fvmptnn04if  20654  distop  20799  indistopon  20805  ppttop  20811  epttop  20813  mretopd  20896  toponmre  20897  neiss  20913  opnneissb  20918  ssnei2  20920  innei  20929  neiptoptop  20935  ordtcld1  21001  ordtcld2  21002  lmconst  21065  cnpnei  21068  iscncl  21073  cnss1  21080  cnss2  21081  cncnpi  21082  cncnp  21084  cnconst2  21087  cnrest  21089  cnpresti  21092  cnpdis  21097  paste  21098  lmcnp  21108  cnhaus  21158  hauscmp  21210  2ndcomap  21261  1stcelcls  21264  1stccnp  21265  llyrest  21288  nllyrest  21289  llyidm  21291  nllyidm  21292  ssref  21315  reftr  21317  refun0  21318  dissnref  21331  kgentopon  21341  kgenidm  21350  kgencn3  21361  txcld  21406  neitx  21410  tx1cn  21412  tx2cn  21413  ptcld  21416  xkoccn  21422  txcnp  21423  ptcnp  21425  txcnmpt  21427  ptcn  21430  txdis1cn  21438  ptrescn  21442  txkgen  21455  xkoco1cn  21460  xkoco2cn  21461  xkococn  21463  xkoinjcn  21490  qtoptop2  21502  qtopuni  21505  qtopid  21508  qtopkgen  21513  basqtop  21514  tgqtop  21515  qtopss  21518  qtopeu  21519  qtoprest  21520  kqopn  21537  kqcld  21538  kqreglem2  21545  reghmph  21596  ordthmeolem  21604  qtopf1  21619  opnfbas  21646  isfil2  21660  fbasweak  21669  fsubbas  21671  filconn  21687  fbasrn  21688  rnelfmlem  21756  flimss2  21776  flimss1  21777  hausflim  21785  flimclslem  21788  flimsncls  21790  cnpflfi  21803  flfcnp2  21811  fclsfnflim  21831  cnextfvval  21869  cnextfres1  21872  symgtgp  21905  opnsubg  21911  ghmcnp  21918  qustgpopn  21923  qustgplem  21924  qustgphaus  21926  tsmsfbas  21931  ustfilxp  22016  utoptop  22038  utopbas  22039  restutopopn  22042  iducn  22087  cstucnd  22088  ucncn  22089  fmucnd  22096  cfilufg  22097  trcfilu  22098  cfiluweak  22099  neipcfilu  22100  psmetsym  22115  psmetres2  22119  isxmetd  22131  xmetsym  22152  xmetpsmet  22153  imasf1oxmet  22180  xblss2ps  22206  xblss2  22207  xblcntrps  22215  xblcntr  22216  blcld  22310  metustfbas  22362  cfilucfil  22364  restmetu  22375  ngptgp  22440  tngngpd  22457  nrmtngnrm  22462  tngnrg  22478  nlmvscn  22491  nrginvrcn  22496  nmo0  22539  nmoeq0  22540  nmoid  22546  nghmcn  22549  0nmhm  22559  blcvx  22601  zcld  22616  iccntr  22624  xrge0tsms  22637  xmetdcn2  22640  metdstri  22654  metdscn  22659  rescncf  22700  cncfco  22710  oprpiece1res2  22751  cnheibor  22754  cnllycmp  22755  bndth  22757  evth  22758  ishtpyd  22774  isphtpyd  22785  pcoval2  22816  nmhmcn  22920  ipcn  23045  lmnn  23061  cfilss  23068  iscfil3  23071  cfilfcls  23072  cmetcaulem  23086  iscmet3lem2  23090  cfilres  23094  lmcau  23111  flimcfil  23112  cncmet  23119  rlmbn  23157  minveclem3b  23199  pjthlem1  23208  pjth2  23211  ivthlem3  23222  ovolssnul  23255  ovolctb  23258  ovolunnul  23268  ovoliunnul  23275  ovolsca  23283  ovolicc  23291  ovolicopnf  23292  voliunlem2  23319  voliunlem3  23320  volsup  23324  uniioovol  23347  uniiccvol  23348  dyadmaxlem  23365  vitalilem5  23381  ismbfd  23407  mbfres  23411  mbfss  23413  mbfmulc2re  23415  mbfadd  23428  mbfmulc2  23430  mbflim  23435  i1faddlem  23460  i1fmullem  23461  mbfmul  23493  itg2itg1  23503  itg2seq  23509  itg2eqa  23512  itg2mulc  23514  itg2split  23516  itg2mono  23520  itg2cnlem1  23528  ibl0  23553  iblposlem  23558  itgreval  23563  iblneg  23569  iblss  23571  iblss2  23572  itgle  23576  iblconst  23584  iblabs  23595  iblabsr  23596  iblmulc2  23597  bddmulibl  23605  limciun  23658  limcun  23659  dvres2lem  23674  dvidlem  23679  dvcnp2  23683  dvcn  23684  cpnres  23700  dvaddbr  23701  dvmulbr  23702  dvcobr  23709  dvcjbr  23712  dvrec  23718  dvcnvlem  23739  dvferm  23751  dvlip2  23758  dveq0  23763  dv11cn  23764  dvivthlem1  23771  lhop1  23777  lhop2  23778  lhop  23779  dvcnvre  23782  dvfsumlem3  23791  dvfsumlem4  23792  dvfsumrlim  23794  dvfsum2  23797  ftc1a  23800  ftc1lem4  23802  ftc1lem6  23804  ftc1  23805  coe1mul3  23859  deg1addle2  23862  deg1add  23863  deg1sublt  23870  deg1mul2  23874  deg1tm  23878  fta1blem  23928  drnguc1p  23930  ig1prsp  23937  plyco0  23948  plyeq0lem  23966  dgrub  23990  dgreq  24000  dgradd2  24024  dgrmul  24026  dgrcolem2  24030  dgrco  24031  plycpn  24044  plydivlem4  24051  plydiveu  24053  vieta1lem2  24066  vieta1  24067  aalioulem2  24088  aalioulem3  24089  aaliou3lem7  24104  tayl0  24116  ulmcn  24153  ulmdvlem3  24156  psercn  24180  abelth  24195  pilem3  24207  efif1olem1  24288  abslogimle  24320  argregt0  24356  argrege0  24357  logf1o2  24396  cxpsqrtlem  24448  cxpcn3  24489  abscxpbnd  24494  logreclem  24500  ang180lem2  24540  ang180lem3  24541  xrlimcnp  24695  harmonicbnd4  24737  fsumharmonic  24738  lgamgulmlem5  24759  lgambdd  24763  basellem3  24809  basellem4  24810  dvdsppwf1o  24912  dvdsflf1o  24913  fsumfldivdiaglem  24915  chpeq0  24933  chteq0  24934  chtub  24937  chpub  24945  dchrelbasd  24964  dchrmulcl  24974  dchrinv  24986  bcmono  25002  bposlem1  25009  bposlem2  25010  lgslem1  25022  lgsdirprm  25056  lgsqrlem2  25072  lgsqrlem3  25073  lgsdchr  25080  lgseisenlem1  25100  lgseisenlem2  25101  lgseisenlem3  25102  lgsquadlem1  25105  2sqlem8  25151  2sqblem  25156  chebbnd1lem1  25158  dchrisumlem1  25178  dchrisumlem2  25179  dchrisumlem3  25180  dchrisum0fno1  25200  pntrmax  25253  pntpbnd1a  25274  pntibndlem3  25281  pntlemn  25289  pntlemi  25293  pntlem3  25298  pntleml  25300  ostth1  25322  ostth2  25326  ostth3  25327  ercgrg  25412  motco  25435  cnvmot  25436  legso  25494  mirmot  25570  lmicom  25680  lmimid  25686  lmimot  25690  hypcgrlem1  25691  hypcgrlem2  25692  ttgcontlem1  25765  brbtwn2  25785  axlowdimlem3  25824  axlowdimlem16  25837  axcontlem8  25851  fusgrfis  26222  nbgr2vtx1edg  26246  uvtxnbgrb  26302  cplgr1v  26326  structtocusgr  26342  0vtxrgr  26472  0vtxrusgr  26473  ewlkle  26501  wlk1ewlk  26536  uspgr2wlkeq2  26543  wlkp1lem8  26577  trlontrl  26607  pthonpth  26644  pthdlem2  26664  wlklnwwlkln1  26754  wlknewwlksn  26773  wwlksnred  26787  wwlksnredwwlkn0  26791  2trlond  26835  2pthond  26838  elwwlks2ons3  26848  clwlkclwwlklem2a1  26893  clwwlkinwwlk  26905  clwwlksel  26914  wwlksext2clwwlk  26924  clwwnisshclwwsn  26930  clwlksf1clwwlk  26969  0trlon  26985  0pthon  26988  1pthond  27004  3trlond  27033  3pthond  27035  3spthond  27037  eupthres  27075  nvabs  27527  vacn  27549  nmcvcn  27550  nmblore  27641  0lno  27645  0blo  27647  nmlno0lem  27648  occl  28163  pjhthlem1  28250  pjpjpre  28278  nmopre  28729  nmlnop0iALT  28854  nmophmi  28890  leoprf2  28986  stlesi  29100  disjdifprg  29388  disjun0  29408  fpwrelmap  29508  fzspl  29550  2sqmod  29648  ogrpaddlt  29718  ogrpsublt  29722  pnfinf  29737  xrge0tsmsd  29785  ornglmullt  29807  orngrmullt  29808  orngmullt  29809  ofldlt1  29813  isarchiofld  29817  psgnfzto1stlem  29850  fzto1st1  29852  qtopt1  29902  reff  29906  locfinreflem  29907  metideq  29936  metider  29937  pstmxmet  29940  qqhval2lem  30025  qqhcn  30035  qqhucn  30036  pwsiga  30193  prsiga  30194  measle0  30271  mbfmcst  30321  1stmbfm  30322  2ndmbfm  30323  imambfm  30324  cnmbfm  30325  mbfmco  30326  mbfmco2  30327  0elcarsg  30369  carsgclctun  30383  sibfof  30402  oddpwdc  30416  eulerpartlemmf  30437  eulerpartlemgs2  30442  0rrv  30513  ballotlemfc0  30554  ballotlemfcc  30555  signstfveq0  30654  breprexplemc  30710  bnj1452  31120  derangen  31154  subfacval3  31171  cvmseu  31258  cvmliftmolem2  31264  cvmliftlem7  31273  cvmliftlem15  31280  cvmlift2lem9a  31285  cvmlift2lem9  31293  cvmlift2lem10  31294  cvmlift2lem11  31295  cvmlift2lem12  31296  cvmlift3lem6  31306  cvmlift3lem8  31308  mclsppslem  31480  mclspps  31481  wsuclem  31773  wsuclemOLD  31774  nosepon  31818  nolesgn2ores  31825  nosupres  31853  nosupbnd1lem2  31855  nosupbnd2lem1  31861  fness  32344  fnetr  32346  fnessref  32352  refssfne  32353  neibastop1  32354  neibastop2  32356  tailfb  32372  filnetlem3  32375  bj-finsumval0  33147  dfgcd3  33170  poimirlem13  33422  poimirlem15  33424  poimirlem17  33426  poimirlem24  33433  poimirlem28  33437  mblfinlem2  33447  ovoliunnfl  33451  volsupnfl  33454  mbfresfi  33456  itg2addnclem2  33462  iblabsnc  33474  iblmulc2nc  33475  ftc1cnnclem  33483  ftc1cnnc  33484  ftc1anc  33493  sdclem2  33538  metf1o  33551  ismtyhmeolem  33603  ismtyres  33607  heibor1lem  33608  bfplem2  33622  bfp  33623  rrncmslem  33631  iccbnd  33639  icccmpALT  33640  rngogrphom  33770  rngoisoco  33781  keridl  33831  lsmcv2  34316  lsatcv0  34318  lcvexchlem4  34324  lcvexchlem5  34325  l1cvpat  34341  lfl0f  34356  lfladdcl  34358  lflnegcl  34362  lkrlss  34382  eqlkr  34386  lkrlsp  34389  lkrlsp2  34390  lshpkrcl  34403  lkrin  34451  1cvrjat  34761  llni  34794  llnle  34804  lplni  34818  lplnle  34826  llncvrlpln2  34843  2atmat  34847  lvoli  34861  lplncvrlvol2  34901  elpaddri  35088  paddclN  35128  pclclN  35177  pclfinN  35186  0psubclN  35229  1psubclN  35230  atpsubclN  35231  pmapsubclN  35232  osumclN  35253  pexmidN  35255  pexmidlem6N  35261  lhp2lt  35287  lautcnv  35376  idlaut  35382  lautco  35383  idldil  35400  ldilcnv  35401  ldilco  35402  ltrncnv  35432  idltrn  35436  cdleme16d  35568  cdleme50laut  35835  cdleme50ldil  35836  cdleme50ltrn  35845  ltrnco  36007  dian0  36328  dia0eldmN  36329  dia1eldmN  36330  dialss  36335  diaintclN  36347  docaclN  36413  doca2N  36415  djajN  36426  dibintclN  36456  diblss  36459  dicvaddcl  36479  dicvscacl  36480  dicn0  36481  cdlemn11a  36496  dihord2cN  36510  dihord11b  36511  dihord6apre  36545  dihmeetlem1N  36579  dihglblem5apreN  36580  dihpN  36625  dihjatcclem4  36710  dochkr1  36767  islpoldN  36773  lcfrlem31  36862  mapdpglem18  36978  mapdheq2  37018  mapdheq4  37021  mapdh6aN  37024  hdmap1l6a  37099  hdmap1neglem1N  37117  hdmap14lem4a  37163  fzsplit1nn0  37317  irrapxlem3  37388  irrapxlem4  37389  pell1234qrdich  37425  pell1qr1  37435  pell14qrgap  37439  pellqrexplicit  37441  rmspecfund  37474  fzmaxdif  37548  acongeq  37550  jm2.23  37563  jm3.1  37587  lmhmlnmsplit  37657  hbt  37700  dgrsub2  37705  proot1ex  37779  clublem  37917  dftrcl3  38012  hashnzfz2  38520  dvconstbi  38533  ubelsupr  39179  lefldiveq  39505  iccintsng  39749  fmul01  39812  fmuldfeq  39815  climsuse  39840  mullimc  39848  limcdm0  39850  limccog  39852  mullimcf  39855  constlimc  39856  idlimc  39858  limcperiod  39860  limsupre  39873  limcleqr  39876  neglimc  39879  addlimc  39880  0ellimcdiv  39881  cncfshift  40087  cncfperiod  40092  cncfuni  40099  icccncfext  40100  cncfiooicclem1  40106  fperdvper  40133  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  mbfres2cn  40174  iblsplit  40182  stoweidlem7  40224  stoweidlem13  40230  stoweidlem26  40243  wallispilem3  40284  stirlinglem6  40296  stirlinglem10  40300  dirkercncf  40324  fourierdlem6  40330  fourierdlem11  40335  fourierdlem12  40336  fourierdlem15  40339  fourierdlem26  40350  fourierdlem42  40366  fourierdlem50  40373  fourierdlem51  40374  fourierdlem52  40375  fourierdlem54  40377  fourierdlem62  40385  fourierdlem79  40402  fourierdlem102  40425  fourierdlem114  40437  etransclem23  40474  zgeltp1eq  41318  setsnidel  41347  iccpartres  41354  pfx2  41412  pfxccatin12d  41432  repswpfx  41436  rabsubmgmd  41791  submgmid  41793  subsubmgm  41797  mgmhmima  41802  mgmhmeql  41803  isassintop  41846  rnghmsscmap2  41973  rnghmsscmap  41974  rnghmsubcsetc  41977  zrzeroorngc  42002  rhmsscmap2  42019  rhmsscmap  42020  rhmsubcsetc  42023  rhmsscrnghm  42026  rhmsubcrngc  42029  srhmsubc  42076  fldhmsubc  42084  rhmsubc  42090  srhmsubcALTV  42094  fldhmsubcALTV  42102  rhmsubcALTV  42108  rmfsupp  42155  mndpfsupp  42157  scmfsupp  42159  mptcfsupp  42161  lcoel0  42217  lincsumcl  42220  lincscmcl  42221  lcoss  42225  lindsrng01  42257  lincreslvec3  42271  lindssnlvec  42275  zgtp1leeq  42311