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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  elpreimad  6699  fveqressseq  6717  fmptsng  6798  fmptsnd  6799  fnprb  6842  fntpb  6843  fdmfifsupp  8694  fczfsuppd  8702  fsuppmptif  8714  fsuppco2  8717  fsuppcor  8718  dffi3  8746  suppr  8786  infpr  8818  ordtypelem7  8839  cantnf0  8989  cantnfp1lem1  8992  cantnfp1lem2  8993  cantnfp1lem3  8994  cantnflem1a  8999  cantnflem1d  9002  cantnflem1  9003  cantnf  9007  rankpwi  9103  carduni  9261  fin23lem32  9617  fpwwe2lem6  9908  fpwwe2lem9  9911  fpwwe2lem12  9914  fpwwe2lem13  9915  fpwwe2  9916  inttsk  10047  grutsk1  10094  add20  11005  supaddc  11461  supadd  11462  supmul  11466  suprzcl  11916  uzwo3  12197  rpnnen1lem5  12235  xrletrid  12403  xrre  12417  xrre3  12419  xleadd1a  12501  xlemul1a  12536  elioc2  12654  elico2  12655  elicc2  12656  elfz1eq  12773  fzadd2  12797  fznatpl1  12816  elfz1uz  12832  nn0fz0  12860  fzctr  12874  fzo1fzo0n0  12943  fzoaddel  12945  elincfzoext  12950  flid  13033  flval3  13040  fladdz  13050  fldiv  13083  modid  13119  seqf1olem1  13264  bcval5  13533  hashf1lem1  13666  eqs1  13815  pfxccatin12d  13948  repswpfx  13988  pfx2  14150  wwlktovf1  14160  sqeqd  14364  sqrlem7  14447  max0add  14509  abs2difabs  14533  rddif  14539  fzomaxdiflem  14541  rexico  14552  icodiamlt  14634  limsupgre  14677  rlim3  14694  icco1  14736  rlimclim  14742  rlimuni  14746  rlimresb  14761  isercolllem2  14861  isercolllem3  14862  isercoll  14863  caucvgrlem  14868  caurcvgr  14869  iseraltlem3  14879  fsum00  14991  o1fsum  15006  bitsfzolem  15621  bitsfzo  15622  bitsmod  15623  bitscmp  15625  gcd0id  15705  gcdneg  15708  bezoutlem4  15724  nn0seqcvgd  15748  lcmneg  15781  lcmfunsnlem2lem2  15817  qredeq  15835  prmind2  15863  hashdvds  15946  eulerthlem2  15953  pcpremul  16014  pcidlem  16042  pcgcd1  16047  fldivp1  16067  pcfaclem  16068  prmreclem5  16090  4sqlem17  16131  vdwlem1  16151  vdwlem6  16156  vdwlem12  16162  vdwlem13  16163  0ram  16190  ram0  16192  ramub1lem1  16196  invco  16875  sectmon  16886  monsect  16887  invid  16891  ssctr  16929  ssceq  16930  0ssc  16941  0subcat  16942  catsubcat  16943  issubc3  16953  fullsubc  16954  funcinv  16977  fthmon  17031  fuccocl  17068  fucidcl  17069  invfuc  17078  2initoinv  17104  2termoinv  17111  elhomai  17127  setcmon  17181  setcepi  17182  catcisolem  17200  curf2cl  17315  yonedalem4c  17361  yonedalem3  17364  yoniso  17369  lublecl  17433  isacs3lem  17610  tsrdir  17682  mnd1  17775  sgrp2nmndlem4  17859  sgrp2nmndlem5  17860  nmznsg  18082  ghmpreima  18126  ghmeql  18127  ghmnsgpreima  18129  cntzsubm  18212  cntzsubg  18213  cntzmhm  18215  symgextfo  18286  symgfixf1  18301  symgfixfolem1  18302  odlem2  18403  gexlem2  18442  gexcl2  18449  sylow1lem5  18462  subgslw  18476  slwhash  18484  fislw  18485  sylow3lem1  18487  lsmsubg  18514  efgredlemd  18602  efgredlem  18605  efgcpbllemb  18613  frgpuplem  18630  cyggeninv  18730  iscygd  18734  iscygodd  18735  gsumzadd  18767  gsumconst  18779  gsumpt  18807  gsum2dlem2  18816  gsum2d  18817  gsum2d2lem  18818  dprdfcntz  18859  eldprdi  18862  subgdmdprd  18878  subgdprd  18879  dprdpr  18894  ablfac1c  18915  ablfac1eu  18917  ablfaclem3  18931  ring1  19047  kerf1ghm  19192  kerf1hrmOLD  19193  issubdrg  19255  rhmeql  19260  rhmima  19261  cntzsubr  19263  isabvd  19286  abvdiv  19303  lsslsp  19482  lmhmima  19514  lmhmpreima  19515  lmhmeql  19522  lsmcl  19550  lspfixed  19595  issubassa  19791  issubassa2  19818  snifpsrbag  19839  psrbaglesupp  19841  psrbaglecl  19842  psrbagaddcl  19843  psrbagcon  19844  mplsubglem  19907  mpllsslem  19908  mplassa  19927  subrgmpl  19933  mplcoe5  19941  mplbas2  19943  mplind  19974  evlslem3  19986  mpfind  20008  mhp0cl  20025  mhpaddcl  20026  mhpinvcl  20027  mhpvscacl  20029  mhplss  20030  ply1assa  20055  coe1tmmul2  20132  coe1tmmul  20133  cply1coe0bi  20156  qsssubdrg  20291  gzrngunit  20298  evpmodpmf1o  20427  ocvpj  20548  dsmm0cl  20571  dsmmacl  20572  dsmmsubg  20574  dsmmlss  20575  frlmsplit2  20604  uvcff  20622  lindfrn  20652  f1lindf  20653  lindsss  20655  mat1rngiso  20784  dmatid  20793  dmatsubcl  20796  dmatscmcl  20801  scmatid  20812  scmataddcl  20814  scmatsubcl  20815  scmatmulcl  20816  smatvscl  20822  scmatrhmcl  20826  scmatrngiso  20834  mat0scmat  20836  mat1scmat  20837  mdet0pr  20890  m2cpmrngiso  21055  pm2mprngiso  21119  chmaidscmat  21145  distop  21292  indistopon  21298  ppttop  21304  epttop  21306  mretopd  21389  toponmre  21390  neiss  21406  opnneissb  21411  ssnei2  21413  innei  21422  neiptoptop  21428  ordtcld1  21494  ordtcld2  21495  lmconst  21558  cnpnei  21561  iscncl  21566  cnss1  21573  cnss2  21574  cncnpi  21575  cncnp  21577  cnconst2  21580  cnrest  21582  cnpresti  21585  cnpdis  21590  paste  21591  lmcnp  21601  cnhaus  21651  hauscmp  21704  2ndcomap  21755  1stcelcls  21758  1stccnp  21759  llyrest  21782  nllyrest  21783  llyidm  21785  nllyidm  21786  ssref  21809  reftr  21811  refun0  21812  dissnref  21825  kgentopon  21835  kgenidm  21844  kgencn3  21855  txcld  21900  neitx  21904  tx1cn  21906  tx2cn  21907  ptcld  21910  xkoccn  21916  txcnp  21917  ptcnp  21919  txcnmpt  21921  ptcn  21924  txdis1cn  21932  ptrescn  21936  txkgen  21949  xkoco1cn  21954  xkoco2cn  21955  xkococn  21957  xkoinjcn  21984  qtoptop2  21996  qtopuni  21999  qtopid  22002  qtopkgen  22007  basqtop  22008  tgqtop  22009  qtopss  22012  qtopeu  22013  qtoprest  22014  kqopn  22031  kqcld  22032  kqreglem2  22039  reghmph  22090  ordthmeolem  22098  qtopf1  22113  opnfbas  22139  isfil2  22153  fbasweak  22162  fsubbas  22164  filconn  22180  fbasrn  22181  rnelfmlem  22249  flimss2  22269  flimss1  22270  hausflim  22278  flimclslem  22281  flimsncls  22283  cnpflfi  22296  flfcnp2  22304  fclsfnflim  22324  cnextfvval  22362  cnextfres1  22365  symgtgp  22398  opnsubg  22404  ghmcnp  22411  qustgpopn  22416  qustgplem  22417  qustgphaus  22419  tsmsfbas  22424  ustfilxp  22509  utoptop  22531  utopbas  22532  restutopopn  22535  iducn  22580  cstucnd  22581  ucncn  22582  fmucnd  22589  cfilufg  22590  trcfilu  22591  cfiluweak  22592  neipcfilu  22593  psmetres2  22612  isxmetd  22624  xmetpsmet  22646  imasf1oxmet  22673  xblss2ps  22699  xblss2  22700  xblcntrps  22708  xblcntr  22709  blcld  22803  metustfbas  22855  cfilucfil  22857  restmetu  22868  ngptgp  22933  tngngpd  22950  nrmtngnrm  22955  tngnrg  22971  nlmvscn  22984  nrginvrcn  22989  nmo0  23032  nmoeq0  23033  nmoid  23039  nghmcn  23042  0nmhm  23052  blcvx  23094  iccntr  23117  xrge0tsms  23130  xmetdcn2  23133  metdstri  23147  metdscn  23152  rescncf  23193  cncfco  23203  oprpiece1res2  23244  cnheibor  23247  cnllycmp  23248  bndth  23250  ishtpyd  23267  isphtpyd  23278  pcoval2  23308  nmhmcn  23412  ipcn  23537  lmnn  23554  cfilss  23561  iscfil3  23564  cfilfcls  23565  cmetcaulem  23579  iscmet3lem2  23583  cfilres  23587  lmcau  23604  flimcfil  23605  cncmet  23613  rlmbn  23652  minveclem3b  23719  pjthlem1  23728  pjth2  23731  ivthlem3  23742  ovolssnul  23776  ovolctb  23779  ovoliunnul  23796  ovolsca  23804  ovolicopnf  23813  voliunlem2  23840  volsup  23845  dyadmaxlem  23886  vitalilem5  23901  mbfres  23933  mbfss  23935  mbfmulc2re  23937  mbfadd  23950  mbfmulc2  23952  mbflim  23957  i1faddlem  23982  i1fmullem  23983  mbfmul  24015  itg2mulc  24036  itg2cnlem1  24050  ibl0  24075  iblposlem  24080  itgreval  24085  iblneg  24091  iblss  24093  iblss2  24094  itgle  24098  iblconst  24106  iblabs  24117  iblabsr  24118  iblmulc2  24119  bddmulibl  24127  limciun  24180  limcun  24181  dvres2lem  24196  dvidlem  24201  dvcnp2  24205  dvcn  24206  cpnres  24222  dvaddbr  24223  dvmulbr  24224  dvcobr  24231  dvcjbr  24234  dvrec  24240  dvcnvlem  24261  dvferm  24273  dvlip2  24280  dveq0  24285  dv11cn  24286  dvivthlem1  24293  lhop1  24299  lhop2  24300  lhop  24301  dvcnvre  24304  dvfsumlem3  24313  dvfsumlem4  24314  dvfsumrlim  24316  dvfsum2  24319  ftc1a  24322  ftc1lem4  24324  ftc1lem6  24326  ftc1  24327  coe1mul3  24381  deg1addle2  24384  deg1sublt  24392  fta1blem  24450  drnguc1p  24452  ig1prsp  24459  plyco0  24470  plyeq0lem  24488  dgrub  24512  dgreq  24522  dgradd2  24546  dgrmul  24548  dgrcolem2  24552  dgrco  24553  plycpn  24566  plydivlem4  24573  plydiveu  24575  vieta1lem2  24588  vieta1  24589  aalioulem2  24610  aalioulem3  24611  aaliou3lem7  24626  tayl0  24638  ulmcn  24675  ulmdvlem3  24678  psercn  24702  abelth  24717  pilem3  24729  efif1olem1  24812  abslogimle  24843  argregt0  24879  argrege0  24880  logf1o2  24919  cxpsqrtlem  24971  cxpcn3  25015  abscxpbnd  25020  logreclem  25026  ang180lem2  25074  ang180lem3  25075  xrlimcnp  25233  harmonicbnd4  25275  fsumharmonic  25276  lgamgulmlem5  25297  lgambdd  25301  basellem3  25347  basellem4  25348  dvdsppwf1o  25450  dvdsflf1o  25451  fsumfldivdiaglem  25453  chpeq0  25471  chteq0  25472  chtub  25475  chpub  25483  dchrelbasd  25502  dchrmulcl  25512  dchrinv  25524  bcmono  25540  bposlem1  25547  bposlem2  25548  lgsdirprm  25594  lgsqrlem2  25610  lgsqrlem3  25611  lgsdchr  25618  lgseisenlem1  25638  lgseisenlem2  25639  lgseisenlem3  25640  lgsquadlem1  25643  2sqlem8  25689  2sqblem  25694  2sqmod  25699  chebbnd1lem1  25732  dchrisumlem1  25752  dchrisumlem2  25753  dchrisumlem3  25754  dchrisum0fno1  25774  pntrmax  25827  pntpbnd1a  25848  pntibndlem3  25855  pntlemn  25863  pntlemi  25867  pntlem3  25872  pntleml  25874  ostth1  25896  ostth2  25900  ostth3  25901  ercgrg  25990  motco  26013  cnvmot  26014  legso  26072  mirmot  26148  colopp  26242  hphl  26244  lmicom  26261  lmimid  26267  lmimot  26271  hypcgrlem1  26272  hypcgrlem2  26273  trgcopyeulem  26278  inagswap  26315  inaghl  26319  cgrg3col4  26327  brbtwn2  26379  axlowdimlem3  26418  axlowdimlem16  26431  axcontlem8  26445  fusgrfis  26800  nbgr2vtx1edg  26820  0vtxrgr  27046  0vtxrusgr  27047  ewlkle  27075  wlk1ewlk  27109  uspgr2wlkeq2  27116  wlkp1lem8  27152  trlontrl  27184  pthonpth  27221  pthdlem2  27241  wlklnwwlkln1  27338  wlknewwlksn  27357  wwlksnred  27362  wwlksnredwwlkn0  27366  2trlond  27410  2pthond  27413  elwwlks2ons3im  27425  clwlkclwwlklem2a1  27462  clwlkclwwlkf1  27480  clwwlkel  27517  wwlksext2clwwlk  27528  1ewlk  27586  0trlon  27595  0pthon  27598  1pthond  27615  3trlond  27644  3pthond  27646  3spthond  27648  eupthresOLD  27686  eupthres  27687  2clwwlk2clwwlk  27826  numclwwlk1lem2foa  27830  numclwwlk1lem2f1  27833  nvabs  28145  vacn  28167  nmcvcn  28168  nmblore  28259  0lno  28263  0blo  28265  nmlno0lem  28266  occl  28777  pjhthlem1  28864  pjpjpre  28892  nmopre  29343  nmlnop0iALT  29468  nmophmi  29504  leoprf2  29600  stlesi  29714  disjdifprg  30020  disjun0  30040  fsuppcurry1  30154  fsuppcurry2  30155  fpwrelmap  30162  fzspl  30204  ogrpaddlt  30383  ogrpsublt  30387  evpmid  30433  pnfinf  30455  xrge0tsmsd  30508  rmfsupp2  30525  ornglmullt  30539  orngrmullt  30540  orngmullt  30541  ofldlt1  30545  isarchiofld  30549  lbsdiflsp0  30631  fedgmul  30636  fldexttr  30657  fldextid  30658  psgnfzto1stlem  30669  fzto1st1  30671  qtopt1  30721  reff  30725  locfinreflem  30726  metideq  30755  metider  30756  pstmxmet  30759  qqhval2lem  30844  qqhcn  30854  qqhucn  30855  pwsiga  31011  prsiga  31012  measle0  31089  mbfmcst  31139  1stmbfm  31140  2ndmbfm  31141  imambfm  31142  cnmbfm  31143  mbfmco  31144  mbfmco2  31145  0elcarsg  31187  carsgclctun  31201  sibfof  31220  oddpwdc  31234  eulerpartlemmf  31255  eulerpartlemgs2  31260  0rrv  31331  ballotlemfc0  31372  ballotlemfcc  31373  signstfveq0  31469  breprexplemc  31525  bnj1452  31943  usgrgt2cycl  31991  acycgr1v  32010  derangen  32033  subfacval3  32050  cvmseu  32137  cvmliftmolem2  32143  cvmliftlem7  32152  cvmliftlem15  32159  cvmlift2lem9a  32164  cvmlift2lem9  32172  cvmlift2lem10  32173  cvmlift2lem11  32174  cvmlift2lem12  32175  cvmlift3lem6  32185  cvmlift3lem8  32187  ex-sategoelel  32282  ex-sategoelelomsuc  32287  mclsppslem  32444  mclspps  32445  wsuclem  32727  fpr3g  32737  frrlem4  32741  nosepon  32787  nolesgn2ores  32794  nosupres  32822  nosupbnd1lem2  32824  nosupbnd2lem1  32830  fness  33312  fnetr  33314  fnessref  33320  refssfne  33321  neibastop1  33322  neibastop2  33324  tailfb  33340  filnetlem3  33343  bj-finsumval0  34144  dfgcd3  34161  lindsadd  34441  poimirlem13  34461  poimirlem15  34463  poimirlem17  34465  poimirlem24  34472  poimirlem28  34476  mblfinlem2  34486  ovoliunnfl  34490  volsupnfl  34493  mbfresfi  34494  itg2addnclem2  34500  iblabsnc  34512  iblmulc2nc  34513  ftc1cnnclem  34521  ftc1cnnc  34522  ftc1anc  34531  sdclem2  34574  metf1o  34587  ismtyhmeolem  34639  ismtyres  34643  heibor1lem  34644  bfplem2  34658  bfp  34659  rrncmslem  34667  iccbnd  34675  icccmpALT  34676  rngogrphom  34806  rngoisoco  34817  keridl  34867  lsmcv2  35721  lsatcv0  35723  lcvexchlem4  35729  lcvexchlem5  35730  l1cvpat  35746  lfl0f  35761  lfladdcl  35763  lflnegcl  35767  lkrlss  35787  eqlkr  35791  lkrlsp  35794  lkrlsp2  35795  lshpkrcl  35808  lkrin  35856  1cvrjat  36167  llni  36200  llnle  36210  lplni  36224  lplnle  36232  llncvrlpln2  36249  2atmat  36253  lvoli  36267  lplncvrlvol2  36307  elpaddri  36494  paddclN  36534  pclclN  36583  pclfinN  36592  0psubclN  36635  1psubclN  36636  atpsubclN  36637  pmapsubclN  36638  osumclN  36659  pexmidN  36661  pexmidlem6N  36667  lhp2lt  36693  lautcnv  36782  idlaut  36788  lautco  36789  idldil  36806  ldilcnv  36807  ldilco  36808  ltrncnv  36838  idltrn  36842  cdleme16d  36973  cdleme50laut  37239  cdleme50ldil  37240  cdleme50ltrn  37249  ltrnco  37411  dian0  37731  dia0eldmN  37732  dia1eldmN  37733  dialss  37738  diaintclN  37750  docaclN  37816  doca2N  37818  djajN  37829  dibintclN  37859  diblss  37862  dicvaddcl  37882  dicvscacl  37883  dicn0  37884  cdlemn11a  37899  dihord2cN  37913  dihord11b  37914  dihord6apre  37948  dihmeetlem1N  37982  dihglblem5apreN  37983  dihpN  38028  dihjatcclem4  38113  dochkr1  38170  islpoldN  38176  lcfrlem31  38265  mapdpglem18  38381  mapdheq2  38421  mapdheq4  38424  mapdh6aN  38427  hdmap1l6a  38501  hdmap14lem4a  38563  frlmfzoccat  38696  prjspvs  38782  fzsplit1nn0  38861  irrapxlem3  38931  irrapxlem4  38932  pell1234qrdich  38968  pell1qr1  38978  pell14qrgap  38982  pellqrexplicit  38984  rmspecfund  39016  fzmaxdif  39088  acongeq  39090  jm2.23  39103  jm3.1  39127  lmhmlnmsplit  39197  hbt  39240  dgrsub2  39245  proot1ex  39311  clublem  39480  dftrcl3  39575  mnugrud  40142  hashnzfz2  40216  dvconstbi  40229  ubelsupr  40841  wessf1ornlem  41010  lefldiveq  41125  iccintsng  41366  fmul01  41428  fmuldfeq  41431  climsuse  41456  mullimc  41464  limcdm0  41466  limccog  41468  mullimcf  41471  constlimc  41472  idlimc  41474  limcperiod  41476  limsupre  41489  limcleqr  41492  neglimc  41495  addlimc  41496  0ellimcdiv  41497  xlimliminflimsup  41710  cncfshift  41724  cncfperiod  41729  cncfuni  41736  icccncfext  41737  cncfiooicclem1  41743  fperdvper  41770  ioodvbdlimc1lem2  41784  ioodvbdlimc2lem  41786  mbfres2cn  41810  iblsplit  41818  stoweidlem7  41860  stoweidlem13  41866  stoweidlem26  41879  wallispilem3  41920  stirlinglem6  41932  stirlinglem10  41936  dirkercncf  41960  fourierdlem6  41966  fourierdlem11  41971  fourierdlem12  41972  fourierdlem15  41975  fourierdlem26  41986  fourierdlem42  42002  fourierdlem50  42009  fourierdlem51  42010  fourierdlem52  42011  fourierdlem54  42013  fourierdlem62  42021  fourierdlem79  42038  fourierdlem102  42061  fourierdlem114  42073  etransclem23  42110  zgeltp1eq  43051  setsnidel  43079  iccpartres  43086  prpair  43171  fpprel2  43414  rabsubmgmd  43566  submgmid  43568  subsubmgm  43572  mgmhmima  43577  mgmhmeql  43578  isassintop  43621  rnghmsscmap2  43748  rnghmsscmap  43749  rnghmsubcsetc  43752  zrzeroorngc  43777  rhmsscmap2  43794  rhmsscmap  43795  rhmsubcsetc  43798  rhmsscrnghm  43801  rhmsubcrngc  43804  srhmsubc  43851  fldhmsubc  43859  rhmsubc  43865  srhmsubcALTV  43869  fldhmsubcALTV  43877  rhmsubcALTV  43883  rmfsupp  43928  mndpfsupp  43930  scmfsupp  43932  mptcfsupp  43934  lcoel0  43989  lincsumcl  43992  lincscmcl  43993  lcoss  43997  lindsrng01  44029  lincreslvec3  44043  lindssnlvec  44047  zgtp1leeq  44083