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  6263  fmptsng  6339  fmptsnd  6340  fnprb  6377  fntpb  6378  fdmfifsupp  8168  fczfsuppd  8176  fsuppmptif  8188  fsuppco2  8191  fsuppcor  8192  dffi3  8220  suppr  8260  infpr  8292  ordtypelem7  8312  cantnf0  8455  cantnfp1lem1  8458  cantnfp1lem2  8459  cantnfp1lem3  8460  cantnflem1a  8465  cantnflem1d  8468  cantnflem1  8469  cantnf  8473  rankpwi  8569  carduni  8690  fin23lem32  9049  fpwwe2lem6  9336  fpwwe2lem9  9339  fpwwe2lem12  9342  fpwwe2lem13  9343  fpwwe2  9344  inttsk  9475  grutsk1  9522  add20  10419  supaddc  10867  supadd  10868  supmul  10872  suprzcl  11333  uzwo3  11659  rpnnen1lem5  11694  rpnnen1lem5OLD  11700  xrre  11874  xrre3  11876  xleadd1a  11955  xlemul1a  11990  supxrre  12029  ixxub  12067  elioc2  12107  elico2  12108  elicc2  12109  elfz1eq  12223  fzadd2  12247  fznatpl1  12265  nn0fz0  12306  fzctr  12320  fzo1fzo0n0  12386  fzoaddel  12388  elincfzoext  12393  flid  12471  flval3  12478  fladdz  12488  fldiv  12521  modid  12557  seqf1olem1  12702  bcval5  12967  hashf1lem1  13096  eqs1  13245  wwlktovf1  13548  sqeqd  13754  sqrlem7  13837  max0add  13898  abs2difabs  13922  rddif  13928  fzomaxdiflem  13930  rexico  13941  icodiamlt  14022  limsupgre  14060  rlim3  14077  icco1  14119  rlimclim  14125  rlimuni  14129  rlimresb  14144  isercolllem2  14244  isercolllem3  14245  isercoll  14246  caucvgrlem  14251  caurcvgr  14252  iseraltlem3  14262  fsum00  14371  o1fsum  14386  bitsfzolem  14994  bitsfzo  14995  bitsmod  14996  bitscmp  14998  gcd0id  15078  gcdneg  15081  bezoutlem4  15097  nn0seqcvgd  15121  lcmneg  15154  qredeq  15209  prmind2  15236  isprm5  15257  hashdvds  15318  eulerthlem2  15325  pcpremul  15386  pcidlem  15414  pcgcd1  15419  pcadd2  15432  fldivp1  15439  pcfaclem  15440  prmreclem5  15462  4sqlem17  15503  vdwlem1  15523  vdwlem6  15528  vdwlem12  15534  vdwlem13  15535  0ram  15562  ram0  15564  ramub1lem1  15568  invco  16254  sectmon  16265  monsect  16266  invid  16270  cicref  16284  ssctr  16308  ssceq  16309  0ssc  16320  0subcat  16321  catsubcat  16322  issubc3  16332  fullsubc  16333  funcinv  16356  fthmon  16410  fuccocl  16447  fucidcl  16448  invfuc  16457  2initoinv  16483  2termoinv  16490  elhomai  16506  setcmon  16560  setcepi  16561  catcisolem  16579  curf2cl  16694  yonedalem4c  16740  yonedalem3  16743  yoniso  16748  lublecl  16812  isacs3lem  16989  tsrdir  17061  mnd1  17154  sgrp2nmndlem4  17238  sgrp2nmndlem5  17239  nmznsg  17461  ghmpreima  17505  ghmeql  17506  ghmnsgpreima  17508  cntzsubm  17591  cntzsubg  17592  cntzmhm  17594  symgextfo  17665  symgfixf1  17680  symgfixfolem1  17681  odlem2  17781  gexlem2  17820  gexcl2  17827  sylow1lem5  17840  subgslw  17854  slwhash  17862  fislw  17863  sylow3lem1  17865  lsmsubg  17892  efgredlemd  17980  efgredlem  17983  efgcpbllemb  17991  frgpuplem  18008  cyggeninv  18108  iscygd  18112  iscygodd  18113  gsumzadd  18145  gsumconst  18157  gsumpt  18184  gsum2dlem2  18193  gsum2d  18194  gsum2d2lem  18195  dprdfcntz  18237  eldprdi  18240  subgdmdprd  18256  subgdprd  18257  dprdpr  18272  ablfac1c  18293  ablfac1eu  18295  ablfaclem3  18309  ring1  18425  kerf1hrm  18566  issubdrg  18628  rhmeql  18633  rhmima  18634  cntzsubr  18635  isabvd  18643  abvdiv  18660  lsslsp  18836  lmhmima  18868  lmhmpreima  18869  lmhmeql  18876  lsmcl  18904  lspfixed  18949  issubassa  19145  issubassa2  19166  snifpsrbag  19187  psrbaglesupp  19189  psrbaglecl  19190  psrbagaddcl  19191  psrbagcon  19192  mplsubglem  19255  mpllsslem  19256  mplassa  19275  subrgmpl  19281  mplcoe5  19289  mplbas2  19291  mplind  19323  evlslem3  19335  mpfind  19357  ply1assa  19390  coe1tmmul2  19467  coe1tmmul  19468  cply1coe0bi  19491  qsssubdrg  19624  gzrngunit  19631  evpmodpmf1o  19761  ocvpj  19880  dsmm0cl  19903  dsmmacl  19904  dsmmsubg  19906  dsmmlss  19907  frlmsplit2  19931  uvcff  19949  lindfrn  19979  f1lindf  19980  lindsss  19982  mat1rngiso  20111  dmatid  20120  dmatsubcl  20123  dmatscmcl  20128  scmatid  20139  scmataddcl  20141  scmatsubcl  20142  scmatmulcl  20143  smatvscl  20149  scmatrhmcl  20153  scmatrngiso  20161  mat0scmat  20163  mat1scmat  20164  mdet0pr  20217  m2cpmrngiso  20382  pm2mprngiso  20446  chmaidscmat  20472  fvmptnn04if  20473  distop  20610  indistopon  20615  ppttop  20621  epttop  20623  mretopd  20706  toponmre  20707  neiss  20723  opnneissb  20728  ssnei2  20730  innei  20739  neiptoptop  20745  ordtcld1  20811  ordtcld2  20812  lmconst  20875  cnpnei  20878  iscncl  20883  cnss1  20890  cnss2  20891  cncnpi  20892  cncnp  20894  cnconst2  20897  cnrest  20899  cnpresti  20902  cnpdis  20907  paste  20908  lmcnp  20918  cnhaus  20968  hauscmp  21020  2ndcomap  21071  1stcelcls  21074  1stccnp  21075  llyrest  21098  nllyrest  21099  llyidm  21101  nllyidm  21102  ssref  21125  reftr  21127  refun0  21128  dissnref  21141  kgentopon  21151  kgenidm  21160  kgencn3  21171  txcld  21216  neitx  21220  tx1cn  21222  tx2cn  21223  ptcld  21226  xkoccn  21232  txcnp  21233  ptcnp  21235  txcnmpt  21237  ptcn  21240  txdis1cn  21248  ptrescn  21252  txkgen  21265  xkoco1cn  21270  xkoco2cn  21271  xkococn  21273  xkoinjcn  21300  qtoptop2  21312  qtopuni  21315  qtopid  21318  qtopkgen  21323  basqtop  21324  tgqtop  21325  qtopss  21328  qtopeu  21329  qtoprest  21330  kqopn  21347  kqcld  21348  kqreglem2  21355  reghmph  21406  ordthmeolem  21414  qtopf1  21429  opnfbas  21456  isfil2  21470  fbasweak  21479  fsubbas  21481  filcon  21497  fbasrn  21498  rnelfmlem  21566  flimss2  21586  flimss1  21587  hausflim  21595  flimclslem  21598  flimsncls  21600  cnpflfi  21613  flfcnp2  21621  fclsfnflim  21641  cnextfvval  21679  cnextfres1  21682  symgtgp  21715  opnsubg  21721  ghmcnp  21728  qustgpopn  21733  qustgplem  21734  qustgphaus  21736  tsmsfbas  21741  ustfilxp  21826  utoptop  21848  utopbas  21849  restutopopn  21852  iducn  21897  cstucnd  21898  ucncn  21899  fmucnd  21906  cfilufg  21907  trcfilu  21908  cfiluweak  21909  neipcfilu  21910  psmetsym  21925  psmetres2  21929  isxmetd  21941  xmetsym  21962  xmetpsmet  21963  imasf1oxmet  21990  xblss2ps  22016  xblss2  22017  xblcntrps  22025  xblcntr  22026  blcld  22120  metustfbas  22172  cfilucfil  22174  restmetu  22185  ngptgp  22250  tngngpd  22267  nrmtngnrm  22272  tngnrg  22288  nlmvscn  22301  nrginvrcn  22306  nmo0  22349  nmoeq0  22350  nmoid  22356  nghmcn  22359  0nmhm  22369  blcvx  22409  zcld  22424  iccntr  22432  xrge0tsms  22445  xmetdcn2  22448  metdstri  22462  metdscn  22467  rescncf  22508  cncfco  22518  oprpiece1res2  22559  cnheibor  22562  cnllycmp  22563  bndth  22565  evth  22566  ishtpyd  22582  isphtpyd  22593  pcoval2  22624  nmhmcn  22728  ipcn  22853  lmnn  22869  cfilss  22876  iscfil3  22879  cfilfcls  22880  cmetcaulem  22894  iscmet3lem2  22898  cfilres  22902  lmcau  22919  flimcfil  22920  cncmet  22927  rlmbn  22965  minveclem3b  23007  pjthlem1  23016  pjth2  23019  ivthlem3  23029  ovolssnul  23062  ovolctb  23065  ovolunnul  23075  ovoliunnul  23082  ovolsca  23090  ovolicc  23098  ovolicopnf  23099  voliunlem2  23126  voliunlem3  23127  volsup  23131  uniioovol  23153  uniiccvol  23154  dyadmaxlem  23171  vitalilem5  23187  ismbfd  23213  mbfres  23217  mbfss  23219  mbfmulc2re  23221  mbfadd  23234  mbfmulc2  23236  mbflim  23241  i1faddlem  23266  i1fmullem  23267  mbfmul  23299  itg2itg1  23309  itg2seq  23315  itg2eqa  23318  itg2mulc  23320  itg2split  23322  itg2mono  23326  itg2cnlem1  23334  ibl0  23359  iblposlem  23364  itgreval  23369  iblneg  23375  iblss  23377  iblss2  23378  itgle  23382  iblconst  23390  iblabs  23401  iblabsr  23402  iblmulc2  23403  bddmulibl  23411  limciun  23464  limcun  23465  dvres2lem  23480  dvidlem  23485  dvcnp2  23489  dvcn  23490  cpnres  23506  dvaddbr  23507  dvmulbr  23508  dvcobr  23515  dvcjbr  23518  dvrec  23524  dvcnvlem  23543  dvferm  23555  dvlip2  23562  dveq0  23567  dv11cn  23568  dvivthlem1  23575  lhop1  23581  lhop2  23582  lhop  23583  dvcnvre  23586  dvfsumlem3  23595  dvfsumlem4  23596  dvfsumrlim  23598  dvfsum2  23601  ftc1a  23604  ftc1lem4  23606  ftc1lem6  23608  ftc1  23609  coe1mul3  23663  deg1addle2  23666  deg1add  23667  deg1sublt  23674  deg1mul2  23678  deg1tm  23682  fta1blem  23732  drnguc1p  23734  ig1prsp  23741  plyco0  23752  plyeq0lem  23770  dgrub  23794  dgreq  23804  dgradd2  23828  dgrmul  23830  dgrcolem2  23834  dgrco  23835  plycpn  23848  plydivlem4  23855  plydiveu  23857  vieta1lem2  23870  vieta1  23871  aalioulem2  23892  aalioulem3  23893  aaliou3lem7  23908  tayl0  23920  ulmcn  23957  ulmdvlem3  23960  psercn  23984  abelth  23999  pilem3  24011  efif1olem1  24092  abslogimle  24124  argregt0  24160  argrege0  24161  logf1o2  24196  cxpsqrtlem  24248  cxpcn3  24289  abscxpbnd  24294  logreclem  24300  ang180lem2  24340  ang180lem3  24341  xrlimcnp  24495  harmonicbnd4  24537  fsumharmonic  24538  lgamgulmlem5  24559  lgambdd  24563  basellem3  24609  basellem4  24610  dvdsppwf1o  24712  dvdsflf1o  24713  fsumfldivdiaglem  24715  chpeq0  24733  chteq0  24734  chtub  24737  chpub  24745  dchrelbasd  24764  dchrmulcl  24774  dchrinv  24786  bcmono  24802  bposlem1  24809  bposlem2  24810  lgslem1  24822  lgsdirprm  24856  lgsqrlem2  24872  lgsqrlem3  24873  lgsdchr  24880  lgseisenlem1  24900  lgseisenlem2  24901  lgseisenlem3  24902  lgsquadlem1  24905  2sqlem8  24951  2sqblem  24956  chebbnd1lem1  24958  dchrisumlem1  24978  dchrisumlem2  24979  dchrisumlem3  24980  dchrisum0fno1  25000  pntrmax  25053  pntpbnd1a  25074  pntibndlem3  25081  pntlemn  25089  pntlemi  25093  pntlem3  25098  pntleml  25100  ostth1  25122  ostth2  25126  ostth3  25127  ercgrg  25212  motco  25235  cnvmot  25236  legso  25294  mirmot  25370  lmicom  25480  lmimid  25486  lmimot  25490  hypcgrlem1  25491  hypcgrlem2  25492  ttgcontlem1  25565  brbtwn2  25585  axlowdimlem3  25624  axlowdimlem16  25637  axcontlem8  25651  cusgra0v  25989  cusgraexi  25997  cusgrares  26001  uvtxnb  26025  1pthon  26121  constr2spth  26130  2pthon  26132  usgra2wlkspthlem2  26148  usgra2wlkspth  26149  constr3trllem3  26180  constr3cycl  26189  wlklniswwlkn1  26227  vfwlkniswwlkn  26234  usg2wlkeq2  26237  wwlknred  26251  wwlknredwwlkn0  26255  clwlkisclwwlklem2a1  26307  clwwlkel  26321  wwlkext2clwwlk  26331  clwwnisshclwwn  26337  clwlkf1clwwlk  26377  0egra0rgra  26463  0vgrargra  26464  eupares  26502  eupap1  26503  frgra0v  26520  frgra1v  26525  nvabs  26911  vacn  26933  nmcvcn  26934  nmblore  27025  0lno  27029  0blo  27031  nmlno0lem  27032  occl  27547  pjhthlem1  27634  pjpjpre  27662  nmopre  28113  nmlnop0iALT  28238  nmophmi  28274  leoprf2  28370  stlesi  28484  disjdifprg  28770  disjun0  28790  fpwrelmap  28896  fzspl  28938  2sqmod  28979  ogrpaddlt  29049  ogrpsublt  29053  pnfinf  29068  xrge0tsmsd  29116  ornglmullt  29138  orngrmullt  29139  orngmullt  29140  ofldlt1  29144  isarchiofld  29148  psgnfzto1stlem  29181  fzto1st1  29183  qtopt1  29230  reff  29234  locfinreflem  29235  metideq  29264  metider  29265  pstmxmet  29268  qqhval2lem  29353  qqhcn  29363  qqhucn  29364  pwsiga  29520  prsiga  29521  measle0  29598  mbfmcst  29648  1stmbfm  29649  2ndmbfm  29650  imambfm  29651  cnmbfm  29652  mbfmco  29653  mbfmco2  29654  0elcarsg  29696  carsgclctun  29710  sibfof  29729  oddpwdc  29743  eulerpartlemmf  29764  eulerpartlemgs2  29769  0rrv  29840  ballotlemfc0  29881  ballotlemfcc  29882  signstfveq0  29980  bnj1452  30374  derangen  30408  subfacval3  30425  cvmseu  30512  cvmliftmolem2  30518  cvmliftlem7  30527  cvmliftlem15  30534  cvmlift2lem9a  30539  cvmlift2lem9  30547  cvmlift2lem10  30548  cvmlift2lem11  30549  cvmlift2lem12  30550  cvmlift3lem6  30560  cvmlift3lem8  30562  mclsppslem  30734  mclspps  30735  wsuclem  31017  wsuclemOLD  31018  nosepon  31066  fness  31514  fnetr  31516  fnessref  31522  refssfne  31523  neibastop1  31524  neibastop2  31526  tailfb  31542  filnetlem3  31545  bj-finsumval0  32324  poimirlem13  32592  poimirlem15  32594  poimirlem17  32596  poimirlem24  32603  poimirlem28  32607  mblfinlem2  32617  ovoliunnfl  32621  volsupnfl  32624  mbfresfi  32626  itg2addnclem2  32632  iblabsnc  32644  iblmulc2nc  32645  ftc1cnnclem  32653  ftc1cnnc  32654  ftc1anc  32663  sdclem2  32708  metf1o  32721  ismtyhmeolem  32773  ismtyres  32777  heibor1lem  32778  bfplem2  32792  bfp  32793  rrncmslem  32801  iccbnd  32809  icccmpALT  32810  rngogrphom  32940  rngoisoco  32951  keridl  33001  lsmcv2  33334  lsatcv0  33336  lcvexchlem4  33342  lcvexchlem5  33343  l1cvpat  33359  lfl0f  33374  lfladdcl  33376  lflnegcl  33380  lkrlss  33400  eqlkr  33404  lkrlsp  33407  lkrlsp2  33408  lshpkrcl  33421  lkrin  33469  1cvrjat  33779  llni  33812  llnle  33822  lplni  33836  lplnle  33844  llncvrlpln2  33861  2atmat  33865  lvoli  33879  lplncvrlvol2  33919  elpaddri  34106  paddclN  34146  pclclN  34195  pclfinN  34204  0psubclN  34247  1psubclN  34248  atpsubclN  34249  pmapsubclN  34250  osumclN  34271  pexmidN  34273  pexmidlem6N  34279  lhp2lt  34305  lautcnv  34394  idlaut  34400  lautco  34401  idldil  34418  ldilcnv  34419  ldilco  34420  ltrncnv  34450  idltrn  34454  cdleme16d  34586  cdleme50laut  34853  cdleme50ldil  34854  cdleme50ltrn  34863  ltrnco  35025  dian0  35346  dia0eldmN  35347  dia1eldmN  35348  dialss  35353  diaintclN  35365  docaclN  35431  doca2N  35433  djajN  35444  dibintclN  35474  diblss  35477  dicvaddcl  35497  dicvscacl  35498  dicn0  35499  cdlemn11a  35514  dihord2cN  35528  dihord11b  35529  dihord6apre  35563  dihmeetlem1N  35597  dihglblem5apreN  35598  dihpN  35643  dihjatcclem4  35728  dochkr1  35785  islpoldN  35791  lcfrlem31  35880  mapdpglem18  35996  mapdheq2  36036  mapdheq4  36039  mapdh6aN  36042  hdmap1l6a  36117  hdmap1neglem1N  36135  hdmap14lem4a  36181  fzsplit1nn0  36335  irrapxlem3  36406  irrapxlem4  36407  pell1234qrdich  36443  pell1qr1  36453  pell14qrgap  36457  pellqrexplicit  36459  rmspecfund  36492  fzmaxdif  36566  acongeq  36568  jm2.23  36581  jm3.1  36605  lmhmlnmsplit  36675  hbt  36719  dgrsub2  36724  proot1ex  36798  clublem  36936  dftrcl3  37031  hashnzfz2  37542  dvconstbi  37555  ubelsupr  38202  lefldiveq  38446  iccintsng  38596  fmul01  38647  fmuldfeq  38650  climsuse  38675  mullimc  38683  limcdm0  38685  limccog  38687  mullimcf  38690  constlimc  38691  idlimc  38693  limcperiod  38695  limsupre  38708  limcleqr  38711  neglimc  38714  addlimc  38715  0ellimcdiv  38716  cncfshift  38759  cncfperiod  38764  cncfuni  38772  icccncfext  38773  cncfiooicclem1  38779  fperdvper  38808  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  mbfres2cn  38850  iblsplit  38858  stoweidlem7  38900  stoweidlem13  38906  stoweidlem26  38919  wallispilem3  38960  stirlinglem6  38972  stirlinglem10  38976  dirkercncf  39000  fourierdlem6  39006  fourierdlem11  39011  fourierdlem12  39012  fourierdlem15  39015  fourierdlem26  39026  fourierdlem42  39042  fourierdlem50  39049  fourierdlem51  39050  fourierdlem52  39051  fourierdlem54  39053  fourierdlem62  39061  fourierdlem79  39078  fourierdlem102  39101  fourierdlem114  39113  etransclem23  39150  zgeltp1eq  39943  iccpartres  39956  pfx2  40275  pfxccatin12d  40295  repswpfx  40299  fusgrfis  40549  nbgr2vtx1edg  40572  uvtxnbgrb  40628  cplgr1v  40652  0vtxrgr  40776  0vtxrusgr  40777  ewlkle  40807  1wlk1ewlk  40844  uspgr2wlkeq2  40855  1wlkp1lem8  40889  trlres  40908  trlOntrl  40918  pthOnpth  40954  uhgr1wlkspth  40961  usgr2wlkspth  40965  pthdlem2  40974  crctcshtrl  41026  1wlklnwwlkln1  41065  wlknewwlksn  41084  wwlksnred  41098  wwlksnredwwlkn0  41102  2trld  41145  2trlond  41146  2spthd  41148  2pthond  41149  elwwlks2ons3  41159  clwlkclwwlklem2a1  41201  clwwlksel  41221  wwlksext2clwwlk  41231  clwwnisshclwwsn  41237  clwlksf1clwwlk  41276  0TrlOn  41292  0pthon-av  41295  1trld  41309  1pthond  41311  lp1cycl  41319  3trld  41339  3trlond  41340  3pthond  41342  3spthd  41343  3spthond  41344  3cycld  41345  eupthres  41383  eupthp1  41384  eupth2eucrct  41385  frgrregorufrg  41505  rabsubmgmd  41581  submgmid  41583  subsubmgm  41587  mgmhmima  41592  mgmhmeql  41593  isassintop  41636  rnghmsscmap2  41765  rnghmsscmap  41766  rnghmsubcsetc  41769  zrzeroorngc  41794  rhmsscmap2  41811  rhmsscmap  41812  rhmsubcsetc  41815  rhmsscrnghm  41818  rhmsubcrngc  41821  srhmsubc  41868  fldhmsubc  41876  rhmsubc  41882  srhmsubcALTV  41887  fldhmsubcALTV  41895  rhmsubcALTV  41901  rmfsupp  41949  mndpfsupp  41951  scmfsupp  41953  mptcfsupp  41955  lcoel0  42011  lincsumcl  42014  lincscmcl  42015  lcoss  42019  lindsrng01  42051  lincreslvec3  42065  lindssnlvec  42069  zgtp1leeq  42105
  Copyright terms: Public domain W3C validator