Theorem mpbir2and 695

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

Syntax hints:   → wi 4   ↔ wb 197   ∧ wa 384

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 198  df-an 385

This theorem is referenced by:  fveqressseq  6573  fmptsng  6655  fmptsnd  6656  fnprb  6693  fntpb  6694  fdmfifsupp  8520  fczfsuppd  8528  fsuppmptif  8540  fsuppco2  8543  fsuppcor  8544  dffi3  8572  suppr  8612  infpr  8644  ordtypelem7  8664  cantnf0  8815  cantnfp1lem1  8818  cantnfp1lem2  8819  cantnfp1lem3  8820  cantnflem1a  8825  cantnflem1d  8828  cantnflem1  8829  cantnf  8833  rankpwi  8929  carduni  9086  fin23lem32  9447  fpwwe2lem6  9738  fpwwe2lem9  9741  fpwwe2lem12  9744  fpwwe2lem13  9745  fpwwe2  9746  inttsk  9877  grutsk1  9924  add20  10821  supaddc  11271  supadd  11272  supmul  11276  suprzcl  11719  uzwo3  11998  rpnnen1lem5  12033  xrre  12214  xrre3  12216  xleadd1a  12297  xlemul1a  12332  supxrre  12371  ixxub  12410  elioc2  12450  elico2  12451  elicc2  12452  elfz1eq  12571  fzadd2  12595  fznatpl1  12614  elfz1uz  12629  nn0fz0  12657  fzctr  12671  fzo1fzo0n0  12739  fzoaddel  12741  elincfzoext  12746  flid  12829  flval3  12836  fladdz  12846  fldiv  12879  modid  12915  seqf1olem1  13059  bcval5  13321  hashf1lem1  13452  eqs1  13603  wwlktovf1  13921  sqeqd  14125  sqrlem7  14208  max0add  14269  abs2difabs  14293  rddif  14299  fzomaxdiflem  14301  rexico  14312  icodiamlt  14393  limsupgre  14431  rlim3  14448  icco1  14490  rlimclim  14496  rlimuni  14500  rlimresb  14515  isercolllem2  14615  isercolllem3  14616  isercoll  14617  caucvgrlem  14622  caurcvgr  14623  iseraltlem3  14633  fsum00  14748  o1fsum  14763  bitsfzolem  15371  bitsfzo  15372  bitsmod  15373  bitscmp  15375  gcd0id  15455  gcdneg  15458  bezoutlem4  15474  nn0seqcvgd  15498  lcmneg  15531  qredeq  15585  prmind2  15612  isprm5  15632  hashdvds  15693  eulerthlem2  15700  pcpremul  15761  pcidlem  15789  pcgcd1  15794  pcadd2  15807  fldivp1  15814  pcfaclem  15815  prmreclem5  15837  4sqlem17  15878  vdwlem1  15898  vdwlem6  15903  vdwlem12  15909  vdwlem13  15910  0ram  15937  ram0  15939  ramub1lem1  15943  invco  16631  sectmon  16642  monsect  16643  invid  16647  cicref  16661  ssctr  16685  ssceq  16686  0ssc  16697  0subcat  16698  catsubcat  16699  issubc3  16709  fullsubc  16710  funcinv  16733  fthmon  16787  fuccocl  16824  fucidcl  16825  invfuc  16834  2initoinv  16860  2termoinv  16867  elhomai  16883  setcmon  16937  setcepi  16938  catcisolem  16956  curf2cl  17072  yonedalem4c  17118  yonedalem3  17121  yoniso  17126  lublecl  17190  isacs3lem  17367  tsrdir  17439  mnd1  17532  sgrp2nmndlem4  17616  sgrp2nmndlem5  17617  nmznsg  17836  ghmpreima  17880  ghmeql  17881  ghmnsgpreima  17883  cntzsubm  17965  cntzsubg  17966  cntzmhm  17968  symgextfo  18039  symgfixf1  18054  symgfixfolem1  18055  odlem2  18155  gexlem2  18194  gexcl2  18201  sylow1lem5  18214  subgslw  18228  slwhash  18236  fislw  18237  sylow3lem1  18239  lsmsubg  18266  efgredlemd  18354  efgredlem  18357  efgcpbllemb  18365  frgpuplem  18382  cyggeninv  18482  iscygd  18486  iscygodd  18487  gsumzadd  18519  gsumconst  18531  gsumpt  18558  gsum2dlem2  18567  gsum2d  18568  gsum2d2lem  18569  dprdfcntz  18612  eldprdi  18615  subgdmdprd  18631  subgdprd  18632  dprdpr  18647  ablfac1c  18668  ablfac1eu  18670  ablfaclem3  18684  ring1  18800  kerf1hrm  18943  issubdrg  19005  rhmeql  19010  rhmima  19011  cntzsubr  19012  isabvd  19020  abvdiv  19037  lsslsp  19218  lmhmima  19250  lmhmpreima  19251  lmhmeql  19258  lsmcl  19286  lspfixed  19331  lspfixedOLD  19332  issubassa  19529  issubassa2  19550  snifpsrbag  19571  psrbaglesupp  19573  psrbaglecl  19574  psrbagaddcl  19575  psrbagcon  19576  mplsubglem  19639  mpllsslem  19640  mplassa  19659  subrgmpl  19665  mplcoe5  19673  mplbas2  19675  mplind  19706  evlslem3  19718  mpfind  19740  ply1assa  19773  coe1tmmul2  19850  coe1tmmul  19851  cply1coe0bi  19874  qsssubdrg  20009  gzrngunit  20016  evpmodpmf1o  20146  ocvpj  20267  dsmm0cl  20290  dsmmacl  20291  dsmmsubg  20293  dsmmlss  20294  frlmsplit2  20318  uvcff  20336  lindfrn  20366  f1lindf  20367  lindsss  20369  mat1rngiso  20499  dmatid  20508  dmatsubcl  20511  dmatscmcl  20516  scmatid  20527  scmataddcl  20529  scmatsubcl  20530  scmatmulcl  20531  smatvscl  20537  scmatrhmcl  20541  scmatrngiso  20549  mat0scmat  20551  mat1scmat  20552  mdet0pr  20605  m2cpmrngiso  20772  pm2mprngiso  20836  chmaidscmat  20862  fvmptnn04if  20863  distop  21009  indistopon  21015  ppttop  21021  epttop  21023  mretopd  21106  toponmre  21107  neiss  21123  opnneissb  21128  ssnei2  21130  innei  21139  neiptoptop  21145  ordtcld1  21211  ordtcld2  21212  lmconst  21275  cnpnei  21278  iscncl  21283  cnss1  21290  cnss2  21291  cncnpi  21292  cncnp  21294  cnconst2  21297  cnrest  21299  cnpresti  21302  cnpdis  21307  paste  21308  lmcnp  21318  cnhaus  21368  hauscmp  21420  2ndcomap  21471  1stcelcls  21474  1stccnp  21475  llyrest  21498  nllyrest  21499  llyidm  21501  nllyidm  21502  ssref  21525  reftr  21527  refun0  21528  dissnref  21541  kgentopon  21551  kgenidm  21560  kgencn3  21571  txcld  21616  neitx  21620  tx1cn  21622  tx2cn  21623  ptcld  21626  xkoccn  21632  txcnp  21633  ptcnp  21635  txcnmpt  21637  ptcn  21640  txdis1cn  21648  ptrescn  21652  txkgen  21665  xkoco1cn  21670  xkoco2cn  21671  xkococn  21673  xkoinjcn  21700  qtoptop2  21712  qtopuni  21715  qtopid  21718  qtopkgen  21723  basqtop  21724  tgqtop  21725  qtopss  21728  qtopeu  21729  qtoprest  21730  kqopn  21747  kqcld  21748  kqreglem2  21755  reghmph  21806  ordthmeolem  21814  qtopf1  21829  opnfbas  21855  isfil2  21869  fbasweak  21878  fsubbas  21880  filconn  21896  fbasrn  21897  rnelfmlem  21965  flimss2  21985  flimss1  21986  hausflim  21994  flimclslem  21997  flimsncls  21999  cnpflfi  22012  flfcnp2  22020  fclsfnflim  22040  cnextfvval  22078  cnextfres1  22081  symgtgp  22114  opnsubg  22120  ghmcnp  22127  qustgpopn  22132  qustgplem  22133  qustgphaus  22135  tsmsfbas  22140  ustfilxp  22225  utoptop  22247  utopbas  22248  restutopopn  22251  iducn  22296  cstucnd  22297  ucncn  22298  fmucnd  22305  cfilufg  22306  trcfilu  22307  cfiluweak  22308  neipcfilu  22309  psmetsym  22324  psmetres2  22328  isxmetd  22340  xmetsym  22361  xmetpsmet  22362  imasf1oxmet  22389  xblss2ps  22415  xblss2  22416  xblcntrps  22424  xblcntr  22425  blcld  22519  metustfbas  22571  cfilucfil  22573  restmetu  22584  ngptgp  22649  tngngpd  22666  nrmtngnrm  22671  tngnrg  22687  nlmvscn  22700  nrginvrcn  22705  nmo0  22748  nmoeq0  22749  nmoid  22755  nghmcn  22758  0nmhm  22768  blcvx  22810  zcld  22825  iccntr  22833  xrge0tsms  22846  xmetdcn2  22849  metdstri  22863  metdscn  22868  rescncf  22909  cncfco  22919  oprpiece1res2  22960  cnheibor  22963  cnllycmp  22964  bndth  22966  evth  22967  ishtpyd  22983  isphtpyd  22994  pcoval2  23024  nmhmcn  23128  ipcn  23253  lmnn  23269  cfilss  23276  iscfil3  23279  cfilfcls  23280  cmetcaulem  23294  iscmet3lem2  23298  cfilres  23302  lmcau  23319  flimcfil  23320  cncmet  23327  rlmbn  23365  minveclem3b  23407  pjthlem1  23416  pjth2  23419  ivthlem3  23430  ovolssnul  23464  ovolctb  23467  ovolunnul  23477  ovoliunnul  23484  ovolsca  23492  ovolicc  23500  ovolicopnf  23501  voliunlem2  23528  voliunlem3  23529  volsup  23533  uniioovol  23556  uniiccvol  23557  dyadmaxlem  23574  vitalilem5  23589  ismbfd  23616  mbfres  23621  mbfss  23623  mbfmulc2re  23625  mbfadd  23638  mbfmulc2  23640  mbflim  23645  i1faddlem  23670  i1fmullem  23671  mbfmul  23703  itg2itg1  23713  itg2seq  23719  itg2eqa  23722  itg2mulc  23724  itg2split  23726  itg2mono  23730  itg2cnlem1  23738  ibl0  23763  iblposlem  23768  itgreval  23773  iblneg  23779  iblss  23781  iblss2  23782  itgle  23786  iblconst  23794  iblabs  23805  iblabsr  23806  iblmulc2  23807  bddmulibl  23815  limciun  23868  limcun  23869  dvres2lem  23884  dvidlem  23889  dvcnp2  23893  dvcn  23894  cpnres  23910  dvaddbr  23911  dvmulbr  23912  dvcobr  23919  dvcjbr  23922  dvrec  23928  dvcnvlem  23949  dvferm  23961  dvlip2  23968  dveq0  23973  dv11cn  23974  dvivthlem1  23981  lhop1  23987  lhop2  23988  lhop  23989  dvcnvre  23992  dvfsumlem3  24001  dvfsumlem4  24002  dvfsumrlim  24004  dvfsum2  24007  ftc1a  24010  ftc1lem4  24012  ftc1lem6  24014  ftc1  24015  coe1mul3  24069  deg1addle2  24072  deg1add  24073  deg1sublt  24080  deg1mul2  24084  deg1tm  24088  fta1blem  24138  drnguc1p  24140  ig1prsp  24147  plyco0  24158  plyeq0lem  24176  dgrub  24200  dgreq  24210  dgradd2  24234  dgrmul  24236  dgrcolem2  24240  dgrco  24241  plycpn  24254  plydivlem4  24261  plydiveu  24263  vieta1lem2  24276  vieta1  24277  aalioulem2  24298  aalioulem3  24299  aaliou3lem7  24314  tayl0  24326  ulmcn  24363  ulmdvlem3  24366  psercn  24390  abelth  24405  pilem3  24417  pilem3OLD  24418  efif1olem1  24499  abslogimle  24530  argregt0  24566  argrege0  24567  logf1o2  24606  cxpsqrtlem  24658  cxpcn3  24699  abscxpbnd  24704  logreclem  24710  ang180lem2  24750  ang180lem3  24751  xrlimcnp  24905  harmonicbnd4  24947  fsumharmonic  24948  lgamgulmlem5  24969  lgambdd  24973  basellem3  25019  basellem4  25020  dvdsppwf1o  25122  dvdsflf1o  25123  fsumfldivdiaglem  25125  chpeq0  25143  chteq0  25144  chtub  25147  chpub  25155  dchrelbasd  25174  dchrmulcl  25184  dchrinv  25196  bcmono  25212  bposlem1  25219  bposlem2  25220  lgslem1  25232  lgsdirprm  25266  lgsqrlem2  25282  lgsqrlem3  25283  lgsdchr  25290  lgseisenlem1  25310  lgseisenlem2  25311  lgseisenlem3  25312  lgsquadlem1  25315  2sqlem8  25361  2sqblem  25366  chebbnd1lem1  25368  dchrisumlem1  25388  dchrisumlem2  25389  dchrisumlem3  25390  dchrisum0fno1  25410  pntrmax  25463  pntpbnd1a  25484  pntibndlem3  25491  pntlemn  25499  pntlemi  25503  pntlem3  25508  pntleml  25510  ostth1  25532  ostth2  25536  ostth3  25537  ercgrg  25622  motco  25645  cnvmot  25646  legso  25704  mirmot  25780  lmicom  25890  lmimid  25896  lmimot  25900  hypcgrlem1  25901  hypcgrlem2  25902  ttgcontlem1  25975  brbtwn2  25995  axlowdimlem3  26034  axlowdimlem16  26047  axcontlem8  26061  fusgrfis  26434  nbgr2vtx1edg  26458  0vtxrgr  26696  0vtxrusgr  26697  ewlkle  26725  wlk1ewlk  26760  uspgr2wlkeq2  26767  wlkp1lem8  26801  trlontrl  26831  pthonpth  26868  pthdlem2  26888  wlklnwwlkln1  26991  wlknewwlksn  27010  wwlksnred  27025  wwlksnredwwlkn0  27029  2trlond  27075  2pthond  27078  elwwlks2ons3im  27090  elwwlks2ons3OLD  27092  clwlkclwwlklem2a1  27131  clwlkclwwlkf1  27149  clwwlkel  27191  wwlksext2clwwlk  27203  wwlksext2clwwlkOLD  27204  clwlksf1clwwlkOLD  27239  0trlon  27293  0pthon  27296  1pthond  27313  3trlond  27342  3pthond  27344  3spthond  27346  eupthres  27384  2clwwlk2clwwlk  27523  numclwwlk1lem2foa  27529  numclwwlk1lem2f1  27532  nvabs  27851  vacn  27873  nmcvcn  27874  nmblore  27965  0lno  27969  0blo  27971  nmlno0lem  27972  occl  28487  pjhthlem1  28574  pjpjpre  28602  nmopre  29053  nmlnop0iALT  29178  nmophmi  29214  leoprf2  29310  stlesi  29424  disjdifprg  29709  disjun0  29729  fpwrelmap  29831  fzspl  29873  2sqmod  29969  ogrpaddlt  30039  ogrpsublt  30043  pnfinf  30058  xrge0tsmsd  30106  ornglmullt  30128  orngrmullt  30129  orngmullt  30130  ofldlt1  30134  isarchiofld  30138  psgnfzto1stlem  30171  fzto1st1  30173  qtopt1  30223  reff  30227  locfinreflem  30228  metideq  30257  metider  30258  pstmxmet  30261  qqhval2lem  30346  qqhcn  30356  qqhucn  30357  pwsiga  30514  prsiga  30515  measle0  30592  mbfmcst  30642  1stmbfm  30643  2ndmbfm  30644  imambfm  30645  cnmbfm  30646  mbfmco  30647  mbfmco2  30648  0elcarsg  30690  carsgclctun  30704  sibfof  30723  oddpwdc  30737  eulerpartlemmf  30758  eulerpartlemgs2  30763  0rrv  30834  ballotlemfc0  30875  ballotlemfcc  30876  signstfveq0  30975  breprexplemc  31031  bnj1452  31438  derangen  31472  subfacval3  31489  cvmseu  31576  cvmliftmolem2  31582  cvmliftlem7  31591  cvmliftlem15  31598  cvmlift2lem9a  31603  cvmlift2lem9  31611  cvmlift2lem10  31612  cvmlift2lem11  31613  cvmlift2lem12  31614  cvmlift3lem6  31624  cvmlift3lem8  31626  mclsppslem  31798  mclspps  31799  wsuclem  32086  frrlem4  32099  nosepon  32134  nolesgn2ores  32141  nosupres  32169  nosupbnd1lem2  32171  nosupbnd2lem1  32177  fness  32660  fnetr  32662  fnessref  32668  refssfne  32669  neibastop1  32670  neibastop2  32672  tailfb  32688  filnetlem3  32691  bj-finsumval0  33459  dfgcd3  33482  poimirlem13  33730  poimirlem15  33732  poimirlem17  33734  poimirlem24  33741  poimirlem28  33745  mblfinlem2  33755  ovoliunnfl  33759  volsupnfl  33762  mbfresfi  33763  itg2addnclem2  33769  iblabsnc  33781  iblmulc2nc  33782  ftc1cnnclem  33790  ftc1cnnc  33791  ftc1anc  33800  sdclem2  33844  metf1o  33857  ismtyhmeolem  33909  ismtyres  33913  heibor1lem  33914  bfplem2  33928  bfp  33929  rrncmslem  33937  iccbnd  33945  icccmpALT  33946  rngogrphom  34076  rngoisoco  34087  keridl  34137  lsmcv2  34804  lsatcv0  34806  lcvexchlem4  34812  lcvexchlem5  34813  l1cvpat  34829  lfl0f  34844  lfladdcl  34846  lflnegcl  34850  lkrlss  34870  eqlkr  34874  lkrlsp  34877  lkrlsp2  34878  lshpkrcl  34891  lkrin  34939  1cvrjat  35250  llni  35283  llnle  35293  lplni  35307  lplnle  35315  llncvrlpln2  35332  2atmat  35336  lvoli  35350  lplncvrlvol2  35390  elpaddri  35577  paddclN  35617  pclclN  35666  pclfinN  35675  0psubclN  35718  1psubclN  35719  atpsubclN  35720  pmapsubclN  35721  osumclN  35742  pexmidN  35744  pexmidlem6N  35750  lhp2lt  35776  lautcnv  35865  idlaut  35871  lautco  35872  idldil  35889  ldilcnv  35890  ldilco  35891  ltrncnv  35921  idltrn  35925  cdleme16d  36056  cdleme50laut  36322  cdleme50ldil  36323  cdleme50ltrn  36332  ltrnco  36494  dian0  36814  dia0eldmN  36815  dia1eldmN  36816  dialss  36821  diaintclN  36833  docaclN  36899  doca2N  36901  djajN  36912  dibintclN  36942  diblss  36945  dicvaddcl  36965  dicvscacl  36966  dicn0  36967  cdlemn11a  36982  dihord2cN  36996  dihord11b  36997  dihord6apre  37031  dihmeetlem1N  37065  dihglblem5apreN  37066  dihpN  37111  dihjatcclem4  37196  dochkr1  37253  islpoldN  37259  lcfrlem31  37348  mapdpglem18  37464  mapdheq2  37504  mapdheq4  37507  mapdh6aN  37510  hdmap1l6a  37584  hdmap14lem4a  37646  fzsplit1nn0  37813  irrapxlem3  37884  irrapxlem4  37885  pell1234qrdich  37921  pell1qr1  37931  pell14qrgap  37935  pellqrexplicit  37937  rmspecfund  37969  fzmaxdif  38043  acongeq  38045  jm2.23  38058  jm3.1  38082  lmhmlnmsplit  38152  hbt  38195  dgrsub2  38200  proot1ex  38274  clublem  38411  dftrcl3  38506  hashnzfz2  39014  dvconstbi  39027  ubelsupr  39667  lefldiveq  39981  iccintsng  40224  fmul01  40286  fmuldfeq  40289  climsuse  40314  mullimc  40322  limcdm0  40324  limccog  40326  mullimcf  40329  constlimc  40330  idlimc  40332  limcperiod  40334  limsupre  40347  limcleqr  40350  neglimc  40353  addlimc  40354  0ellimcdiv  40355  cncfshift  40561  cncfperiod  40566  cncfuni  40573  icccncfext  40574  cncfiooicclem1  40580  fperdvper  40607  ioodvbdlimc1lem2  40621  ioodvbdlimc2lem  40623  mbfres2cn  40647  iblsplit  40655  stoweidlem7  40697  stoweidlem13  40703  stoweidlem26  40716  wallispilem3  40757  stirlinglem6  40769  stirlinglem10  40773  dirkercncf  40797  fourierdlem6  40803  fourierdlem11  40808  fourierdlem12  40809  fourierdlem15  40812  fourierdlem26  40823  fourierdlem42  40839  fourierdlem50  40846  fourierdlem51  40847  fourierdlem52  40848  fourierdlem54  40850  fourierdlem62  40858  fourierdlem79  40875  fourierdlem102  40898  fourierdlem114  40910  etransclem23  40947  zgeltp1eq  41888  setsnidel  41916  iccpartres  41923  pfx2  41981  pfxccatin12d  42001  repswpfx  42005  rabsubmgmd  42353  submgmid  42355  subsubmgm  42359  mgmhmima  42364  mgmhmeql  42365  isassintop  42408  rnghmsscmap2  42535  rnghmsscmap  42536  rnghmsubcsetc  42539  zrzeroorngc  42564  rhmsscmap2  42581  rhmsscmap  42582  rhmsubcsetc  42585  rhmsscrnghm  42588  rhmsubcrngc  42591  srhmsubc  42638  fldhmsubc  42646  rhmsubc  42652  srhmsubcALTV  42656  fldhmsubcALTV  42664  rhmsubcALTV  42670  rmfsupp  42717  mndpfsupp  42719  scmfsupp  42721  mptcfsupp  42723  lcoel0  42779  lincsumcl  42782  lincscmcl  42783  lcoss  42787  lindsrng01  42819  lincreslvec3  42833  lindssnlvec  42837  zgtp1leeq  42873