Theorem mpbir2and 709

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

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

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 396

This theorem is referenced by:  elpreimad  6930  fveqressseq  6951  fmptsng  7034  fmptsnd  7035  fnprb  7078  fntpb  7079  fpr3g  8085  frrlem4  8089  fdmfifsupp  9099  fczfsuppd  9107  fsuppmptif  9119  fsuppco2  9123  fsuppcor  9124  dffi3  9151  suppr  9191  infpr  9223  ordtypelem7  9244  cantnf0  9394  cantnfp1lem1  9397  cantnfp1lem2  9398  cantnfp1lem3  9399  cantnflem1a  9404  cantnflem1d  9407  cantnflem1  9408  cantnf  9412  rankpwi  9565  carduni  9723  fin23lem32  10084  fpwwe2lem5  10375  fpwwe2lem11  10381  fpwwe2lem12  10382  fpwwe2  10383  inttsk  10514  grutsk1  10561  add20  11470  supaddc  11925  supadd  11926  supmul  11930  suprzcl  12383  uzid  12579  uzwo3  12665  rpnnen1lem5  12703  xrletrid  12871  xrre  12885  xrre3  12887  xleadd1a  12969  xlemul1a  13004  elioc2  13124  elico2  13125  elicc2  13126  elfz1eq  13249  fzadd2  13273  fznatpl1  13292  elfz1uz  13308  nn0fz0  13336  fzctr  13350  fzo1fzo0n0  13419  fzoaddel  13421  elincfzoext  13426  flid  13509  flval3  13516  fladdz  13526  fldiv  13561  modid  13597  hashf1lem1  14149  hashf1lem1OLD  14150  pfxccatin12d  14439  repswpfx  14479  2cshw  14507  pfx2  14641  wwlktovf1  14653  sqeqd  14858  sqrlem7  14941  max0add  15003  abs2difabs  15027  rddif  15033  fzomaxdiflem  15035  rexico  15046  icodiamlt  15128  limsupgre  15171  rlim3  15188  icco1  15230  rlimclim  15236  rlimuni  15240  rlimresb  15255  isercolllem2  15358  isercolllem3  15359  isercoll  15360  caucvgrlem  15365  caurcvgr  15366  iseraltlem3  15376  fsum00  15491  o1fsum  15506  bitsfzolem  16122  bitsfzo  16123  bitsmod  16124  bitscmp  16126  gcd0id  16207  gcdneg  16210  bezoutlem4  16231  nn0seqcvgd  16256  lcmneg  16289  lcmfunsnlem2lem2  16325  qredeq  16343  prmind2  16371  eulerthlem2  16464  pcpremul  16525  pcidlem  16554  pcgcd1  16559  fldivp1  16579  pcfaclem  16580  4sqlem17  16643  vdwlem1  16663  vdwlem6  16668  vdwlem12  16674  vdwlem13  16675  0ram  16702  ram0  16704  ramub1lem1  16708  invco  17464  sectmon  17475  monsect  17476  invid  17480  ssctr  17518  ssceq  17519  0ssc  17533  0subcat  17534  catsubcat  17535  issubc3  17545  fullsubc  17546  funcinv  17569  fthmon  17624  fuccocl  17663  fucidcl  17664  invfuc  17673  2initoinv  17706  2termoinv  17713  elhomai  17729  setcmon  17783  setcepi  17784  catcisolem  17806  curf2cl  17930  yonedalem4c  17976  yonedalem3  17979  yoniso  17984  lublecl  18060  isacs3lem  18241  tsrdir  18303  mnd1  18407  sgrp2nmndlem4  18548  sgrp2nmndlem5  18549  nmznsg  18777  ghmpreima  18837  ghmeql  18838  ghmnsgpreima  18840  cntzsubm  18923  cntzsubg  18924  cntzmhm  18926  symgextfo  19011  symgfixf1  19026  symgfixfolem1  19027  odlem2  19128  gexlem2  19168  gexcl2  19175  sylow1lem5  19188  subgslw  19202  slwhash  19210  fislw  19211  sylow3lem1  19213  lsmsubg  19240  efgredlemd  19331  efgredlem  19334  efgcpbllemb  19342  frgpuplem  19359  cyggeninv  19464  iscygd  19468  iscygodd  19469  gsumzadd  19504  gsumconst  19516  gsumpt  19544  gsum2dlem2  19553  gsum2d  19554  gsum2d2lem  19555  dprdfcntz  19599  eldprdi  19602  subgdmdprd  19618  subgdprd  19619  dprdpr  19634  ablfac1c  19655  ablfac1eu  19657  ablfaclem3  19671  ring1  19822  kerf1ghm  19968  issubdrg  20030  rhmeql  20035  rhmima  20036  cntzsubr  20038  isabvd  20061  abvdiv  20078  lsslsp  20258  lmhmima  20290  lmhmpreima  20291  lmhmeql  20298  lsmcl  20326  lspfixed  20371  qsssubdrg  20638  gzrngunit  20645  evpmodpmf1o  20782  ocvpj  20905  dsmm0cl  20928  dsmmacl  20929  dsmmsubg  20931  dsmmlss  20932  frlmsplit2  20961  uvcff  20979  lindfrn  21009  f1lindf  21010  lindsss  21012  issubassa  21054  issubassa2  21077  snifpsrbag  21106  psrbaglesupp  21108  psrbaglesuppOLD  21109  psrbaglecl  21110  psrbagleclOLD  21111  psrbagaddcl  21112  psrbagaddclOLD  21113  psrbagcon  21114  psrbagconOLD  21115  mplsubglem  21186  mpllsslem  21187  mplassa  21208  subrgmpl  21214  mplcoe5  21222  mplbas2  21224  mplind  21259  mpfind  21298  ismhp2  21313  mhpmulcl  21320  mhplss  21326  ply1assa  21351  coe1tmmul2  21428  coe1tmmul  21429  cply1coe0bi  21452  mat1rngiso  21616  dmatid  21625  dmatsubcl  21628  dmatscmcl  21633  scmatid  21644  scmataddcl  21646  scmatsubcl  21647  scmatmulcl  21648  smatvscl  21654  scmatrhmcl  21658  scmatrngiso  21666  mat0scmat  21668  mat1scmat  21669  mdet0pr  21722  m2cpmrngiso  21888  pm2mprngiso  21952  chmaidscmat  21978  distop  22126  indistopon  22132  ppttop  22138  epttop  22140  mretopd  22224  toponmre  22225  neiss  22241  opnneissb  22246  ssnei2  22248  innei  22257  neiptoptop  22263  ordtcld1  22329  ordtcld2  22330  lmconst  22393  cnpnei  22396  iscncl  22401  cnss1  22408  cnss2  22409  cncnpi  22410  cncnp  22412  cnconst2  22415  cnrest  22417  cnpresti  22420  cnpdis  22425  paste  22426  lmcnp  22436  cnhaus  22486  hauscmp  22539  2ndcomap  22590  1stcelcls  22593  1stccnp  22594  llyrest  22617  nllyrest  22618  llyidm  22620  nllyidm  22621  ssref  22644  reftr  22646  refun0  22647  dissnref  22660  kgentopon  22670  kgenidm  22679  kgencn3  22690  txcld  22735  neitx  22739  tx1cn  22741  tx2cn  22742  ptcld  22745  xkoccn  22751  txcnp  22752  ptcnp  22754  txcnmpt  22756  ptcn  22759  txdis1cn  22767  ptrescn  22771  txkgen  22784  xkoco1cn  22789  xkoco2cn  22790  xkococn  22792  xkoinjcn  22819  qtoptop2  22831  qtopuni  22834  qtopid  22837  qtopkgen  22842  basqtop  22843  tgqtop  22844  qtopss  22847  qtopeu  22848  qtoprest  22849  kqopn  22866  kqcld  22867  kqreglem2  22874  reghmph  22925  ordthmeolem  22933  qtopf1  22948  opnfbas  22974  isfil2  22988  fbasweak  22997  fsubbas  22999  filconn  23015  fbasrn  23016  rnelfmlem  23084  flimss2  23104  flimss1  23105  hausflim  23113  flimclslem  23116  flimsncls  23118  cnpflfi  23131  flfcnp2  23139  fclsfnflim  23159  cnextfvval  23197  cnextfres1  23200  symgtgp  23238  opnsubg  23240  ghmcnp  23247  qustgpopn  23252  qustgplem  23253  qustgphaus  23255  tsmsfbas  23260  ustfilxp  23345  utoptop  23367  utopbas  23368  restutopopn  23371  iducn  23416  cstucnd  23417  ucncn  23418  fmucnd  23425  cfilufg  23426  trcfilu  23427  cfiluweak  23428  neipcfilu  23429  psmetres2  23448  isxmetd  23460  xmetpsmet  23482  imasf1oxmet  23509  xblss2ps  23535  xblss2  23536  xblcntrps  23544  xblcntr  23545  blcld  23642  metustfbas  23694  cfilucfil  23696  restmetu  23707  ngptgp  23773  tngngpd  23798  nrmtngnrm  23803  tngnrg  23819  nlmvscn  23832  nrginvrcn  23837  nmo0  23880  nmoeq0  23881  nmoid  23887  nghmcn  23890  0nmhm  23900  blcvx  23942  iccntr  23965  xrge0tsms  23978  xmetdcn2  23981  metdstri  23995  metdscn  24000  rescncf  24041  cncfco  24051  oprpiece1res2  24096  cnheibor  24099  cnllycmp  24100  bndth  24102  ishtpyd  24119  isphtpyd  24130  pcoval2  24160  nmhmcn  24264  ipcn  24391  lmnn  24408  cfilss  24415  iscfil3  24418  cfilfcls  24419  cmetcaulem  24433  iscmet3lem2  24437  cfilres  24441  lmcau  24458  flimcfil  24459  cncmet  24467  rlmbn  24506  minveclem3b  24573  pjthlem1  24582  pjth2  24585  ivthlem3  24598  ovolssnul  24632  ovolctb  24635  ovoliunnul  24652  ovolsca  24660  ovolicopnf  24669  voliunlem2  24696  volsup  24701  dyadmaxlem  24742  vitalilem5  24757  mbfres  24789  mbfss  24791  mbfmulc2re  24793  mbfadd  24806  mbfmulc2  24808  mbflim  24813  i1faddlem  24838  i1fmullem  24839  mbfmul  24872  itg2mulc  24893  itg2cnlem1  24907  ibl0  24932  iblposlem  24937  itgreval  24942  iblneg  24948  iblss  24950  iblss2  24951  itgle  24955  iblconst  24963  iblabs  24974  iblabsr  24975  iblmulc2  24976  bddmulibl  24984  limciun  25039  limcun  25040  dvres2lem  25055  dvidlem  25060  dvcnp2  25065  dvcn  25066  cpnres  25082  dvaddbr  25083  dvmulbr  25084  dvcobr  25091  dvcjbr  25094  dvrec  25100  dvcnvlem  25121  dvferm  25133  dvlip2  25140  dveq0  25145  dv11cn  25146  dvivthlem1  25153  lhop1  25159  lhop2  25160  lhop  25161  dvcnvre  25164  dvfsumlem3  25173  dvfsumlem4  25174  dvfsumrlim  25176  dvfsum2  25179  ftc1a  25182  ftc1lem4  25184  ftc1lem6  25186  ftc1  25187  coe1mul3  25245  deg1addle2  25248  deg1sublt  25256  fta1blem  25314  drnguc1p  25316  ig1prsp  25323  plyco0  25334  plyeq0lem  25352  dgrub  25376  dgreq  25386  dgradd2  25410  dgrmul  25412  dgrcolem2  25416  dgrco  25417  plycpn  25430  plydivlem4  25437  plydiveu  25439  vieta1lem2  25452  vieta1  25453  aalioulem2  25474  aalioulem3  25475  aaliou3lem7  25490  tayl0  25502  ulmcn  25539  ulmdvlem3  25542  psercn  25566  abelth  25581  pilem3  25593  efif1olem1  25679  abslogimle  25710  argregt0  25746  argrege0  25747  logf1o2  25786  cxpsqrtlem  25838  cxpcn3  25882  abscxpbnd  25887  logreclem  25893  ang180lem2  25941  ang180lem3  25942  xrlimcnp  26099  harmonicbnd4  26141  fsumharmonic  26142  lgamgulmlem5  26163  lgambdd  26167  basellem4  26214  dvdsppwf1o  26316  dvdsflf1o  26317  fsumfldivdiaglem  26319  chpeq0  26337  chteq0  26338  chtub  26341  chpub  26349  dchrelbasd  26368  dchrmulcl  26378  dchrinv  26390  bposlem1  26413  bposlem2  26414  lgsdirprm  26460  lgsqrlem2  26476  lgsqrlem3  26477  lgsdchr  26484  lgseisenlem1  26504  lgseisenlem2  26505  lgseisenlem3  26506  lgsquadlem1  26509  2sqlem8  26555  2sqblem  26560  2sqmod  26565  chebbnd1lem1  26598  dchrisumlem1  26618  dchrisumlem2  26619  dchrisumlem3  26620  dchrisum0fno1  26640  pntrmax  26693  pntpbnd1a  26714  pntibndlem3  26721  pntlemn  26729  pntlemi  26733  pntlem3  26738  pntleml  26740  ostth1  26762  ostth2  26766  ostth3  26767  ercgrg  26859  motco  26882  cnvmot  26883  legso  26941  mirmot  27017  colopp  27111  hphl  27113  lmicom  27130  lmimid  27136  lmimot  27140  hypcgrlem1  27141  hypcgrlem2  27142  trgcopyeulem  27147  inagswap  27183  inaghl  27187  cgrg3col4  27195  brbtwn2  27254  axlowdimlem3  27293  axlowdimlem16  27306  axcontlem8  27320  fusgrfis  27678  nbgr2vtx1edg  27698  0vtxrgr  27924  0vtxrusgr  27925  ewlkle  27953  wlk1ewlk  27987  uspgr2wlkeq2  27994  wlkp1lem8  28028  trlontrl  28058  pthonpth  28095  pthdlem2  28115  wlklnwwlkln1  28212  wlknewwlksn  28231  wwlksnred  28236  wwlksnredwwlkn0  28240  2trlond  28283  2pthond  28286  elwwlks2ons3im  28298  clwlkclwwlklem2a1  28335  clwlkclwwlkf1  28353  clwwlkel  28389  clwwlkwwlksb  28397  wwlksext2clwwlk  28400  1ewlk  28458  0trlon  28467  0pthon  28470  1pthond  28487  3trlond  28516  3pthond  28518  3spthond  28520  eupthres  28558  2clwwlk2clwwlk  28693  numclwwlk1lem2foa  28697  numclwwlk1lem2f1  28700  nvabs  29013  vacn  29035  nmcvcn  29036  nmblore  29127  0lno  29131  0blo  29133  nmlno0lem  29134  occl  29645  pjhthlem1  29732  pjpjpre  29760  nmopre  30211  nmlnop0iALT  30336  nmophmi  30372  leoprf2  30468  stlesi  30582  disjdifprg  30893  disjun0  30913  fsuppcurry1  31039  fsuppcurry2  31040  fpwrelmap  31047  fzspl  31090  dfmgc2lem  31252  pwrssmgc  31257  xrge0tsmsd  31296  ogrpaddlt  31322  ogrpsublt  31326  psgnfzto1stlem  31346  fzto1st1  31348  evpmid  31394  pnfinf  31416  rmfsupp2  31471  ornglmullt  31485  orngrmullt  31486  orngmullt  31487  ofldlt1  31491  isarchiofld  31495  nsgmgc  31576  lbsdiflsp0  31686  fedgmul  31691  fldexttr  31712  fldextid  31713  qtopt1  31764  reff  31768  locfinreflem  31769  metideq  31822  metider  31823  pstmxmet  31826  qqhval2lem  31910  qqhcn  31920  qqhucn  31921  pwsiga  32077  prsiga  32078  measle0  32155  mbfmcst  32205  1stmbfm  32206  2ndmbfm  32207  imambfm  32208  cnmbfm  32209  mbfmco  32210  mbfmco2  32211  0elcarsg  32253  carsgclctun  32267  sibfof  32286  oddpwdc  32300  eulerpartlemmf  32321  eulerpartlemgs2  32326  0rrv  32397  ballotlemfc0  32438  ballotlemfcc  32439  signstfveq0  32535  breprexplemc  32591  bnj1452  33011  usgrgt2cycl  33071  acycgr1v  33090  derangen  33113  subfacval3  33130  cvmseu  33217  cvmliftmolem2  33223  cvmliftlem7  33232  cvmliftlem15  33239  cvmlift2lem9a  33244  cvmlift2lem9  33252  cvmlift2lem10  33253  cvmlift2lem11  33254  cvmlift2lem12  33255  cvmlift3lem6  33265  cvmlift3lem8  33267  ex-sategoelel  33362  ex-sategoelelomsuc  33367  mclsppslem  33524  mclspps  33525  wsuclem  33798  nosepon  33847  nolesgn2ores  33854  nogesgn1ores  33856  nosupres  33889  nosupbnd1lem2  33891  nosupbnd2lem1  33897  noinfres  33904  noinfbnd1lem2  33906  noinfbnd2lem1  33912  cofcutrtime  34072  fness  34517  fnetr  34519  fnessref  34525  refssfne  34526  neibastop1  34527  neibastop2  34529  tailfb  34545  filnetlem3  34548  bj-finsumval0  35435  bj-rvecvec  35449  dfgcd3  35474  lindsadd  35749  poimirlem13  35769  poimirlem15  35771  poimirlem24  35780  poimirlem28  35784  mblfinlem2  35794  ovoliunnfl  35798  volsupnfl  35801  mbfresfi  35802  iblabsnc  35820  iblmulc2nc  35821  ftc1cnnclem  35827  ftc1cnnc  35828  ftc1anc  35837  sdclem2  35879  metf1o  35892  ismtyhmeolem  35941  ismtyres  35945  heibor1lem  35946  bfplem2  35960  bfp  35961  rrncmslem  35969  iccbnd  35977  icccmpALT  35978  rngogrphom  36108  rngoisoco  36119  keridl  36169  lsmcv2  37022  lsatcv0  37024  lcvexchlem4  37030  lcvexchlem5  37031  l1cvpat  37047  lfl0f  37062  lfladdcl  37064  lflnegcl  37068  lkrlss  37088  eqlkr  37092  lkrlsp  37095  lkrlsp2  37096  lshpkrcl  37109  lkrin  37157  1cvrjat  37468  llni  37501  llnle  37511  lplni  37525  lplnle  37533  llncvrlpln2  37550  2atmat  37554  lvoli  37568  lplncvrlvol2  37608  elpaddri  37795  paddclN  37835  pclclN  37884  pclfinN  37893  0psubclN  37936  1psubclN  37937  atpsubclN  37938  pmapsubclN  37939  osumclN  37960  pexmidN  37962  pexmidlem6N  37968  lhp2lt  37994  lautcnv  38083  idlaut  38089  lautco  38090  idldil  38107  ldilcnv  38108  ldilco  38109  ltrncnv  38139  idltrn  38143  cdleme16d  38274  cdleme50laut  38540  cdleme50ldil  38541  cdleme50ltrn  38550  ltrnco  38712  dian0  39032  dia0eldmN  39033  dia1eldmN  39034  dialss  39039  diaintclN  39051  docaclN  39117  doca2N  39119  djajN  39130  dibintclN  39160  diblss  39163  dicvaddcl  39183  dicvscacl  39184  dicn0  39185  cdlemn11a  39200  dihord2cN  39214  dihord11b  39215  dihord6apre  39249  dihmeetlem1N  39283  dihglblem5apreN  39284  dihpN  39329  dihjatcclem4  39414  dochkr1  39471  islpoldN  39477  lcfrlem31  39566  mapdpglem18  39682  mapdheq2  39722  mapdheq4  39725  mapdh6aN  39728  hdmap1l6a  39802  hdmap14lem4a  39864  lcmineqlem4  40020  isfsuppd  40197  frlmfzoccat  40216  drnginvmuld  40234  fsuppind  40259  fsuppssind  40262  prjspvs  40429  irrapxlem4  40627  pell1234qrdich  40663  pell1qr1  40673  pell14qrgap  40677  pellqrexplicit  40679  rmspecfund  40711  fzmaxdif  40783  acongeq  40785  jm2.23  40798  jm3.1  40822  lmhmlnmsplit  40892  hbt  40935  dgrsub2  40940  proot1ex  41006  clublem  41171  dftrcl3  41281  mnugrud  41855  hashnzfz2  41892  dvconstbi  41905  ubelsupr  42516  wessf1ornlem  42675  lefldiveq  42785  iccintsng  43015  climsuse  43103  mullimc  43111  limcdm0  43113  limccog  43115  mullimcf  43118  constlimc  43119  idlimc  43121  limcperiod  43123  limsupre  43136  limcleqr  43139  neglimc  43142  addlimc  43143  0ellimcdiv  43144  xlimliminflimsup  43357  cncfshift  43369  cncfperiod  43374  cncfuni  43381  icccncfext  43382  cncfiooicclem1  43388  fperdvper  43414  ioodvbdlimc1lem2  43427  ioodvbdlimc2lem  43429  mbfres2cn  43453  iblsplit  43461  stoweidlem7  43502  stoweidlem13  43508  stoweidlem26  43521  wallispilem3  43562  stirlinglem6  43574  stirlinglem10  43578  dirkercncf  43602  fourierdlem6  43608  fourierdlem11  43613  fourierdlem12  43614  fourierdlem15  43617  fourierdlem26  43628  fourierdlem42  43644  fourierdlem50  43651  fourierdlem51  43652  fourierdlem52  43653  fourierdlem54  43655  fourierdlem62  43663  fourierdlem79  43680  fourierdlem102  43703  fourierdlem114  43715  etransclem23  43752  zgeltp1eq  44753  setsnidel  44781  preimafvsnel  44783  iccpartres  44822  prpair  44905  fpprel2  45145  rabsubmgmd  45297  submgmid  45299  subsubmgm  45303  mgmhmima  45308  mgmhmeql  45309  isassintop  45356  rnghmsscmap2  45483  rnghmsscmap  45484  rnghmsubcsetc  45487  zrzeroorngc  45512  rhmsscmap2  45529  rhmsscmap  45530  rhmsubcsetc  45533  rhmsscrnghm  45536  rhmsubcrngc  45539  srhmsubc  45586  fldhmsubc  45594  rhmsubc  45600  srhmsubcALTV  45604  fldhmsubcALTV  45612  rhmsubcALTV  45618  rmfsupp  45662  mndpfsupp  45664  scmfsupp  45666  mptcfsupp  45668  lcoel0  45721  lincsumcl  45724  lincscmcl  45725  lcoss  45729  lindsrng01  45761  lincreslvec3  45775  lindssnlvec  45779  zgtp1leeq  45814  lubsscl  46206  glbsscl  46207  idmon  46249  idepi  46250  thinciso  46293