Theorem mpbir2and 713

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

Step	Hyp	Ref	Expression
1		mpbir2and.1	. . 3 ⊢ (𝜑 → 𝜒)
2		mpbir2and.2	. . 3 ⊢ (𝜑 → 𝜃)
3	1, 2	jca 515	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃))
4		mpbir2and.3	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))
5	3, 4	mpbird 260	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  elpreimad  6879  fveqressseq  6900  fmptsng  6983  fmptsnd  6984  fnprb  7024  fntpb  7025  fpr3g  8026  frrlem4  8030  fdmfifsupp  8995  fczfsuppd  9003  fsuppmptif  9015  fsuppco2  9019  fsuppcor  9020  dffi3  9047  suppr  9087  infpr  9119  ordtypelem7  9140  cantnf0  9290  cantnfp1lem1  9293  cantnfp1lem2  9294  cantnfp1lem3  9295  cantnflem1a  9300  cantnflem1d  9303  cantnflem1  9304  cantnf  9308  rankpwi  9439  carduni  9597  fin23lem32  9958  fpwwe2lem5  10249  fpwwe2lem11  10255  fpwwe2lem12  10256  fpwwe2  10257  inttsk  10388  grutsk1  10435  add20  11344  supaddc  11799  supadd  11800  supmul  11804  suprzcl  12257  uzid  12453  uzwo3  12539  rpnnen1lem5  12577  xrletrid  12745  xrre  12759  xrre3  12761  xleadd1a  12843  xlemul1a  12878  elioc2  12998  elico2  12999  elicc2  13000  elfz1eq  13123  fzadd2  13147  fznatpl1  13166  elfz1uz  13182  nn0fz0  13210  fzctr  13224  fzo1fzo0n0  13293  fzoaddel  13295  elincfzoext  13300  flid  13383  flval3  13390  fladdz  13400  fldiv  13433  modid  13469  hashf1lem1  14020  hashf1lem1OLD  14021  pfxccatin12d  14310  repswpfx  14350  2cshw  14378  pfx2  14512  wwlktovf1  14524  sqeqd  14729  sqrlem7  14812  max0add  14874  abs2difabs  14898  rddif  14904  fzomaxdiflem  14906  rexico  14917  icodiamlt  14999  limsupgre  15042  rlim3  15059  icco1  15101  rlimclim  15107  rlimuni  15111  rlimresb  15126  isercolllem2  15229  isercolllem3  15230  isercoll  15231  caucvgrlem  15236  caurcvgr  15237  iseraltlem3  15247  fsum00  15362  o1fsum  15377  bitsfzolem  15993  bitsfzo  15994  bitsmod  15995  bitscmp  15997  gcd0id  16078  gcdneg  16081  bezoutlem4  16102  nn0seqcvgd  16127  lcmneg  16160  lcmfunsnlem2lem2  16196  qredeq  16214  prmind2  16242  eulerthlem2  16335  pcpremul  16396  pcidlem  16425  pcgcd1  16430  fldivp1  16450  pcfaclem  16451  4sqlem17  16514  vdwlem1  16534  vdwlem6  16539  vdwlem12  16545  vdwlem13  16546  0ram  16573  ram0  16575  ramub1lem1  16579  invco  17276  sectmon  17287  monsect  17288  invid  17292  ssctr  17330  ssceq  17331  0ssc  17343  0subcat  17344  catsubcat  17345  issubc3  17355  fullsubc  17356  funcinv  17379  fthmon  17434  fuccocl  17473  fucidcl  17474  invfuc  17483  2initoinv  17516  2termoinv  17523  elhomai  17539  setcmon  17593  setcepi  17594  catcisolem  17616  curf2cl  17739  yonedalem4c  17785  yonedalem3  17788  yoniso  17793  lublecl  17867  isacs3lem  18048  tsrdir  18110  mnd1  18214  sgrp2nmndlem4  18355  sgrp2nmndlem5  18356  nmznsg  18584  ghmpreima  18644  ghmeql  18645  ghmnsgpreima  18647  cntzsubm  18730  cntzsubg  18731  cntzmhm  18733  symgextfo  18814  symgfixf1  18829  symgfixfolem1  18830  odlem2  18931  gexlem2  18971  gexcl2  18978  sylow1lem5  18991  subgslw  19005  slwhash  19013  fislw  19014  sylow3lem1  19016  lsmsubg  19043  efgredlemd  19134  efgredlem  19137  efgcpbllemb  19145  frgpuplem  19162  cyggeninv  19267  iscygd  19271  iscygodd  19272  gsumzadd  19307  gsumconst  19319  gsumpt  19347  gsum2dlem2  19356  gsum2d  19357  gsum2d2lem  19358  dprdfcntz  19402  eldprdi  19405  subgdmdprd  19421  subgdprd  19422  dprdpr  19437  ablfac1c  19458  ablfac1eu  19460  ablfaclem3  19474  ring1  19620  kerf1ghm  19763  issubdrg  19825  rhmeql  19830  rhmima  19831  cntzsubr  19833  isabvd  19856  abvdiv  19873  lsslsp  20052  lmhmima  20084  lmhmpreima  20085  lmhmeql  20092  lsmcl  20120  lspfixed  20165  qsssubdrg  20422  gzrngunit  20429  evpmodpmf1o  20558  ocvpj  20679  dsmm0cl  20702  dsmmacl  20703  dsmmsubg  20705  dsmmlss  20706  frlmsplit2  20735  uvcff  20753  lindfrn  20783  f1lindf  20784  lindsss  20786  issubassa  20828  issubassa2  20852  snifpsrbag  20881  psrbaglesupp  20883  psrbaglesuppOLD  20884  psrbaglecl  20885  psrbagleclOLD  20886  psrbagaddcl  20887  psrbagaddclOLD  20888  psrbagcon  20889  psrbagconOLD  20890  mplsubglem  20961  mpllsslem  20962  mplassa  20983  subrgmpl  20989  mplcoe5  20997  mplbas2  20999  mplind  21028  mpfind  21067  ismhp2  21082  mhpmulcl  21089  mhplss  21095  ply1assa  21120  coe1tmmul2  21197  coe1tmmul  21198  cply1coe0bi  21221  mat1rngiso  21383  dmatid  21392  dmatsubcl  21395  dmatscmcl  21400  scmatid  21411  scmataddcl  21413  scmatsubcl  21414  scmatmulcl  21415  smatvscl  21421  scmatrhmcl  21425  scmatrngiso  21433  mat0scmat  21435  mat1scmat  21436  mdet0pr  21489  m2cpmrngiso  21655  pm2mprngiso  21719  chmaidscmat  21745  distop  21892  indistopon  21898  ppttop  21904  epttop  21906  mretopd  21989  toponmre  21990  neiss  22006  opnneissb  22011  ssnei2  22013  innei  22022  neiptoptop  22028  ordtcld1  22094  ordtcld2  22095  lmconst  22158  cnpnei  22161  iscncl  22166  cnss1  22173  cnss2  22174  cncnpi  22175  cncnp  22177  cnconst2  22180  cnrest  22182  cnpresti  22185  cnpdis  22190  paste  22191  lmcnp  22201  cnhaus  22251  hauscmp  22304  2ndcomap  22355  1stcelcls  22358  1stccnp  22359  llyrest  22382  nllyrest  22383  llyidm  22385  nllyidm  22386  ssref  22409  reftr  22411  refun0  22412  dissnref  22425  kgentopon  22435  kgenidm  22444  kgencn3  22455  txcld  22500  neitx  22504  tx1cn  22506  tx2cn  22507  ptcld  22510  xkoccn  22516  txcnp  22517  ptcnp  22519  txcnmpt  22521  ptcn  22524  txdis1cn  22532  ptrescn  22536  txkgen  22549  xkoco1cn  22554  xkoco2cn  22555  xkococn  22557  xkoinjcn  22584  qtoptop2  22596  qtopuni  22599  qtopid  22602  qtopkgen  22607  basqtop  22608  tgqtop  22609  qtopss  22612  qtopeu  22613  qtoprest  22614  kqopn  22631  kqcld  22632  kqreglem2  22639  reghmph  22690  ordthmeolem  22698  qtopf1  22713  opnfbas  22739  isfil2  22753  fbasweak  22762  fsubbas  22764  filconn  22780  fbasrn  22781  rnelfmlem  22849  flimss2  22869  flimss1  22870  hausflim  22878  flimclslem  22881  flimsncls  22883  cnpflfi  22896  flfcnp2  22904  fclsfnflim  22924  cnextfvval  22962  cnextfres1  22965  symgtgp  23003  opnsubg  23005  ghmcnp  23012  qustgpopn  23017  qustgplem  23018  qustgphaus  23020  tsmsfbas  23025  ustfilxp  23110  utoptop  23132  utopbas  23133  restutopopn  23136  iducn  23180  cstucnd  23181  ucncn  23182  fmucnd  23189  cfilufg  23190  trcfilu  23191  cfiluweak  23192  neipcfilu  23193  psmetres2  23212  isxmetd  23224  xmetpsmet  23246  imasf1oxmet  23273  xblss2ps  23299  xblss2  23300  xblcntrps  23308  xblcntr  23309  blcld  23403  metustfbas  23455  cfilucfil  23457  restmetu  23468  ngptgp  23534  tngngpd  23551  nrmtngnrm  23556  tngnrg  23572  nlmvscn  23585  nrginvrcn  23590  nmo0  23633  nmoeq0  23634  nmoid  23640  nghmcn  23643  0nmhm  23653  blcvx  23695  iccntr  23718  xrge0tsms  23731  xmetdcn2  23734  metdstri  23748  metdscn  23753  rescncf  23794  cncfco  23804  oprpiece1res2  23849  cnheibor  23852  cnllycmp  23853  bndth  23855  ishtpyd  23872  isphtpyd  23883  pcoval2  23913  nmhmcn  24017  ipcn  24143  lmnn  24160  cfilss  24167  iscfil3  24170  cfilfcls  24171  cmetcaulem  24185  iscmet3lem2  24189  cfilres  24193  lmcau  24210  flimcfil  24211  cncmet  24219  rlmbn  24258  minveclem3b  24325  pjthlem1  24334  pjth2  24337  ivthlem3  24350  ovolssnul  24384  ovolctb  24387  ovoliunnul  24404  ovolsca  24412  ovolicopnf  24421  voliunlem2  24448  volsup  24453  dyadmaxlem  24494  vitalilem5  24509  mbfres  24541  mbfss  24543  mbfmulc2re  24545  mbfadd  24558  mbfmulc2  24560  mbflim  24565  i1faddlem  24590  i1fmullem  24591  mbfmul  24624  itg2mulc  24645  itg2cnlem1  24659  ibl0  24684  iblposlem  24689  itgreval  24694  iblneg  24700  iblss  24702  iblss2  24703  itgle  24707  iblconst  24715  iblabs  24726  iblabsr  24727  iblmulc2  24728  bddmulibl  24736  limciun  24791  limcun  24792  dvres2lem  24807  dvidlem  24812  dvcnp2  24817  dvcn  24818  cpnres  24834  dvaddbr  24835  dvmulbr  24836  dvcobr  24843  dvcjbr  24846  dvrec  24852  dvcnvlem  24873  dvferm  24885  dvlip2  24892  dveq0  24897  dv11cn  24898  dvivthlem1  24905  lhop1  24911  lhop2  24912  lhop  24913  dvcnvre  24916  dvfsumlem3  24925  dvfsumlem4  24926  dvfsumrlim  24928  dvfsum2  24931  ftc1a  24934  ftc1lem4  24936  ftc1lem6  24938  ftc1  24939  coe1mul3  24997  deg1addle2  25000  deg1sublt  25008  fta1blem  25066  drnguc1p  25068  ig1prsp  25075  plyco0  25086  plyeq0lem  25104  dgrub  25128  dgreq  25138  dgradd2  25162  dgrmul  25164  dgrcolem2  25168  dgrco  25169  plycpn  25182  plydivlem4  25189  plydiveu  25191  vieta1lem2  25204  vieta1  25205  aalioulem2  25226  aalioulem3  25227  aaliou3lem7  25242  tayl0  25254  ulmcn  25291  ulmdvlem3  25294  psercn  25318  abelth  25333  pilem3  25345  efif1olem1  25431  abslogimle  25462  argregt0  25498  argrege0  25499  logf1o2  25538  cxpsqrtlem  25590  cxpcn3  25634  abscxpbnd  25639  logreclem  25645  ang180lem2  25693  ang180lem3  25694  xrlimcnp  25851  harmonicbnd4  25893  fsumharmonic  25894  lgamgulmlem5  25915  lgambdd  25919  basellem4  25966  dvdsppwf1o  26068  dvdsflf1o  26069  fsumfldivdiaglem  26071  chpeq0  26089  chteq0  26090  chtub  26093  chpub  26101  dchrelbasd  26120  dchrmulcl  26130  dchrinv  26142  bposlem1  26165  bposlem2  26166  lgsdirprm  26212  lgsqrlem2  26228  lgsqrlem3  26229  lgsdchr  26236  lgseisenlem1  26256  lgseisenlem2  26257  lgseisenlem3  26258  lgsquadlem1  26261  2sqlem8  26307  2sqblem  26312  2sqmod  26317  chebbnd1lem1  26350  dchrisumlem1  26370  dchrisumlem2  26371  dchrisumlem3  26372  dchrisum0fno1  26392  pntrmax  26445  pntpbnd1a  26466  pntibndlem3  26473  pntlemn  26481  pntlemi  26485  pntlem3  26490  pntleml  26492  ostth1  26514  ostth2  26518  ostth3  26519  ercgrg  26608  motco  26631  cnvmot  26632  legso  26690  mirmot  26766  colopp  26860  hphl  26862  lmicom  26879  lmimid  26885  lmimot  26889  hypcgrlem1  26890  hypcgrlem2  26891  trgcopyeulem  26896  inagswap  26932  inaghl  26936  cgrg3col4  26944  brbtwn2  26996  axlowdimlem3  27035  axlowdimlem16  27048  axcontlem8  27062  fusgrfis  27418  nbgr2vtx1edg  27438  0vtxrgr  27664  0vtxrusgr  27665  ewlkle  27693  wlk1ewlk  27727  uspgr2wlkeq2  27734  wlkp1lem8  27768  trlontrl  27798  pthonpth  27835  pthdlem2  27855  wlklnwwlkln1  27952  wlknewwlksn  27971  wwlksnred  27976  wwlksnredwwlkn0  27980  2trlond  28023  2pthond  28026  elwwlks2ons3im  28038  clwlkclwwlklem2a1  28075  clwlkclwwlkf1  28093  clwwlkel  28129  clwwlkwwlksb  28137  wwlksext2clwwlk  28140  1ewlk  28198  0trlon  28207  0pthon  28210  1pthond  28227  3trlond  28256  3pthond  28258  3spthond  28260  eupthres  28298  2clwwlk2clwwlk  28433  numclwwlk1lem2foa  28437  numclwwlk1lem2f1  28440  nvabs  28753  vacn  28775  nmcvcn  28776  nmblore  28867  0lno  28871  0blo  28873  nmlno0lem  28874  occl  29385  pjhthlem1  29472  pjpjpre  29500  nmopre  29951  nmlnop0iALT  30076  nmophmi  30112  leoprf2  30208  stlesi  30322  disjdifprg  30633  disjun0  30653  fsuppcurry1  30780  fsuppcurry2  30781  fpwrelmap  30788  fzspl  30831  dfmgc2lem  30992  pwrssmgc  30997  xrge0tsmsd  31036  ogrpaddlt  31062  ogrpsublt  31066  psgnfzto1stlem  31086  fzto1st1  31088  evpmid  31134  pnfinf  31156  rmfsupp2  31211  ornglmullt  31225  orngrmullt  31226  orngmullt  31227  ofldlt1  31231  isarchiofld  31235  nsgmgc  31311  lbsdiflsp0  31421  fedgmul  31426  fldexttr  31447  fldextid  31448  qtopt1  31499  reff  31503  locfinreflem  31504  metideq  31557  metider  31558  pstmxmet  31561  qqhval2lem  31643  qqhcn  31653  qqhucn  31654  pwsiga  31810  prsiga  31811  measle0  31888  mbfmcst  31938  1stmbfm  31939  2ndmbfm  31940  imambfm  31941  cnmbfm  31942  mbfmco  31943  mbfmco2  31944  0elcarsg  31986  carsgclctun  32000  sibfof  32019  oddpwdc  32033  eulerpartlemmf  32054  eulerpartlemgs2  32059  0rrv  32130  ballotlemfc0  32171  ballotlemfcc  32172  signstfveq0  32268  breprexplemc  32324  bnj1452  32745  usgrgt2cycl  32805  acycgr1v  32824  derangen  32847  subfacval3  32864  cvmseu  32951  cvmliftmolem2  32957  cvmliftlem7  32966  cvmliftlem15  32973  cvmlift2lem9a  32978  cvmlift2lem9  32986  cvmlift2lem10  32987  cvmlift2lem11  32988  cvmlift2lem12  32989  cvmlift3lem6  32999  cvmlift3lem8  33001  ex-sategoelel  33096  ex-sategoelelomsuc  33101  mclsppslem  33258  mclspps  33259  wsuclem  33556  nosepon  33605  nolesgn2ores  33612  nogesgn1ores  33614  nosupres  33647  nosupbnd1lem2  33649  nosupbnd2lem1  33655  noinfres  33662  noinfbnd1lem2  33664  noinfbnd2lem1  33670  cofcutrtime  33830  fness  34275  fnetr  34277  fnessref  34283  refssfne  34284  neibastop1  34285  neibastop2  34287  tailfb  34303  filnetlem3  34306  bj-finsumval0  35191  bj-rvecvec  35204  dfgcd3  35229  lindsadd  35507  poimirlem13  35527  poimirlem15  35529  poimirlem24  35538  poimirlem28  35542  mblfinlem2  35552  ovoliunnfl  35556  volsupnfl  35559  mbfresfi  35560  iblabsnc  35578  iblmulc2nc  35579  ftc1cnnclem  35585  ftc1cnnc  35586  ftc1anc  35595  sdclem2  35637  metf1o  35650  ismtyhmeolem  35699  ismtyres  35703  heibor1lem  35704  bfplem2  35718  bfp  35719  rrncmslem  35727  iccbnd  35735  icccmpALT  35736  rngogrphom  35866  rngoisoco  35877  keridl  35927  lsmcv2  36780  lsatcv0  36782  lcvexchlem4  36788  lcvexchlem5  36789  l1cvpat  36805  lfl0f  36820  lfladdcl  36822  lflnegcl  36826  lkrlss  36846  eqlkr  36850  lkrlsp  36853  lkrlsp2  36854  lshpkrcl  36867  lkrin  36915  1cvrjat  37226  llni  37259  llnle  37269  lplni  37283  lplnle  37291  llncvrlpln2  37308  2atmat  37312  lvoli  37326  lplncvrlvol2  37366  elpaddri  37553  paddclN  37593  pclclN  37642  pclfinN  37651  0psubclN  37694  1psubclN  37695  atpsubclN  37696  pmapsubclN  37697  osumclN  37718  pexmidN  37720  pexmidlem6N  37726  lhp2lt  37752  lautcnv  37841  idlaut  37847  lautco  37848  idldil  37865  ldilcnv  37866  ldilco  37867  ltrncnv  37897  idltrn  37901  cdleme16d  38032  cdleme50laut  38298  cdleme50ldil  38299  cdleme50ltrn  38308  ltrnco  38470  dian0  38790  dia0eldmN  38791  dia1eldmN  38792  dialss  38797  diaintclN  38809  docaclN  38875  doca2N  38877  djajN  38888  dibintclN  38918  diblss  38921  dicvaddcl  38941  dicvscacl  38942  dicn0  38943  cdlemn11a  38958  dihord2cN  38972  dihord11b  38973  dihord6apre  39007  dihmeetlem1N  39041  dihglblem5apreN  39042  dihpN  39087  dihjatcclem4  39172  dochkr1  39229  islpoldN  39235  lcfrlem31  39324  mapdpglem18  39440  mapdheq2  39480  mapdheq4  39483  mapdh6aN  39486  hdmap1l6a  39560  hdmap14lem4a  39622  lcmineqlem4  39774  isfsuppd  39930  frlmfzoccat  39949  drnginvmuld  39967  fsuppind  39989  fsuppssind  39992  prjspvs  40157  irrapxlem4  40350  pell1234qrdich  40386  pell1qr1  40396  pell14qrgap  40400  pellqrexplicit  40402  rmspecfund  40434  fzmaxdif  40506  acongeq  40508  jm2.23  40521  jm3.1  40545  lmhmlnmsplit  40615  hbt  40658  dgrsub2  40663  proot1ex  40729  clublem  40894  dftrcl3  41005  mnugrud  41575  hashnzfz2  41612  dvconstbi  41625  ubelsupr  42236  wessf1ornlem  42395  lefldiveq  42504  iccintsng  42736  climsuse  42824  mullimc  42832  limcdm0  42834  limccog  42836  mullimcf  42839  constlimc  42840  idlimc  42842  limcperiod  42844  limsupre  42857  limcleqr  42860  neglimc  42863  addlimc  42864  0ellimcdiv  42865  xlimliminflimsup  43078  cncfshift  43090  cncfperiod  43095  cncfuni  43102  icccncfext  43103  cncfiooicclem1  43109  fperdvper  43135  ioodvbdlimc1lem2  43148  ioodvbdlimc2lem  43150  mbfres2cn  43174  iblsplit  43182  stoweidlem7  43223  stoweidlem13  43229  stoweidlem26  43242  wallispilem3  43283  stirlinglem6  43295  stirlinglem10  43299  dirkercncf  43323  fourierdlem6  43329  fourierdlem11  43334  fourierdlem12  43335  fourierdlem15  43338  fourierdlem26  43349  fourierdlem42  43365  fourierdlem50  43372  fourierdlem51  43373  fourierdlem52  43374  fourierdlem54  43376  fourierdlem62  43384  fourierdlem79  43401  fourierdlem102  43424  fourierdlem114  43436  etransclem23  43473  zgeltp1eq  44474  setsnidel  44502  preimafvsnel  44504  iccpartres  44543  prpair  44626  fpprel2  44866  rabsubmgmd  45018  submgmid  45020  subsubmgm  45024  mgmhmima  45029  mgmhmeql  45030  isassintop  45077  rnghmsscmap2  45204  rnghmsscmap  45205  rnghmsubcsetc  45208  zrzeroorngc  45233  rhmsscmap2  45250  rhmsscmap  45251  rhmsubcsetc  45254  rhmsscrnghm  45257  rhmsubcrngc  45260  srhmsubc  45307  fldhmsubc  45315  rhmsubc  45321  srhmsubcALTV  45325  fldhmsubcALTV  45333  rhmsubcALTV  45339  rmfsupp  45383  mndpfsupp  45385  scmfsupp  45387  mptcfsupp  45389  lcoel0  45442  lincsumcl  45445  lincscmcl  45446  lcoss  45450  lindsrng01  45482  lincreslvec3  45496  lindssnlvec  45500  zgtp1leeq  45535  lubsscl  45927  glbsscl  45928  idmon  45970  idepi  45971  thinciso  46014