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

Theorem mpbir2and 977
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 247 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  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 197  df-an 385
This theorem is referenced by:  fveqressseq  6395  fmptsng  6475  fmptsnd  6476  fnprb  6513  fntpb  6514  fdmfifsupp  8326  fczfsuppd  8334  fsuppmptif  8346  fsuppco2  8349  fsuppcor  8350  dffi3  8378  suppr  8418  infpr  8450  ordtypelem7  8470  cantnf0  8610  cantnfp1lem1  8613  cantnfp1lem2  8614  cantnfp1lem3  8615  cantnflem1a  8620  cantnflem1d  8623  cantnflem1  8624  cantnf  8628  rankpwi  8724  carduni  8845  fin23lem32  9204  fpwwe2lem6  9495  fpwwe2lem9  9498  fpwwe2lem12  9501  fpwwe2lem13  9502  fpwwe2  9503  inttsk  9634  grutsk1  9681  add20  10578  supaddc  11028  supadd  11029  supmul  11033  suprzcl  11495  uzwo3  11821  rpnnen1lem5  11856  rpnnen1lem5OLD  11862  xrre  12038  xrre3  12040  xleadd1a  12121  xlemul1a  12156  supxrre  12195  ixxub  12234  elioc2  12274  elico2  12275  elicc2  12276  elfz1eq  12390  fzadd2  12414  fznatpl1  12433  elfz1uz  12448  nn0fz0  12476  fzctr  12490  fzo1fzo0n0  12558  fzoaddel  12560  elincfzoext  12565  flid  12649  flval3  12656  fladdz  12666  fldiv  12699  modid  12735  seqf1olem1  12880  bcval5  13145  hashf1lem1  13277  eqs1  13429  wwlktovf1  13746  sqeqd  13950  sqrlem7  14033  max0add  14094  abs2difabs  14118  rddif  14124  fzomaxdiflem  14126  rexico  14137  icodiamlt  14218  limsupgre  14256  rlim3  14273  icco1  14315  rlimclim  14321  rlimuni  14325  rlimresb  14340  isercolllem2  14440  isercolllem3  14441  isercoll  14442  caucvgrlem  14447  caurcvgr  14448  iseraltlem3  14458  fsum00  14574  o1fsum  14589  bitsfzolem  15203  bitsfzo  15204  bitsmod  15205  bitscmp  15207  gcd0id  15287  gcdneg  15290  bezoutlem4  15306  nn0seqcvgd  15330  lcmneg  15363  qredeq  15418  prmind2  15445  isprm5  15466  hashdvds  15527  eulerthlem2  15534  pcpremul  15595  pcidlem  15623  pcgcd1  15628  pcadd2  15641  fldivp1  15648  pcfaclem  15649  prmreclem5  15671  4sqlem17  15712  vdwlem1  15732  vdwlem6  15737  vdwlem12  15743  vdwlem13  15744  0ram  15771  ram0  15773  ramub1lem1  15777  invco  16478  sectmon  16489  monsect  16490  invid  16494  cicref  16508  ssctr  16532  ssceq  16533  0ssc  16544  0subcat  16545  catsubcat  16546  issubc3  16556  fullsubc  16557  funcinv  16580  fthmon  16634  fuccocl  16671  fucidcl  16672  invfuc  16681  2initoinv  16707  2termoinv  16714  elhomai  16730  setcmon  16784  setcepi  16785  catcisolem  16803  curf2cl  16918  yonedalem4c  16964  yonedalem3  16967  yoniso  16972  lublecl  17036  isacs3lem  17213  tsrdir  17285  mnd1  17378  sgrp2nmndlem4  17462  sgrp2nmndlem5  17463  nmznsg  17685  ghmpreima  17729  ghmeql  17730  ghmnsgpreima  17732  cntzsubm  17814  cntzsubg  17815  cntzmhm  17817  symgextfo  17888  symgfixf1  17903  symgfixfolem1  17904  odlem2  18004  gexlem2  18043  gexcl2  18050  sylow1lem5  18063  subgslw  18077  slwhash  18085  fislw  18086  sylow3lem1  18088  lsmsubg  18115  efgredlemd  18203  efgredlem  18206  efgcpbllemb  18214  frgpuplem  18231  cyggeninv  18331  iscygd  18335  iscygodd  18336  gsumzadd  18368  gsumconst  18380  gsumpt  18407  gsum2dlem2  18416  gsum2d  18417  gsum2d2lem  18418  dprdfcntz  18460  eldprdi  18463  subgdmdprd  18479  subgdprd  18480  dprdpr  18495  ablfac1c  18516  ablfac1eu  18518  ablfaclem3  18532  ring1  18648  kerf1hrm  18791  issubdrg  18853  rhmeql  18858  rhmima  18859  cntzsubr  18860  isabvd  18868  abvdiv  18885  lsslsp  19063  lmhmima  19095  lmhmpreima  19096  lmhmeql  19103  lsmcl  19131  lspfixed  19176  issubassa  19372  issubassa2  19393  snifpsrbag  19414  psrbaglesupp  19416  psrbaglecl  19417  psrbagaddcl  19418  psrbagcon  19419  mplsubglem  19482  mpllsslem  19483  mplassa  19502  subrgmpl  19508  mplcoe5  19516  mplbas2  19518  mplind  19550  evlslem3  19562  mpfind  19584  ply1assa  19617  coe1tmmul2  19694  coe1tmmul  19695  cply1coe0bi  19718  qsssubdrg  19853  gzrngunit  19860  evpmodpmf1o  19990  ocvpj  20109  dsmm0cl  20132  dsmmacl  20133  dsmmsubg  20135  dsmmlss  20136  frlmsplit2  20160  uvcff  20178  lindfrn  20208  f1lindf  20209  lindsss  20211  mat1rngiso  20340  dmatid  20349  dmatsubcl  20352  dmatscmcl  20357  scmatid  20368  scmataddcl  20370  scmatsubcl  20371  scmatmulcl  20372  smatvscl  20378  scmatrhmcl  20382  scmatrngiso  20390  mat0scmat  20392  mat1scmat  20393  mdet0pr  20446  m2cpmrngiso  20611  pm2mprngiso  20675  chmaidscmat  20701  fvmptnn04if  20702  distop  20847  indistopon  20853  ppttop  20859  epttop  20861  mretopd  20944  toponmre  20945  neiss  20961  opnneissb  20966  ssnei2  20968  innei  20977  neiptoptop  20983  ordtcld1  21049  ordtcld2  21050  lmconst  21113  cnpnei  21116  iscncl  21121  cnss1  21128  cnss2  21129  cncnpi  21130  cncnp  21132  cnconst2  21135  cnrest  21137  cnpresti  21140  cnpdis  21145  paste  21146  lmcnp  21156  cnhaus  21206  hauscmp  21258  2ndcomap  21309  1stcelcls  21312  1stccnp  21313  llyrest  21336  nllyrest  21337  llyidm  21339  nllyidm  21340  ssref  21363  reftr  21365  refun0  21366  dissnref  21379  kgentopon  21389  kgenidm  21398  kgencn3  21409  txcld  21454  neitx  21458  tx1cn  21460  tx2cn  21461  ptcld  21464  xkoccn  21470  txcnp  21471  ptcnp  21473  txcnmpt  21475  ptcn  21478  txdis1cn  21486  ptrescn  21490  txkgen  21503  xkoco1cn  21508  xkoco2cn  21509  xkococn  21511  xkoinjcn  21538  qtoptop2  21550  qtopuni  21553  qtopid  21556  qtopkgen  21561  basqtop  21562  tgqtop  21563  qtopss  21566  qtopeu  21567  qtoprest  21568  kqopn  21585  kqcld  21586  kqreglem2  21593  reghmph  21644  ordthmeolem  21652  qtopf1  21667  opnfbas  21693  isfil2  21707  fbasweak  21716  fsubbas  21718  filconn  21734  fbasrn  21735  rnelfmlem  21803  flimss2  21823  flimss1  21824  hausflim  21832  flimclslem  21835  flimsncls  21837  cnpflfi  21850  flfcnp2  21858  fclsfnflim  21878  cnextfvval  21916  cnextfres1  21919  symgtgp  21952  opnsubg  21958  ghmcnp  21965  qustgpopn  21970  qustgplem  21971  qustgphaus  21973  tsmsfbas  21978  ustfilxp  22063  utoptop  22085  utopbas  22086  restutopopn  22089  iducn  22134  cstucnd  22135  ucncn  22136  fmucnd  22143  cfilufg  22144  trcfilu  22145  cfiluweak  22146  neipcfilu  22147  psmetsym  22162  psmetres2  22166  isxmetd  22178  xmetsym  22199  xmetpsmet  22200  imasf1oxmet  22227  xblss2ps  22253  xblss2  22254  xblcntrps  22262  xblcntr  22263  blcld  22357  metustfbas  22409  cfilucfil  22411  restmetu  22422  ngptgp  22487  tngngpd  22504  nrmtngnrm  22509  tngnrg  22525  nlmvscn  22538  nrginvrcn  22543  nmo0  22586  nmoeq0  22587  nmoid  22593  nghmcn  22596  0nmhm  22606  blcvx  22648  zcld  22663  iccntr  22671  xrge0tsms  22684  xmetdcn2  22687  metdstri  22701  metdscn  22706  rescncf  22747  cncfco  22757  oprpiece1res2  22798  cnheibor  22801  cnllycmp  22802  bndth  22804  evth  22805  ishtpyd  22821  isphtpyd  22832  pcoval2  22862  nmhmcn  22966  ipcn  23091  lmnn  23107  cfilss  23114  iscfil3  23117  cfilfcls  23118  cmetcaulem  23132  iscmet3lem2  23136  cfilres  23140  lmcau  23157  flimcfil  23158  cncmet  23165  rlmbn  23203  minveclem3b  23245  pjthlem1  23254  pjth2  23257  ivthlem3  23268  ovolssnul  23301  ovolctb  23304  ovolunnul  23314  ovoliunnul  23321  ovolsca  23329  ovolicc  23337  ovolicopnf  23338  voliunlem2  23365  voliunlem3  23366  volsup  23370  uniioovol  23393  uniiccvol  23394  dyadmaxlem  23411  vitalilem5  23426  ismbfd  23452  mbfres  23456  mbfss  23458  mbfmulc2re  23460  mbfadd  23473  mbfmulc2  23475  mbflim  23480  i1faddlem  23505  i1fmullem  23506  mbfmul  23538  itg2itg1  23548  itg2seq  23554  itg2eqa  23557  itg2mulc  23559  itg2split  23561  itg2mono  23565  itg2cnlem1  23573  ibl0  23598  iblposlem  23603  itgreval  23608  iblneg  23614  iblss  23616  iblss2  23617  itgle  23621  iblconst  23629  iblabs  23640  iblabsr  23641  iblmulc2  23642  bddmulibl  23650  limciun  23703  limcun  23704  dvres2lem  23719  dvidlem  23724  dvcnp2  23728  dvcn  23729  cpnres  23745  dvaddbr  23746  dvmulbr  23747  dvcobr  23754  dvcjbr  23757  dvrec  23763  dvcnvlem  23784  dvferm  23796  dvlip2  23803  dveq0  23808  dv11cn  23809  dvivthlem1  23816  lhop1  23822  lhop2  23823  lhop  23824  dvcnvre  23827  dvfsumlem3  23836  dvfsumlem4  23837  dvfsumrlim  23839  dvfsum2  23842  ftc1a  23845  ftc1lem4  23847  ftc1lem6  23849  ftc1  23850  coe1mul3  23904  deg1addle2  23907  deg1add  23908  deg1sublt  23915  deg1mul2  23919  deg1tm  23923  fta1blem  23973  drnguc1p  23975  ig1prsp  23982  plyco0  23993  plyeq0lem  24011  dgrub  24035  dgreq  24045  dgradd2  24069  dgrmul  24071  dgrcolem2  24075  dgrco  24076  plycpn  24089  plydivlem4  24096  plydiveu  24098  vieta1lem2  24111  vieta1  24112  aalioulem2  24133  aalioulem3  24134  aaliou3lem7  24149  tayl0  24161  ulmcn  24198  ulmdvlem3  24201  psercn  24225  abelth  24240  pilem3  24252  efif1olem1  24333  abslogimle  24365  argregt0  24401  argrege0  24402  logf1o2  24441  cxpsqrtlem  24493  cxpcn3  24534  abscxpbnd  24539  logreclem  24545  ang180lem2  24585  ang180lem3  24586  xrlimcnp  24740  harmonicbnd4  24782  fsumharmonic  24783  lgamgulmlem5  24804  lgambdd  24808  basellem3  24854  basellem4  24855  dvdsppwf1o  24957  dvdsflf1o  24958  fsumfldivdiaglem  24960  chpeq0  24978  chteq0  24979  chtub  24982  chpub  24990  dchrelbasd  25009  dchrmulcl  25019  dchrinv  25031  bcmono  25047  bposlem1  25054  bposlem2  25055  lgslem1  25067  lgsdirprm  25101  lgsqrlem2  25117  lgsqrlem3  25118  lgsdchr  25125  lgseisenlem1  25145  lgseisenlem2  25146  lgseisenlem3  25147  lgsquadlem1  25150  2sqlem8  25196  2sqblem  25201  chebbnd1lem1  25203  dchrisumlem1  25223  dchrisumlem2  25224  dchrisumlem3  25225  dchrisum0fno1  25245  pntrmax  25298  pntpbnd1a  25319  pntibndlem3  25326  pntlemn  25334  pntlemi  25338  pntlem3  25343  pntleml  25345  ostth1  25367  ostth2  25371  ostth3  25372  ercgrg  25457  motco  25480  cnvmot  25481  legso  25539  mirmot  25615  lmicom  25725  lmimid  25731  lmimot  25735  hypcgrlem1  25736  hypcgrlem2  25737  ttgcontlem1  25810  brbtwn2  25830  axlowdimlem3  25869  axlowdimlem16  25882  axcontlem8  25896  fusgrfis  26267  nbgr2vtx1edg  26291  0vtxrgr  26528  0vtxrusgr  26529  ewlkle  26557  wlk1ewlk  26592  uspgr2wlkeq2  26599  wlkp1lem8  26633  trlontrl  26663  pthonpth  26700  pthdlem2  26720  wlklnwwlkln1  26822  wlknewwlksn  26841  wwlksnred  26855  wwlksnredwwlkn0  26859  2trlond  26904  2pthond  26907  elwwlks2ons3im  26919  elwwlks2ons3OLD  26921  clwlkclwwlklem2a1  26958  clwwlkel  27009  wwlksext2clwwlk  27021  wwlksext2clwwlkOLD  27022  clwlksf1clwwlk  27056  0trlon  27102  0pthon  27105  1pthond  27122  3trlond  27151  3pthond  27153  3spthond  27155  eupthres  27193  numclwlk1lem2foa  27344  numclwlk1lem2f1  27347  nvabs  27655  vacn  27677  nmcvcn  27678  nmblore  27769  0lno  27773  0blo  27775  nmlno0lem  27776  occl  28291  pjhthlem1  28378  pjpjpre  28406  nmopre  28857  nmlnop0iALT  28982  nmophmi  29018  leoprf2  29114  stlesi  29228  disjdifprg  29514  disjun0  29534  fpwrelmap  29636  fzspl  29678  2sqmod  29776  ogrpaddlt  29846  ogrpsublt  29850  pnfinf  29865  xrge0tsmsd  29913  ornglmullt  29935  orngrmullt  29936  orngmullt  29937  ofldlt1  29941  isarchiofld  29945  psgnfzto1stlem  29978  fzto1st1  29980  qtopt1  30030  reff  30034  locfinreflem  30035  metideq  30064  metider  30065  pstmxmet  30068  qqhval2lem  30153  qqhcn  30163  qqhucn  30164  pwsiga  30321  prsiga  30322  measle0  30399  mbfmcst  30449  1stmbfm  30450  2ndmbfm  30451  imambfm  30452  cnmbfm  30453  mbfmco  30454  mbfmco2  30455  0elcarsg  30497  carsgclctun  30511  sibfof  30530  oddpwdc  30544  eulerpartlemmf  30565  eulerpartlemgs2  30570  0rrv  30641  ballotlemfc0  30682  ballotlemfcc  30683  signstfveq0  30782  breprexplemc  30838  bnj1452  31246  derangen  31280  subfacval3  31297  cvmseu  31384  cvmliftmolem2  31390  cvmliftlem7  31399  cvmliftlem15  31406  cvmlift2lem9a  31411  cvmlift2lem9  31419  cvmlift2lem10  31420  cvmlift2lem11  31421  cvmlift2lem12  31422  cvmlift3lem6  31432  cvmlift3lem8  31434  mclsppslem  31606  mclspps  31607  wsuclem  31895  frrlem4  31908  nosepon  31943  nolesgn2ores  31950  nosupres  31978  nosupbnd1lem2  31980  nosupbnd2lem1  31986  fness  32469  fnetr  32471  fnessref  32477  refssfne  32478  neibastop1  32479  neibastop2  32481  tailfb  32497  filnetlem3  32500  bj-finsumval0  33277  dfgcd3  33300  poimirlem13  33552  poimirlem15  33554  poimirlem17  33556  poimirlem24  33563  poimirlem28  33567  mblfinlem2  33577  ovoliunnfl  33581  volsupnfl  33584  mbfresfi  33586  itg2addnclem2  33592  iblabsnc  33604  iblmulc2nc  33605  ftc1cnnclem  33613  ftc1cnnc  33614  ftc1anc  33623  sdclem2  33668  metf1o  33681  ismtyhmeolem  33733  ismtyres  33737  heibor1lem  33738  bfplem2  33752  bfp  33753  rrncmslem  33761  iccbnd  33769  icccmpALT  33770  rngogrphom  33900  rngoisoco  33911  keridl  33961  lsmcv2  34634  lsatcv0  34636  lcvexchlem4  34642  lcvexchlem5  34643  l1cvpat  34659  lfl0f  34674  lfladdcl  34676  lflnegcl  34680  lkrlss  34700  eqlkr  34704  lkrlsp  34707  lkrlsp2  34708  lshpkrcl  34721  lkrin  34769  1cvrjat  35079  llni  35112  llnle  35122  lplni  35136  lplnle  35144  llncvrlpln2  35161  2atmat  35165  lvoli  35179  lplncvrlvol2  35219  elpaddri  35406  paddclN  35446  pclclN  35495  pclfinN  35504  0psubclN  35547  1psubclN  35548  atpsubclN  35549  pmapsubclN  35550  osumclN  35571  pexmidN  35573  pexmidlem6N  35579  lhp2lt  35605  lautcnv  35694  idlaut  35700  lautco  35701  idldil  35718  ldilcnv  35719  ldilco  35720  ltrncnv  35750  idltrn  35754  cdleme16d  35886  cdleme50laut  36152  cdleme50ldil  36153  cdleme50ltrn  36162  ltrnco  36324  dian0  36645  dia0eldmN  36646  dia1eldmN  36647  dialss  36652  diaintclN  36664  docaclN  36730  doca2N  36732  djajN  36743  dibintclN  36773  diblss  36776  dicvaddcl  36796  dicvscacl  36797  dicn0  36798  cdlemn11a  36813  dihord2cN  36827  dihord11b  36828  dihord6apre  36862  dihmeetlem1N  36896  dihglblem5apreN  36897  dihpN  36942  dihjatcclem4  37027  dochkr1  37084  islpoldN  37090  lcfrlem31  37179  mapdpglem18  37295  mapdheq2  37335  mapdheq4  37338  mapdh6aN  37341  hdmap1l6a  37416  hdmap1neglem1N  37434  hdmap14lem4a  37480  fzsplit1nn0  37634  irrapxlem3  37705  irrapxlem4  37706  pell1234qrdich  37742  pell1qr1  37752  pell14qrgap  37756  pellqrexplicit  37758  rmspecfund  37791  fzmaxdif  37865  acongeq  37867  jm2.23  37880  jm3.1  37904  lmhmlnmsplit  37974  hbt  38017  dgrsub2  38022  proot1ex  38096  clublem  38234  dftrcl3  38329  hashnzfz2  38837  dvconstbi  38850  ubelsupr  39493  lefldiveq  39819  iccintsng  40067  fmul01  40130  fmuldfeq  40133  climsuse  40158  mullimc  40166  limcdm0  40168  limccog  40170  mullimcf  40173  constlimc  40174  idlimc  40176  limcperiod  40178  limsupre  40191  limcleqr  40194  neglimc  40197  addlimc  40198  0ellimcdiv  40199  cncfshift  40405  cncfperiod  40410  cncfuni  40417  icccncfext  40418  cncfiooicclem1  40424  fperdvper  40451  ioodvbdlimc1lem2  40465  ioodvbdlimc2lem  40467  mbfres2cn  40492  iblsplit  40500  stoweidlem7  40542  stoweidlem13  40548  stoweidlem26  40561  wallispilem3  40602  stirlinglem6  40614  stirlinglem10  40618  dirkercncf  40642  fourierdlem6  40648  fourierdlem11  40653  fourierdlem12  40654  fourierdlem15  40657  fourierdlem26  40668  fourierdlem42  40684  fourierdlem50  40691  fourierdlem51  40692  fourierdlem52  40693  fourierdlem54  40695  fourierdlem62  40703  fourierdlem79  40720  fourierdlem102  40743  fourierdlem114  40755  etransclem23  40792  zgeltp1eq  41643  setsnidel  41672  iccpartres  41679  pfx2  41737  pfxccatin12d  41757  repswpfx  41761  rabsubmgmd  42116  submgmid  42118  subsubmgm  42122  mgmhmima  42127  mgmhmeql  42128  isassintop  42171  rnghmsscmap2  42298  rnghmsscmap  42299  rnghmsubcsetc  42302  zrzeroorngc  42327  rhmsscmap2  42344  rhmsscmap  42345  rhmsubcsetc  42348  rhmsscrnghm  42351  rhmsubcrngc  42354  srhmsubc  42401  fldhmsubc  42409  rhmsubc  42415  srhmsubcALTV  42419  fldhmsubcALTV  42427  rhmsubcALTV  42433  rmfsupp  42480  mndpfsupp  42482  scmfsupp  42484  mptcfsupp  42486  lcoel0  42542  lincsumcl  42545  lincscmcl  42546  lcoss  42550  lindsrng01  42582  lincreslvec3  42596  lindssnlvec  42600  zgtp1leeq  42636
  Copyright terms: Public domain W3C validator