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

Theorem mpbir2and 959
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 (𝜑𝜒)
mpbir2and.2 (𝜑𝜃)
mpbir2and.3 (𝜑 → (𝜓 ↔ (𝜒𝜃)))
Assertion
Ref Expression
mpbir2and (𝜑𝜓)

Proof of Theorem mpbir2and
StepHypRef Expression
1 mpbir2and.1 . . 3 (𝜑𝜒)
2 mpbir2and.2 . . 3 (𝜑𝜃)
31, 2jca 553 . 2 (𝜑 → (𝜒𝜃))
4 mpbir2and.3 . 2 (𝜑 → (𝜓 ↔ (𝜒𝜃)))
53, 4mpbird 246 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wa 383
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 196  df-an 385
This theorem is referenced by:  fveqressseq  6248  fmptsng  6317  fmptsnd  6318  fnprb  6355  fntpb  6356  fdmfifsupp  8146  fczfsuppd  8154  fsuppmptif  8166  fsuppco2  8169  fsuppcor  8170  dffi3  8198  suppr  8238  infpr  8270  ordtypelem7  8290  cantnf0  8433  cantnfp1lem1  8436  cantnfp1lem2  8437  cantnfp1lem3  8438  cantnflem1a  8443  cantnflem1d  8446  cantnflem1  8447  cantnf  8451  rankpwi  8547  carduni  8668  fin23lem32  9027  fpwwe2lem6  9314  fpwwe2lem9  9317  fpwwe2lem12  9320  fpwwe2lem13  9321  fpwwe2  9322  inttsk  9453  grutsk1  9500  add20  10392  supaddc  10840  supadd  10841  supmul  10845  suprzcl  11292  uzwo3  11618  rpnnen1lem5  11653  rpnnen1lem5OLD  11659  xrre  11836  xrre3  11838  xleadd1a  11915  xlemul1a  11950  supxrre  11988  ixxub  12026  elioc2  12066  elico2  12067  elicc2  12068  elfz1eq  12181  fzadd2  12205  fznatpl1  12223  nn0fz0  12264  fzctr  12278  fzo1fzo0n0  12344  fzoaddel  12346  elincfzoext  12351  flid  12429  flval3  12436  fladdz  12446  fldiv  12479  modid  12515  seqf1olem1  12660  bcval5  12925  hashf1lem1  13051  eqs1  13194  wwlktovf1  13497  sqeqd  13703  sqrlem7  13786  max0add  13847  abs2difabs  13871  rddif  13877  fzomaxdiflem  13879  rexico  13890  icodiamlt  13971  limsupgre  14009  rlim3  14026  icco1  14068  rlimclim  14074  rlimuni  14078  rlimresb  14093  isercolllem2  14193  isercolllem3  14194  isercoll  14195  caucvgrlem  14200  caurcvgr  14201  iseraltlem3  14211  fsum00  14320  o1fsum  14335  bitsfzolem  14943  bitsfzo  14944  bitsmod  14945  bitscmp  14947  gcd0id  15027  gcdneg  15030  bezoutlem4  15046  nn0seqcvgd  15070  lcmneg  15103  qredeq  15158  prmind2  15185  isprm5  15206  hashdvds  15267  eulerthlem2  15274  pcpremul  15335  pcidlem  15363  pcgcd1  15368  pcadd2  15381  fldivp1  15388  pcfaclem  15389  prmreclem5  15411  4sqlem17  15452  vdwlem1  15472  vdwlem6  15477  vdwlem12  15483  vdwlem13  15484  0ram  15511  ram0  15513  ramub1lem1  15517  invco  16203  sectmon  16214  monsect  16215  invid  16219  cicref  16233  ssctr  16257  ssceq  16258  0ssc  16269  0subcat  16270  catsubcat  16271  issubc3  16281  fullsubc  16282  funcinv  16305  fthmon  16359  fuccocl  16396  fucidcl  16397  invfuc  16406  2initoinv  16432  2termoinv  16439  elhomai  16455  setcmon  16509  setcepi  16510  catcisolem  16528  curf2cl  16643  yonedalem4c  16689  yonedalem3  16692  yoniso  16697  lublecl  16761  isacs3lem  16938  tsrdir  17010  mnd1  17103  sgrp2nmndlem4  17187  sgrp2nmndlem5  17188  nmznsg  17410  ghmpreima  17454  ghmeql  17455  ghmnsgpreima  17457  cntzsubm  17540  cntzsubg  17541  cntzmhm  17543  symgextfo  17614  symgfixf1  17629  symgfixfolem1  17630  odlem2  17730  gexlem2  17769  gexcl2  17776  sylow1lem5  17789  subgslw  17803  slwhash  17811  fislw  17812  sylow3lem1  17814  lsmsubg  17841  efgredlemd  17929  efgredlem  17932  efgcpbllemb  17940  frgpuplem  17957  cyggeninv  18057  iscygd  18061  iscygodd  18062  gsumzadd  18094  gsumconst  18106  gsumpt  18133  gsum2dlem2  18142  gsum2d  18143  gsum2d2lem  18144  dprdfcntz  18186  eldprdi  18189  subgdmdprd  18205  subgdprd  18206  dprdpr  18221  ablfac1c  18242  ablfac1eu  18244  ablfaclem3  18258  ring1  18374  kerf1hrm  18515  issubdrg  18577  rhmeql  18582  rhmima  18583  cntzsubr  18584  isabvd  18592  abvdiv  18609  lsslsp  18785  lmhmima  18817  lmhmpreima  18818  lmhmeql  18825  lsmcl  18853  lspfixed  18898  issubassa  19094  issubassa2  19115  snifpsrbag  19136  psrbaglesupp  19138  psrbaglecl  19139  psrbagaddcl  19140  psrbagcon  19141  mplsubglem  19204  mpllsslem  19205  mplassa  19224  subrgmpl  19230  mplcoe5  19238  mplbas2  19240  mplind  19272  evlslem3  19284  mpfind  19306  ply1assa  19339  coe1tmmul2  19416  coe1tmmul  19417  cply1coe0bi  19440  qsssubdrg  19573  gzrngunit  19580  evpmodpmf1o  19709  ocvpj  19828  dsmm0cl  19851  dsmmacl  19852  dsmmsubg  19854  dsmmlss  19855  frlmsplit2  19879  uvcff  19897  lindfrn  19927  f1lindf  19928  lindsss  19930  mat1rngiso  20059  dmatid  20068  dmatsubcl  20071  dmatscmcl  20076  scmatid  20087  scmataddcl  20089  scmatsubcl  20090  scmatmulcl  20091  smatvscl  20097  scmatrhmcl  20101  scmatrngiso  20109  mat0scmat  20111  mat1scmat  20112  mdet0pr  20165  m2cpmrngiso  20330  pm2mprngiso  20394  chmaidscmat  20420  fvmptnn04if  20421  distop  20558  indistopon  20563  ppttop  20569  epttop  20571  mretopd  20654  toponmre  20655  neiss  20671  opnneissb  20676  ssnei2  20678  innei  20687  neiptoptop  20693  ordtcld1  20759  ordtcld2  20760  lmconst  20823  cnpnei  20826  iscncl  20831  cnss1  20838  cnss2  20839  cncnpi  20840  cncnp  20842  cnconst2  20845  cnrest  20847  cnpresti  20850  cnpdis  20855  paste  20856  lmcnp  20866  cnhaus  20916  hauscmp  20968  2ndcomap  21019  1stcelcls  21022  1stccnp  21023  llyrest  21046  nllyrest  21047  llyidm  21049  nllyidm  21050  ssref  21073  reftr  21075  refun0  21076  dissnref  21089  kgentopon  21099  kgenidm  21108  kgencn3  21119  txcld  21164  neitx  21168  tx1cn  21170  tx2cn  21171  ptcld  21174  xkoccn  21180  txcnp  21181  ptcnp  21183  txcnmpt  21185  ptcn  21188  txdis1cn  21196  ptrescn  21200  txkgen  21213  xkoco1cn  21218  xkoco2cn  21219  xkococn  21221  xkoinjcn  21248  qtoptop2  21260  qtopuni  21263  qtopid  21266  qtopkgen  21271  basqtop  21272  tgqtop  21273  qtopss  21276  qtopeu  21277  qtoprest  21278  kqopn  21295  kqcld  21296  kqreglem2  21303  reghmph  21354  ordthmeolem  21362  qtopf1  21377  opnfbas  21404  isfil2  21418  fbasweak  21427  fsubbas  21429  filcon  21445  fbasrn  21446  rnelfmlem  21514  flimss2  21534  flimss1  21535  hausflim  21543  flimclslem  21546  flimsncls  21548  cnpflfi  21561  flfcnp2  21569  fclsfnflim  21589  cnextfvval  21627  cnextfres1  21630  symgtgp  21663  opnsubg  21669  ghmcnp  21676  qustgpopn  21681  qustgplem  21682  qustgphaus  21684  tsmsfbas  21689  ustfilxp  21774  utoptop  21796  utopbas  21797  restutopopn  21800  iducn  21845  cstucnd  21846  ucncn  21847  fmucnd  21854  cfilufg  21855  trcfilu  21856  cfiluweak  21857  neipcfilu  21858  psmetsym  21873  psmetres2  21877  isxmetd  21889  xmetsym  21910  xmetpsmet  21911  imasf1oxmet  21938  xblss2ps  21964  xblss2  21965  xblcntrps  21973  xblcntr  21974  blcld  22068  metustfbas  22120  cfilucfil  22122  restmetu  22133  ngptgp  22198  tngngpd  22215  nrmtngnrm  22220  tngnrg  22236  nlmvscn  22249  nrginvrcn  22254  nmo0  22297  nmoeq0  22298  nmoid  22304  nghmcn  22307  0nmhm  22317  blcvx  22357  zcld  22372  iccntr  22380  xrge0tsms  22393  xmetdcn2  22396  metdstri  22410  metdscn  22415  rescncf  22456  cncfco  22466  oprpiece1res2  22507  cnheibor  22510  cnllycmp  22511  bndth  22513  evth  22514  ishtpyd  22530  isphtpyd  22541  pcoval2  22572  nmhmcn  22676  ipcn  22798  lmnn  22814  cfilss  22821  iscfil3  22824  cfilfcls  22825  cmetcaulem  22839  iscmet3lem2  22843  cfilres  22847  lmcau  22864  flimcfil  22865  cncmet  22872  rlmbn  22910  minveclem3b  22952  pjthlem1  22961  pjth2  22964  ivthlem3  22974  ovolssnul  23007  ovolctb  23010  ovolunnul  23020  ovoliunnul  23027  ovolsca  23035  ovolicc  23043  ovolicopnf  23044  voliunlem2  23071  voliunlem3  23072  volsup  23076  uniioovol  23098  uniiccvol  23099  dyadmaxlem  23116  vitalilem5  23132  ismbfd  23158  mbfres  23162  mbfss  23164  mbfmulc2re  23166  mbfadd  23179  mbfmulc2  23181  mbflim  23186  i1faddlem  23211  i1fmullem  23212  mbfmul  23244  itg2itg1  23254  itg2seq  23260  itg2eqa  23263  itg2mulc  23265  itg2split  23267  itg2mono  23271  itg2cnlem1  23279  ibl0  23304  iblposlem  23309  itgreval  23314  iblneg  23320  iblss  23322  iblss2  23323  itgle  23327  iblconst  23335  iblabs  23346  iblabsr  23347  iblmulc2  23348  bddmulibl  23356  limciun  23409  limcun  23410  dvres2lem  23425  dvidlem  23430  dvcnp2  23434  dvcn  23435  cpnres  23451  dvaddbr  23452  dvmulbr  23453  dvcobr  23460  dvcjbr  23463  dvrec  23469  dvcnvlem  23488  dvferm  23500  dvlip2  23507  dveq0  23512  dv11cn  23513  dvivthlem1  23520  lhop1  23526  lhop2  23527  lhop  23528  dvcnvre  23531  dvfsumlem3  23540  dvfsumlem4  23541  dvfsumrlim  23543  dvfsum2  23546  ftc1a  23549  ftc1lem4  23551  ftc1lem6  23553  ftc1  23554  coe1mul3  23608  deg1addle2  23611  deg1add  23612  deg1sublt  23619  deg1mul2  23623  deg1tm  23627  fta1blem  23677  drnguc1p  23679  ig1prsp  23686  plyco0  23697  plyeq0lem  23715  dgrub  23739  dgreq  23749  dgradd2  23773  dgrmul  23775  dgrcolem2  23779  dgrco  23780  plycpn  23793  plydivlem4  23800  plydiveu  23802  vieta1lem2  23815  vieta1  23816  aalioulem2  23837  aalioulem3  23838  aaliou3lem7  23853  tayl0  23865  ulmcn  23902  ulmdvlem3  23905  psercn  23929  abelth  23944  pilem3  23956  efif1olem1  24037  abslogimle  24069  argregt0  24105  argrege0  24106  logf1o2  24141  cxpsqrtlem  24193  cxpcn3  24234  abscxpbnd  24239  logreclem  24245  ang180lem2  24285  ang180lem3  24286  xrlimcnp  24440  harmonicbnd4  24482  fsumharmonic  24483  lgamgulmlem5  24504  lgambdd  24508  basellem3  24554  basellem4  24555  dvdsppwf1o  24657  dvdsflf1o  24658  fsumfldivdiaglem  24660  chpeq0  24678  chteq0  24679  chtub  24682  chpub  24690  dchrelbasd  24709  dchrmulcl  24719  dchrinv  24731  bcmono  24747  bposlem1  24754  bposlem2  24755  lgslem1  24767  lgsdirprm  24801  lgsqrlem2  24817  lgsqrlem3  24818  lgsdchr  24825  lgseisenlem1  24845  lgseisenlem2  24846  lgseisenlem3  24847  lgsquadlem1  24850  2sqlem8  24896  2sqblem  24901  chebbnd1lem1  24903  dchrisumlem1  24923  dchrisumlem2  24924  dchrisumlem3  24925  dchrisum0fno1  24945  pntrmax  24998  pntpbnd1a  25019  pntibndlem3  25026  pntlemn  25034  pntlemi  25038  pntlem3  25043  pntleml  25045  ostth1  25067  ostth2  25071  ostth3  25072  ercgrg  25158  motco  25181  cnvmot  25182  legso  25240  mirmot  25316  lmicom  25426  lmimid  25432  lmimot  25436  hypcgrlem1  25437  hypcgrlem2  25438  ttgcontlem1  25511  brbtwn2  25531  axlowdimlem3  25570  axlowdimlem16  25583  axcontlem8  25597  cusgra0v  25783  cusgraexi  25791  cusgrares  25795  uvtxnb  25819  1pthon  25915  constr2spth  25924  2pthon  25926  usgra2wlkspthlem2  25942  usgra2wlkspth  25943  constr3trllem3  25974  constr3cycl  25983  wlklniswwlkn1  26021  vfwlkniswwlkn  26028  usg2wlkeq2  26031  wwlknred  26045  wwlknredwwlkn0  26049  clwlkisclwwlklem2a1  26101  clwwlkel  26115  wwlkext2clwwlk  26125  clwwnisshclwwn  26131  clwlkf1clwwlk  26171  0egra0rgra  26257  0vgrargra  26258  eupares  26296  eupap1  26297  frgra0v  26314  frgra1v  26319  nvabs  26705  vacn  26727  nmcvcn  26728  nmblore  26819  0lno  26823  0blo  26825  nmlno0lem  26826  occl  27341  pjhthlem1  27428  pjpjpre  27456  nmopre  27907  nmlnop0iALT  28032  nmophmi  28068  leoprf2  28164  stlesi  28278  disjdifprg  28564  disjun0  28584  fpwrelmap  28690  fzspl  28732  2sqmod  28773  ogrpaddlt  28843  ogrpsublt  28847  pnfinf  28862  xrge0tsmsd  28910  ornglmullt  28932  orngrmullt  28933  orngmullt  28934  ofldlt1  28938  isarchiofld  28942  psgnfzto1stlem  28975  fzto1st1  28977  qtopt1  29024  reff  29028  locfinreflem  29029  metideq  29058  metider  29059  pstmxmet  29062  qqhval2lem  29147  qqhcn  29157  qqhucn  29158  pwsiga  29314  prsiga  29315  measle0  29392  mbfmcst  29442  1stmbfm  29443  2ndmbfm  29444  imambfm  29445  cnmbfm  29446  mbfmco  29447  mbfmco2  29448  0elcarsg  29490  carsgclctun  29504  sibfof  29523  oddpwdc  29537  eulerpartlemmf  29558  eulerpartlemgs2  29563  0rrv  29634  ballotlemfc0  29675  ballotlemfcc  29676  signstfveq0  29774  bnj1452  30168  derangen  30202  subfacval3  30219  cvmseu  30306  cvmliftmolem2  30312  cvmliftlem7  30321  cvmliftlem15  30328  cvmlift2lem9a  30333  cvmlift2lem9  30341  cvmlift2lem10  30342  cvmlift2lem11  30343  cvmlift2lem12  30344  cvmlift3lem6  30354  cvmlift3lem8  30356  mclsppslem  30528  mclspps  30529  wsuclem  30811  wsuclemOLD  30812  nosepon  30860  fness  31308  fnetr  31310  fnessref  31316  refssfne  31317  neibastop1  31318  neibastop2  31320  tailfb  31336  filnetlem3  31339  bj-finsumval0  32118  poimirlem13  32386  poimirlem15  32388  poimirlem17  32390  poimirlem24  32397  poimirlem28  32401  mblfinlem2  32411  ovoliunnfl  32415  volsupnfl  32418  mbfresfi  32420  itg2addnclem2  32426  iblabsnc  32438  iblmulc2nc  32439  ftc1cnnclem  32447  ftc1cnnc  32448  ftc1anc  32457  sdclem2  32502  metf1o  32515  ismtyhmeolem  32567  ismtyres  32571  heibor1lem  32572  bfplem2  32586  bfp  32587  rrncmslem  32595  iccbnd  32603  icccmpALT  32604  rngogrphom  32734  rngoisoco  32745  keridl  32795  lsmcv2  33128  lsatcv0  33130  lcvexchlem4  33136  lcvexchlem5  33137  l1cvpat  33153  lfl0f  33168  lfladdcl  33170  lflnegcl  33174  lkrlss  33194  eqlkr  33198  lkrlsp  33201  lkrlsp2  33202  lshpkrcl  33215  lkrin  33263  1cvrjat  33573  llni  33606  llnle  33616  lplni  33630  lplnle  33638  llncvrlpln2  33655  2atmat  33659  lvoli  33673  lplncvrlvol2  33713  elpaddri  33900  paddclN  33940  pclclN  33989  pclfinN  33998  0psubclN  34041  1psubclN  34042  atpsubclN  34043  pmapsubclN  34044  osumclN  34065  pexmidN  34067  pexmidlem6N  34073  lhp2lt  34099  lautcnv  34188  idlaut  34194  lautco  34195  idldil  34212  ldilcnv  34213  ldilco  34214  ltrncnv  34244  idltrn  34248  cdleme16d  34380  cdleme50laut  34647  cdleme50ldil  34648  cdleme50ltrn  34657  ltrnco  34819  dian0  35140  dia0eldmN  35141  dia1eldmN  35142  dialss  35147  diaintclN  35159  docaclN  35225  doca2N  35227  djajN  35238  dibintclN  35268  diblss  35271  dicvaddcl  35291  dicvscacl  35292  dicn0  35293  cdlemn11a  35308  dihord2cN  35322  dihord11b  35323  dihord6apre  35357  dihmeetlem1N  35391  dihglblem5apreN  35392  dihpN  35437  dihjatcclem4  35522  dochkr1  35579  islpoldN  35585  lcfrlem31  35674  mapdpglem18  35790  mapdheq2  35830  mapdheq4  35833  mapdh6aN  35836  hdmap1l6a  35911  hdmap1neglem1N  35929  hdmap14lem4a  35975  fzsplit1nn0  36129  irrapxlem3  36200  irrapxlem4  36201  pell1234qrdich  36237  pell1qr1  36247  pell14qrgap  36251  pellqrexplicit  36253  rmspecfund  36286  fzmaxdif  36360  acongeq  36362  jm2.23  36375  jm3.1  36399  lmhmlnmsplit  36469  hbt  36513  dgrsub2  36518  proot1ex  36592  clublem  36730  dftrcl3  36825  hashnzfz2  37336  dvconstbi  37349  ubelsupr  37996  lefldiveq  38240  iccintsng  38390  fmul01  38441  fmuldfeq  38444  climsuse  38469  mullimc  38477  limcdm0  38479  limccog  38481  mullimcf  38484  constlimc  38485  idlimc  38487  limcperiod  38489  limsupre  38502  limcleqr  38505  neglimc  38508  addlimc  38509  0ellimcdiv  38510  cncfshift  38553  cncfperiod  38558  cncfuni  38566  icccncfext  38567  cncfiooicclem1  38573  fperdvper  38602  ioodvbdlimc1lem2  38616  ioodvbdlimc2lem  38618  mbfres2cn  38644  iblsplit  38652  stoweidlem7  38694  stoweidlem13  38700  stoweidlem26  38713  wallispilem3  38754  stirlinglem6  38766  stirlinglem10  38770  dirkercncf  38794  fourierdlem6  38800  fourierdlem11  38805  fourierdlem12  38806  fourierdlem15  38809  fourierdlem26  38820  fourierdlem42  38836  fourierdlem50  38843  fourierdlem51  38844  fourierdlem52  38845  fourierdlem54  38847  fourierdlem62  38855  fourierdlem79  38872  fourierdlem102  38895  fourierdlem114  38907  etransclem23  38944  zgeltp1eq  39738  iccpartres  39751  pfx2  40070  pfxccatin12d  40090  repswpfx  40094  fusgrfis  40541  nbgr2vtx1edg  40564  uvtxnbgrb  40620  cplgr1v  40644  0vtxrgr  40768  0vtxrusgr  40769  ewlkle  40799  1wlk1ewlk  40836  uspgr2wlkeq2  40847  1wlkp1lem8  40881  trlres  40900  trlOntrl  40910  pthOnpth  40946  uhgr1wlkspth  40953  usgr2wlkspth  40957  pthdlem2  40966  crctcshtrl  41018  1wlklnwwlkln1  41057  wlknewwlksn  41076  wwlksnred  41090  wwlksnredwwlkn0  41094  2trld  41137  2trlond  41138  2spthd  41140  2pthond  41141  elwwlks2ons3  41151  clwlkclwwlklem2a1  41193  clwwlksel  41213  wwlksext2clwwlk  41223  clwwnisshclwwsn  41229  clwlksf1clwwlk  41268  0TrlOn  41284  0pthon-av  41287  1trld  41301  1pthond  41303  lp1cycl  41311  3trld  41331  3trlond  41332  3pthond  41334  3spthd  41335  3spthond  41336  3cycld  41337  eupthres  41375  eupthp1  41376  eupth2eucrct  41377  frgrregorufrg  41497  rabsubmgmd  41573  submgmid  41575  subsubmgm  41579  mgmhmima  41584  mgmhmeql  41585  isassintop  41628  rnghmsscmap2  41757  rnghmsscmap  41758  rnghmsubcsetc  41761  zrzeroorngc  41786  rhmsscmap2  41803  rhmsscmap  41804  rhmsubcsetc  41807  rhmsscrnghm  41810  rhmsubcrngc  41813  srhmsubc  41860  fldhmsubc  41868  rhmsubc  41874  srhmsubcALTV  41879  fldhmsubcALTV  41887  rhmsubcALTV  41893  rmfsupp  41941  mndpfsupp  41943  scmfsupp  41945  mptcfsupp  41947  lcoel0  42003  lincsumcl  42006  lincscmcl  42007  lcoss  42011  lindsrng01  42043  lincreslvec3  42057  lindssnlvec  42061  zgtp1leeq  42097
  Copyright terms: Public domain W3C validator