Theorem mpbir2and 711

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 513	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃))
4		mpbir2and.3	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))
5	3, 4	mpbird 257	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  elpreimad  6968  fveqressseq  6989  fmptsng  7072  fmptsnd  7073  fnprb  7116  fntpb  7117  fpr3g  8132  frrlem4  8136  1ellim  8359  fdmfifsupp  9182  fczfsuppd  9190  fsuppmptif  9202  fsuppco2  9206  fsuppcor  9207  dffi3  9234  suppr  9274  infpr  9306  ordtypelem7  9327  cantnf0  9477  cantnfp1lem1  9480  cantnfp1lem2  9481  cantnfp1lem3  9482  cantnflem1a  9487  cantnflem1d  9490  cantnflem1  9491  cantnf  9495  rankpwi  9625  carduni  9783  fin23lem32  10146  fpwwe2lem5  10437  fpwwe2lem11  10443  fpwwe2lem12  10444  fpwwe2  10445  inttsk  10576  grutsk1  10623  add20  11533  supaddc  11988  supadd  11989  supmul  11993  suprzcl  12446  uzid  12643  uzwo3  12729  rpnnen1lem5  12767  xrletrid  12935  xrre  12949  xrre3  12951  xleadd1a  13033  xlemul1a  13068  elioc2  13188  elico2  13189  elicc2  13190  elfz1eq  13313  fzadd2  13337  fznatpl1  13356  elfz1uz  13372  nn0fz0  13400  fzctr  13414  fzo1fzo0n0  13484  fzoaddel  13486  elincfzoext  13491  flid  13574  flval3  13581  fladdz  13591  fldiv  13626  modid  13662  hashf1lem1  14213  hashf1lem1OLD  14214  pfxccatin12d  14503  repswpfx  14543  2cshw  14571  pfx2  14705  wwlktovf1  14717  sqeqd  14922  sqrlem7  15005  max0add  15067  abs2difabs  15091  rddif  15097  fzomaxdiflem  15099  rexico  15110  icodiamlt  15192  limsupgre  15235  rlim3  15252  icco1  15294  rlimclim  15300  rlimuni  15304  rlimresb  15319  isercolllem2  15422  isercolllem3  15423  isercoll  15424  caucvgrlem  15429  caurcvgr  15430  iseraltlem3  15440  fsum00  15555  o1fsum  15570  bitsfzolem  16186  bitsfzo  16187  bitsmod  16188  bitscmp  16190  gcd0id  16271  gcdneg  16274  bezoutlem4  16295  nn0seqcvgd  16320  lcmneg  16353  lcmfunsnlem2lem2  16389  qredeq  16407  prmind2  16435  eulerthlem2  16528  pcpremul  16589  pcidlem  16618  pcgcd1  16623  fldivp1  16643  pcfaclem  16644  4sqlem17  16707  vdwlem1  16727  vdwlem6  16732  vdwlem12  16738  vdwlem13  16739  0ram  16766  ram0  16768  ramub1lem1  16772  invco  17528  sectmon  17539  monsect  17540  invid  17544  ssctr  17582  ssceq  17583  0ssc  17597  0subcat  17598  catsubcat  17599  issubc3  17609  fullsubc  17610  funcinv  17633  fthmon  17688  fuccocl  17727  fucidcl  17728  invfuc  17737  2initoinv  17770  2termoinv  17777  elhomai  17793  setcmon  17847  setcepi  17848  catcisolem  17870  curf2cl  17994  yonedalem4c  18040  yonedalem3  18043  yoniso  18048  lublecl  18124  isacs3lem  18305  tsrdir  18367  mnd1  18471  sgrp2nmndlem4  18612  sgrp2nmndlem5  18613  nmznsg  18841  ghmpreima  18901  ghmeql  18902  ghmnsgpreima  18904  cntzsubm  18987  cntzsubg  18988  cntzmhm  18990  symgextfo  19075  symgfixf1  19090  symgfixfolem1  19091  odlem2  19192  gexlem2  19232  gexcl2  19239  sylow1lem5  19252  subgslw  19266  slwhash  19274  fislw  19275  sylow3lem1  19277  lsmsubg  19304  efgredlemd  19395  efgredlem  19398  efgcpbllemb  19406  frgpuplem  19423  cyggeninv  19528  iscygd  19532  iscygodd  19533  gsumzadd  19568  gsumconst  19580  gsumpt  19608  gsum2dlem2  19617  gsum2d  19618  gsum2d2lem  19619  dprdfcntz  19663  eldprdi  19666  subgdmdprd  19682  subgdprd  19683  dprdpr  19698  ablfac1c  19719  ablfac1eu  19721  ablfaclem3  19735  ring1  19886  kerf1ghm  20032  issubdrg  20094  rhmeql  20099  rhmima  20100  cntzsubr  20102  isabvd  20125  abvdiv  20142  lsslsp  20322  lmhmima  20354  lmhmpreima  20355  lmhmeql  20362  lsmcl  20390  lspfixed  20435  qsssubdrg  20702  gzrngunit  20709  evpmodpmf1o  20846  ocvpj  20969  dsmm0cl  20992  dsmmacl  20993  dsmmsubg  20995  dsmmlss  20996  frlmsplit2  21025  uvcff  21043  lindfrn  21073  f1lindf  21074  lindsss  21076  issubassa  21118  issubassa2  21141  snifpsrbag  21170  psrbaglesupp  21172  psrbaglesuppOLD  21173  psrbaglecl  21174  psrbagleclOLD  21175  psrbagaddcl  21176  psrbagaddclOLD  21177  psrbagcon  21178  psrbagconOLD  21179  mplsubglem  21250  mpllsslem  21251  mplassa  21272  subrgmpl  21278  mplcoe5  21286  mplbas2  21288  mplind  21323  mpfind  21362  ismhp2  21377  mhpmulcl  21384  mhplss  21390  ply1assa  21415  coe1tmmul2  21492  coe1tmmul  21493  cply1coe0bi  21516  mat1rngiso  21680  dmatid  21689  dmatsubcl  21692  dmatscmcl  21697  scmatid  21708  scmataddcl  21710  scmatsubcl  21711  scmatmulcl  21712  smatvscl  21718  scmatrhmcl  21722  scmatrngiso  21730  mat0scmat  21732  mat1scmat  21733  mdet0pr  21786  m2cpmrngiso  21952  pm2mprngiso  22016  chmaidscmat  22042  distop  22190  indistopon  22196  ppttop  22202  epttop  22204  mretopd  22288  toponmre  22289  neiss  22305  opnneissb  22310  ssnei2  22312  innei  22321  neiptoptop  22327  ordtcld1  22393  ordtcld2  22394  lmconst  22457  cnpnei  22460  iscncl  22465  cnss1  22472  cnss2  22473  cncnpi  22474  cncnp  22476  cnconst2  22479  cnrest  22481  cnpresti  22484  cnpdis  22489  paste  22490  lmcnp  22500  cnhaus  22550  hauscmp  22603  2ndcomap  22654  1stcelcls  22657  1stccnp  22658  llyrest  22681  nllyrest  22682  llyidm  22684  nllyidm  22685  ssref  22708  reftr  22710  refun0  22711  dissnref  22724  kgentopon  22734  kgenidm  22743  kgencn3  22754  txcld  22799  neitx  22803  tx1cn  22805  tx2cn  22806  ptcld  22809  xkoccn  22815  txcnp  22816  ptcnp  22818  txcnmpt  22820  ptcn  22823  txdis1cn  22831  ptrescn  22835  txkgen  22848  xkoco1cn  22853  xkoco2cn  22854  xkococn  22856  xkoinjcn  22883  qtoptop2  22895  qtopuni  22898  qtopid  22901  qtopkgen  22906  basqtop  22907  tgqtop  22908  qtopss  22911  qtopeu  22912  qtoprest  22913  kqopn  22930  kqcld  22931  kqreglem2  22938  reghmph  22989  ordthmeolem  22997  qtopf1  23012  opnfbas  23038  isfil2  23052  fbasweak  23061  fsubbas  23063  filconn  23079  fbasrn  23080  rnelfmlem  23148  flimss2  23168  flimss1  23169  hausflim  23177  flimclslem  23180  flimsncls  23182  cnpflfi  23195  flfcnp2  23203  fclsfnflim  23223  cnextfvval  23261  cnextfres1  23264  symgtgp  23302  opnsubg  23304  ghmcnp  23311  qustgpopn  23316  qustgplem  23317  qustgphaus  23319  tsmsfbas  23324  ustfilxp  23409  utoptop  23431  utopbas  23432  restutopopn  23435  iducn  23480  cstucnd  23481  ucncn  23482  fmucnd  23489  cfilufg  23490  trcfilu  23491  cfiluweak  23492  neipcfilu  23493  psmetres2  23512  isxmetd  23524  xmetpsmet  23546  imasf1oxmet  23573  xblss2ps  23599  xblss2  23600  xblcntrps  23608  xblcntr  23609  blcld  23706  metustfbas  23758  cfilucfil  23760  restmetu  23771  ngptgp  23837  tngngpd  23862  nrmtngnrm  23867  tngnrg  23883  nlmvscn  23896  nrginvrcn  23901  nmo0  23944  nmoeq0  23945  nmoid  23951  nghmcn  23954  0nmhm  23964  blcvx  24006  iccntr  24029  xrge0tsms  24042  xmetdcn2  24045  metdstri  24059  metdscn  24064  rescncf  24105  cncfco  24115  oprpiece1res2  24160  cnheibor  24163  cnllycmp  24164  bndth  24166  ishtpyd  24183  isphtpyd  24194  pcoval2  24224  nmhmcn  24328  ipcn  24455  lmnn  24472  cfilss  24479  iscfil3  24482  cfilfcls  24483  cmetcaulem  24497  iscmet3lem2  24501  cfilres  24505  lmcau  24522  flimcfil  24523  cncmet  24531  rlmbn  24570  minveclem3b  24637  pjthlem1  24646  pjth2  24649  ivthlem3  24662  ovolssnul  24696  ovolctb  24699  ovoliunnul  24716  ovolsca  24724  ovolicopnf  24733  voliunlem2  24760  volsup  24765  dyadmaxlem  24806  vitalilem5  24821  mbfres  24853  mbfss  24855  mbfmulc2re  24857  mbfadd  24870  mbfmulc2  24872  mbflim  24877  i1faddlem  24902  i1fmullem  24903  mbfmul  24936  itg2mulc  24957  itg2cnlem1  24971  ibl0  24996  iblposlem  25001  itgreval  25006  iblneg  25012  iblss  25014  iblss2  25015  itgle  25019  iblconst  25027  iblabs  25038  iblabsr  25039  iblmulc2  25040  bddmulibl  25048  limciun  25103  limcun  25104  dvres2lem  25119  dvidlem  25124  dvcnp2  25129  dvcn  25130  cpnres  25146  dvaddbr  25147  dvmulbr  25148  dvcobr  25155  dvcjbr  25158  dvrec  25164  dvcnvlem  25185  dvferm  25197  dvlip2  25204  dveq0  25209  dv11cn  25210  dvivthlem1  25217  lhop1  25223  lhop2  25224  lhop  25225  dvcnvre  25228  dvfsumlem3  25237  dvfsumlem4  25238  dvfsumrlim  25240  dvfsum2  25243  ftc1a  25246  ftc1lem4  25248  ftc1lem6  25250  ftc1  25251  coe1mul3  25309  deg1addle2  25312  deg1sublt  25320  fta1blem  25378  drnguc1p  25380  ig1prsp  25387  plyco0  25398  plyeq0lem  25416  dgrub  25440  dgreq  25450  dgradd2  25474  dgrmul  25476  dgrcolem2  25480  dgrco  25481  plycpn  25494  plydivlem4  25501  plydiveu  25503  vieta1lem2  25516  vieta1  25517  aalioulem2  25538  aalioulem3  25539  aaliou3lem7  25554  tayl0  25566  ulmcn  25603  ulmdvlem3  25606  psercn  25630  abelth  25645  pilem3  25657  efif1olem1  25743  abslogimle  25774  argregt0  25810  argrege0  25811  logf1o2  25850  cxpsqrtlem  25902  cxpcn3  25946  abscxpbnd  25951  logreclem  25957  ang180lem2  26005  ang180lem3  26006  xrlimcnp  26163  harmonicbnd4  26205  fsumharmonic  26206  lgamgulmlem5  26227  lgambdd  26231  basellem4  26278  dvdsppwf1o  26380  dvdsflf1o  26381  fsumfldivdiaglem  26383  chpeq0  26401  chteq0  26402  chtub  26405  chpub  26413  dchrelbasd  26432  dchrmulcl  26442  dchrinv  26454  bposlem1  26477  bposlem2  26478  lgsdirprm  26524  lgsqrlem2  26540  lgsqrlem3  26541  lgsdchr  26548  lgseisenlem1  26568  lgseisenlem2  26569  lgseisenlem3  26570  lgsquadlem1  26573  2sqlem8  26619  2sqblem  26624  2sqmod  26629  chebbnd1lem1  26662  dchrisumlem1  26682  dchrisumlem2  26683  dchrisumlem3  26684  dchrisum0fno1  26704  pntrmax  26757  pntpbnd1a  26778  pntibndlem3  26785  pntlemn  26793  pntlemi  26797  pntlem3  26802  pntleml  26804  ostth1  26826  ostth2  26830  ostth3  26831  ercgrg  26923  motco  26946  cnvmot  26947  legso  27005  mirmot  27081  colopp  27175  hphl  27177  lmicom  27194  lmimid  27200  lmimot  27204  hypcgrlem1  27205  hypcgrlem2  27206  trgcopyeulem  27211  inagswap  27247  inaghl  27251  cgrg3col4  27259  brbtwn2  27318  axlowdimlem3  27357  axlowdimlem16  27370  axcontlem8  27384  fusgrfis  27742  nbgr2vtx1edg  27762  0vtxrgr  27988  0vtxrusgr  27989  ewlkle  28017  wlk1ewlk  28052  uspgr2wlkeq2  28059  wlkp1lem8  28093  trlontrl  28124  pthonpth  28161  pthdlem2  28181  wlklnwwlkln1  28278  wlknewwlksn  28297  wwlksnred  28302  wwlksnredwwlkn0  28306  2trlond  28349  2pthond  28352  elwwlks2ons3im  28364  clwlkclwwlklem2a1  28401  clwlkclwwlkf1  28419  clwwlkel  28455  clwwlkwwlksb  28463  wwlksext2clwwlk  28466  1ewlk  28524  0trlon  28533  0pthon  28536  1pthond  28553  3trlond  28582  3pthond  28584  3spthond  28586  eupthres  28624  2clwwlk2clwwlk  28759  numclwwlk1lem2foa  28763  numclwwlk1lem2f1  28766  nvabs  29079  vacn  29101  nmcvcn  29102  nmblore  29193  0lno  29197  0blo  29199  nmlno0lem  29200  occl  29711  pjhthlem1  29798  pjpjpre  29826  nmopre  30277  nmlnop0iALT  30402  nmophmi  30438  leoprf2  30534  stlesi  30648  disjdifprg  30959  disjun0  30979  fsuppcurry1  31105  fsuppcurry2  31106  fpwrelmap  31113  fzspl  31156  dfmgc2lem  31318  pwrssmgc  31323  xrge0tsmsd  31362  ogrpaddlt  31388  ogrpsublt  31392  psgnfzto1stlem  31412  fzto1st1  31414  evpmid  31460  pnfinf  31482  rmfsupp2  31537  ornglmullt  31551  orngrmullt  31552  orngmullt  31553  ofldlt1  31557  isarchiofld  31561  nsgmgc  31642  lbsdiflsp0  31752  fedgmul  31757  fldexttr  31778  fldextid  31779  qtopt1  31830  reff  31834  locfinreflem  31835  metideq  31888  metider  31889  pstmxmet  31892  qqhval2lem  31976  qqhcn  31986  qqhucn  31987  pwsiga  32143  prsiga  32144  measle0  32221  mbfmcst  32271  1stmbfm  32272  2ndmbfm  32273  imambfm  32274  cnmbfm  32275  mbfmco  32276  mbfmco2  32277  0elcarsg  32319  carsgclctun  32333  sibfof  32352  oddpwdc  32366  eulerpartlemmf  32387  eulerpartlemgs2  32392  0rrv  32463  ballotlemfc0  32504  ballotlemfcc  32505  signstfveq0  32601  breprexplemc  32657  bnj1452  33077  usgrgt2cycl  33137  acycgr1v  33156  derangen  33179  subfacval3  33196  cvmseu  33283  cvmliftmolem2  33289  cvmliftlem7  33298  cvmliftlem15  33305  cvmlift2lem9a  33310  cvmlift2lem9  33318  cvmlift2lem10  33319  cvmlift2lem11  33320  cvmlift2lem12  33321  cvmlift3lem6  33331  cvmlift3lem8  33333  ex-sategoelel  33428  ex-sategoelelomsuc  33433  mclsppslem  33590  mclspps  33591  wsuclem  33864  nosepon  33913  nolesgn2ores  33920  nogesgn1ores  33922  nosupres  33955  nosupbnd1lem2  33957  nosupbnd2lem1  33963  noinfres  33970  noinfbnd1lem2  33972  noinfbnd2lem1  33978  cofcutrtime  34138  fness  34583  fnetr  34585  fnessref  34591  refssfne  34592  neibastop1  34593  neibastop2  34595  tailfb  34611  filnetlem3  34614  bj-finsumval0  35500  bj-rvecvec  35514  dfgcd3  35539  lindsadd  35814  poimirlem13  35834  poimirlem15  35836  poimirlem24  35845  poimirlem28  35849  mblfinlem2  35859  ovoliunnfl  35863  volsupnfl  35866  mbfresfi  35867  iblabsnc  35885  iblmulc2nc  35886  ftc1cnnclem  35892  ftc1cnnc  35893  ftc1anc  35902  sdclem2  35944  metf1o  35957  ismtyhmeolem  36006  ismtyres  36010  heibor1lem  36011  bfplem2  36025  bfp  36026  rrncmslem  36034  iccbnd  36042  icccmpALT  36043  rngogrphom  36173  rngoisoco  36184  keridl  36234  lsmcv2  37085  lsatcv0  37087  lcvexchlem4  37093  lcvexchlem5  37094  l1cvpat  37110  lfl0f  37125  lfladdcl  37127  lflnegcl  37131  lkrlss  37151  eqlkr  37155  lkrlsp  37158  lkrlsp2  37159  lshpkrcl  37172  lkrin  37220  1cvrjat  37531  llni  37564  llnle  37574  lplni  37588  lplnle  37596  llncvrlpln2  37613  2atmat  37617  lvoli  37631  lplncvrlvol2  37671  elpaddri  37858  paddclN  37898  pclclN  37947  pclfinN  37956  0psubclN  37999  1psubclN  38000  atpsubclN  38001  pmapsubclN  38002  osumclN  38023  pexmidN  38025  pexmidlem6N  38031  lhp2lt  38057  lautcnv  38146  idlaut  38152  lautco  38153  idldil  38170  ldilcnv  38171  ldilco  38172  ltrncnv  38202  idltrn  38206  cdleme16d  38337  cdleme50laut  38603  cdleme50ldil  38604  cdleme50ltrn  38613  ltrnco  38775  dian0  39095  dia0eldmN  39096  dia1eldmN  39097  dialss  39102  diaintclN  39114  docaclN  39180  doca2N  39182  djajN  39193  dibintclN  39223  diblss  39226  dicvaddcl  39246  dicvscacl  39247  dicn0  39248  cdlemn11a  39263  dihord2cN  39277  dihord11b  39278  dihord6apre  39312  dihmeetlem1N  39346  dihglblem5apreN  39347  dihpN  39392  dihjatcclem4  39477  dochkr1  39534  islpoldN  39540  lcfrlem31  39629  mapdpglem18  39745  mapdheq2  39785  mapdheq4  39788  mapdh6aN  39791  hdmap1l6a  39865  hdmap14lem4a  39927  lcmineqlem4  40082  isfsuppd  40254  frlmfzoccat  40273  drnginvmuld  40291  fsuppind  40316  fsuppssind  40319  prjspvs  40486  irrapxlem4  40684  pell1234qrdich  40720  pell1qr1  40730  pell14qrgap  40734  pellqrexplicit  40736  rmspecfund  40768  fzmaxdif  40841  acongeq  40843  jm2.23  40856  jm3.1  40880  lmhmlnmsplit  40950  hbt  40993  dgrsub2  40998  proot1ex  41064  clublem  41256  dftrcl3  41366  mnugrud  41940  hashnzfz2  41977  dvconstbi  41990  ubelsupr  42601  restopn3  42743  wessf1ornlem  42766  lefldiveq  42879  iccintsng  43110  climsuse  43198  mullimc  43206  limcdm0  43208  limccog  43210  mullimcf  43213  constlimc  43214  idlimc  43216  limcperiod  43218  limsupre  43231  limcleqr  43234  neglimc  43237  addlimc  43238  0ellimcdiv  43239  xlimliminflimsup  43452  cncfshift  43464  cncfperiod  43469  cncfuni  43476  icccncfext  43477  cncfiooicclem1  43483  fperdvper  43509  ioodvbdlimc1lem2  43522  ioodvbdlimc2lem  43524  mbfres2cn  43548  iblsplit  43556  stoweidlem7  43597  stoweidlem13  43603  stoweidlem26  43616  wallispilem3  43657  stirlinglem6  43669  stirlinglem10  43673  dirkercncf  43697  fourierdlem6  43703  fourierdlem11  43708  fourierdlem12  43709  fourierdlem15  43712  fourierdlem26  43723  fourierdlem42  43739  fourierdlem50  43746  fourierdlem51  43747  fourierdlem52  43748  fourierdlem54  43750  fourierdlem62  43758  fourierdlem79  43775  fourierdlem102  43798  fourierdlem114  43810  etransclem23  43847  zgeltp1eq  44859  setsnidel  44887  preimafvsnel  44889  iccpartres  44928  prpair  45011  fpprel2  45251  rabsubmgmd  45403  submgmid  45405  subsubmgm  45409  mgmhmima  45414  mgmhmeql  45415  isassintop  45462  rnghmsscmap2  45589  rnghmsscmap  45590  rnghmsubcsetc  45593  zrzeroorngc  45618  rhmsscmap2  45635  rhmsscmap  45636  rhmsubcsetc  45639  rhmsscrnghm  45642  rhmsubcrngc  45645  srhmsubc  45692  fldhmsubc  45700  rhmsubc  45706  srhmsubcALTV  45710  fldhmsubcALTV  45718  rhmsubcALTV  45724  rmfsupp  45768  mndpfsupp  45770  scmfsupp  45772  mptcfsupp  45774  lcoel0  45827  lincsumcl  45830  lincscmcl  45831  lcoss  45835  lindsrng01  45867  lincreslvec3  45881  lindssnlvec  45885  zgtp1leeq  45920  lubsscl  46312  glbsscl  46313  idmon  46355  idepi  46356  thinciso  46399