Theorem mpbir2and 710

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 256	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 397

This theorem is referenced by:  elpreimad  6992  fveqressseq  7013  fmptsng  7096  fmptsnd  7097  fnprb  7140  fntpb  7141  fpr3g  8171  frrlem4  8175  1ellim  8399  fdmfifsupp  9236  fczfsuppd  9244  fsuppmptif  9256  fsuppco2  9260  fsuppcor  9261  dffi3  9288  suppr  9328  infpr  9360  ordtypelem7  9381  cantnf0  9532  cantnfp1lem1  9535  cantnfp1lem2  9536  cantnfp1lem3  9537  cantnflem1a  9542  cantnflem1d  9545  cantnflem1  9546  cantnf  9550  rankpwi  9680  carduni  9838  fin23lem32  10201  fpwwe2lem5  10492  fpwwe2lem11  10498  fpwwe2lem12  10499  fpwwe2  10500  inttsk  10631  grutsk1  10678  add20  11588  supaddc  12043  supadd  12044  supmul  12048  suprzcl  12501  uzid  12698  uzwo3  12784  rpnnen1lem5  12822  xrletrid  12990  xrre  13004  xrre3  13006  xleadd1a  13088  xlemul1a  13123  elioc2  13243  elico2  13244  elicc2  13245  elfz1eq  13368  fzadd2  13392  fznatpl1  13411  elfz1uz  13427  nn0fz0  13455  fzctr  13469  fzo1fzo0n0  13539  fzoaddel  13541  elincfzoext  13546  flid  13629  flval3  13636  fladdz  13646  fldiv  13681  modid  13717  hashf1lem1  14268  hashf1lem1OLD  14269  pfxccatin12d  14556  repswpfx  14596  2cshw  14624  pfx2  14759  wwlktovf1  14771  sqeqd  14976  sqrlem7  15059  max0add  15121  abs2difabs  15145  rddif  15151  fzomaxdiflem  15153  rexico  15164  icodiamlt  15246  limsupgre  15289  rlim3  15306  icco1  15348  rlimclim  15354  rlimuni  15358  rlimresb  15373  isercolllem2  15476  isercolllem3  15477  isercoll  15478  caucvgrlem  15483  caurcvgr  15484  iseraltlem3  15494  fsum00  15609  o1fsum  15624  bitsfzolem  16240  bitsfzo  16241  bitsmod  16242  bitscmp  16244  gcd0id  16325  gcdneg  16328  bezoutlem4  16349  nn0seqcvgd  16372  lcmneg  16405  lcmfunsnlem2lem2  16441  qredeq  16459  prmind2  16487  eulerthlem2  16580  pcpremul  16641  pcidlem  16670  pcgcd1  16675  fldivp1  16695  pcfaclem  16696  4sqlem17  16759  vdwlem1  16779  vdwlem6  16784  vdwlem12  16790  vdwlem13  16791  0ram  16818  ram0  16820  ramub1lem1  16824  invco  17580  sectmon  17591  monsect  17592  invid  17596  ssctr  17634  ssceq  17635  0ssc  17649  0subcat  17650  catsubcat  17651  issubc3  17661  fullsubc  17662  funcinv  17685  fthmon  17740  fuccocl  17779  fucidcl  17780  invfuc  17789  2initoinv  17822  2termoinv  17829  elhomai  17845  setcmon  17899  setcepi  17900  catcisolem  17922  curf2cl  18046  yonedalem4c  18092  yonedalem3  18095  yoniso  18100  lublecl  18176  isacs3lem  18357  tsrdir  18419  mnd1  18523  sgrp2nmndlem4  18663  sgrp2nmndlem5  18664  nmznsg  18892  ghmpreima  18952  ghmeql  18953  ghmnsgpreima  18955  cntzsubm  19038  cntzsubg  19039  cntzmhm  19041  symgextfo  19126  symgfixf1  19141  symgfixfolem1  19142  odlem2  19243  gexlem2  19283  gexcl2  19290  sylow1lem5  19303  subgslw  19317  slwhash  19325  fislw  19326  sylow3lem1  19328  lsmsubg  19355  efgredlemd  19445  efgredlem  19448  efgcpbllemb  19456  frgpuplem  19473  cyggeninv  19578  iscygd  19582  iscygodd  19583  gsumzadd  19618  gsumconst  19630  gsumpt  19658  gsum2dlem2  19667  gsum2d  19668  gsum2d2lem  19669  dprdfcntz  19713  eldprdi  19716  subgdmdprd  19732  subgdprd  19733  dprdpr  19748  ablfac1c  19769  ablfac1eu  19771  ablfaclem3  19785  ring1  19936  kerf1ghm  20085  issubdrg  20154  rhmeql  20159  rhmima  20160  cntzsubr  20162  isabvd  20186  abvdiv  20203  lsslsp  20383  lmhmima  20415  lmhmpreima  20416  lmhmeql  20423  lsmcl  20451  lspfixed  20496  qsssubdrg  20763  gzrngunit  20770  evpmodpmf1o  20907  ocvpj  21030  dsmm0cl  21053  dsmmacl  21054  dsmmsubg  21056  dsmmlss  21057  frlmsplit2  21086  uvcff  21104  lindfrn  21134  f1lindf  21135  lindsss  21137  issubassa  21179  issubassa2  21202  snifpsrbag  21231  psrbaglesupp  21233  psrbaglesuppOLD  21234  psrbaglecl  21235  psrbagleclOLD  21236  psrbagaddcl  21237  psrbagaddclOLD  21238  psrbagcon  21239  psrbagconOLD  21240  mplsubglem  21311  mpllsslem  21312  mplassa  21333  subrgmpl  21339  mplcoe5  21347  mplbas2  21349  mplind  21384  mpfind  21423  ismhp2  21438  mhpmulcl  21445  mhplss  21451  ply1assa  21476  coe1tmmul2  21553  coe1tmmul  21554  cply1coe0bi  21577  dmatid  21750  dmatsubcl  21753  dmatscmcl  21758  scmatid  21769  scmataddcl  21771  scmatsubcl  21772  scmatmulcl  21773  smatvscl  21779  scmatrhmcl  21783  mat0scmat  21793  mat1scmat  21794  mdet0pr  21847  chmaidscmat  22103  distop  22251  indistopon  22257  ppttop  22263  epttop  22265  mretopd  22349  toponmre  22350  neiss  22366  opnneissb  22371  ssnei2  22373  innei  22382  neiptoptop  22388  ordtcld1  22454  ordtcld2  22455  lmconst  22518  cnpnei  22521  iscncl  22526  cnss1  22533  cnss2  22534  cncnpi  22535  cncnp  22537  cnconst2  22540  cnrest  22542  cnpresti  22545  cnpdis  22550  paste  22551  lmcnp  22561  cnhaus  22611  hauscmp  22664  2ndcomap  22715  1stcelcls  22718  1stccnp  22719  llyrest  22742  nllyrest  22743  llyidm  22745  nllyidm  22746  ssref  22769  reftr  22771  refun0  22772  dissnref  22785  kgentopon  22795  kgenidm  22804  kgencn3  22815  txcld  22860  neitx  22864  tx1cn  22866  tx2cn  22867  ptcld  22870  xkoccn  22876  txcnp  22877  ptcnp  22879  txcnmpt  22881  ptcn  22884  txdis1cn  22892  ptrescn  22896  txkgen  22909  xkoco1cn  22914  xkoco2cn  22915  xkococn  22917  xkoinjcn  22944  qtoptop2  22956  qtopuni  22959  qtopid  22962  qtopkgen  22967  basqtop  22968  tgqtop  22969  qtopss  22972  qtopeu  22973  qtoprest  22974  kqopn  22991  kqcld  22992  kqreglem2  22999  reghmph  23050  ordthmeolem  23058  qtopf1  23073  opnfbas  23099  isfil2  23113  fbasweak  23122  fsubbas  23124  filconn  23140  fbasrn  23141  rnelfmlem  23209  flimss2  23229  flimss1  23230  hausflim  23238  flimclslem  23241  flimsncls  23243  cnpflfi  23256  flfcnp2  23264  fclsfnflim  23284  cnextfvval  23322  cnextfres1  23325  symgtgp  23363  opnsubg  23365  ghmcnp  23372  qustgpopn  23377  qustgplem  23378  qustgphaus  23380  tsmsfbas  23385  ustfilxp  23470  utoptop  23492  utopbas  23493  restutopopn  23496  iducn  23541  cstucnd  23542  ucncn  23543  fmucnd  23550  cfilufg  23551  trcfilu  23552  cfiluweak  23553  neipcfilu  23554  psmetres2  23573  isxmetd  23585  xmetpsmet  23607  imasf1oxmet  23634  xblss2ps  23660  xblss2  23661  xblcntrps  23669  xblcntr  23670  blcld  23767  metustfbas  23819  cfilucfil  23821  restmetu  23832  ngptgp  23898  tngngpd  23923  nrmtngnrm  23928  tngnrg  23944  nlmvscn  23957  nrginvrcn  23962  nmo0  24005  nmoeq0  24006  nmoid  24012  nghmcn  24015  0nmhm  24025  blcvx  24067  iccntr  24090  xrge0tsms  24103  xmetdcn2  24106  metdstri  24120  metdscn  24125  rescncf  24166  cncfco  24176  oprpiece1res2  24221  cnheibor  24224  cnllycmp  24225  bndth  24227  ishtpyd  24244  isphtpyd  24255  pcoval2  24285  nmhmcn  24389  ipcn  24516  lmnn  24533  cfilss  24540  iscfil3  24543  cfilfcls  24544  cmetcaulem  24558  iscmet3lem2  24562  cfilres  24566  lmcau  24583  flimcfil  24584  cncmet  24592  rlmbn  24631  minveclem3b  24698  pjthlem1  24707  pjth2  24710  ivthlem3  24723  ovolssnul  24757  ovolctb  24760  ovoliunnul  24777  ovolsca  24785  ovolicopnf  24794  voliunlem2  24821  volsup  24826  dyadmaxlem  24867  vitalilem5  24882  mbfres  24914  mbfss  24916  mbfmulc2re  24918  mbfadd  24931  mbfmulc2  24933  mbflim  24938  i1faddlem  24963  i1fmullem  24964  mbfmul  24997  itg2mulc  25018  itg2cnlem1  25032  ibl0  25057  iblposlem  25062  itgreval  25067  iblneg  25073  iblss  25075  iblss2  25076  itgle  25080  iblconst  25088  iblabs  25099  iblabsr  25100  iblmulc2  25101  bddmulibl  25109  limciun  25164  limcun  25165  dvres2lem  25180  dvidlem  25185  dvcnp2  25190  dvcn  25191  cpnres  25207  dvaddbr  25208  dvmulbr  25209  dvcobr  25216  dvcjbr  25219  dvrec  25225  dvcnvlem  25246  dvferm  25258  dvlip2  25265  dveq0  25270  dv11cn  25271  dvivthlem1  25278  lhop1  25284  lhop2  25285  lhop  25286  dvcnvre  25289  dvfsumlem3  25298  dvfsumlem4  25299  dvfsumrlim  25301  dvfsum2  25304  ftc1a  25307  ftc1lem4  25309  ftc1lem6  25311  ftc1  25312  coe1mul3  25370  deg1addle2  25373  deg1sublt  25381  fta1blem  25439  drnguc1p  25441  ig1prsp  25448  plyco0  25459  plyeq0lem  25477  dgrub  25501  dgreq  25511  dgradd2  25535  dgrmul  25537  dgrcolem2  25541  dgrco  25542  plycpn  25555  plydivlem4  25562  plydiveu  25564  vieta1lem2  25577  vieta1  25578  aalioulem2  25599  aalioulem3  25600  aaliou3lem7  25615  tayl0  25627  ulmcn  25664  ulmdvlem3  25667  psercn  25691  abelth  25706  pilem3  25718  efif1olem1  25804  abslogimle  25835  argregt0  25871  argrege0  25872  logf1o2  25911  cxpsqrtlem  25963  cxpcn3  26007  abscxpbnd  26012  logreclem  26018  ang180lem2  26066  ang180lem3  26067  xrlimcnp  26224  harmonicbnd4  26266  fsumharmonic  26267  lgamgulmlem5  26288  lgambdd  26292  basellem4  26339  dvdsppwf1o  26441  dvdsflf1o  26442  fsumfldivdiaglem  26444  chpeq0  26462  chteq0  26463  chtub  26466  chpub  26474  dchrelbasd  26493  dchrmulcl  26503  dchrinv  26515  bposlem1  26538  bposlem2  26539  lgsdirprm  26585  lgsqrlem2  26601  lgsqrlem3  26602  lgsdchr  26609  lgseisenlem1  26629  lgseisenlem2  26630  lgseisenlem3  26631  lgsquadlem1  26634  2sqlem8  26680  2sqblem  26685  2sqmod  26690  chebbnd1lem1  26723  dchrisumlem1  26743  dchrisumlem2  26744  dchrisumlem3  26745  dchrisum0fno1  26765  pntrmax  26818  pntpbnd1a  26839  pntibndlem3  26846  pntlemn  26854  pntlemi  26858  pntlem3  26863  pntleml  26865  ostth1  26887  ostth2  26891  ostth3  26892  nosepon  26919  nolesgn2ores  26926  nogesgn1ores  26928  nosupres  26961  nosupbnd1lem2  26963  nosupbnd2lem1  26969  noinfres  26976  noinfbnd1lem2  26978  noinfbnd2lem1  26984  ercgrg  27167  motco  27190  cnvmot  27191  legso  27249  mirmot  27325  colopp  27419  hphl  27421  lmicom  27438  lmimid  27444  lmimot  27448  hypcgrlem1  27449  hypcgrlem2  27450  trgcopyeulem  27455  inagswap  27491  inaghl  27495  cgrg3col4  27503  brbtwn2  27562  axlowdimlem3  27601  axlowdimlem16  27614  axcontlem8  27628  fusgrfis  27986  nbgr2vtx1edg  28006  0vtxrgr  28232  0vtxrusgr  28233  ewlkle  28261  wlk1ewlk  28296  uspgr2wlkeq2  28303  wlkp1lem8  28336  trlontrl  28367  pthonpth  28404  pthdlem2  28424  wlklnwwlkln1  28521  wlknewwlksn  28540  wwlksnred  28545  wwlksnredwwlkn0  28549  2trlond  28592  2pthond  28595  elwwlks2ons3im  28607  clwlkclwwlklem2a1  28644  clwlkclwwlkf1  28662  clwwlkel  28698  clwwlkwwlksb  28706  wwlksext2clwwlk  28709  1ewlk  28767  0trlon  28776  0pthon  28779  1pthond  28796  3trlond  28825  3pthond  28827  3spthond  28829  eupthres  28867  2clwwlk2clwwlk  29002  numclwwlk1lem2foa  29006  numclwwlk1lem2f1  29009  nvabs  29322  vacn  29344  nmcvcn  29345  nmblore  29436  0lno  29440  0blo  29442  nmlno0lem  29443  occl  29954  pjhthlem1  30041  pjpjpre  30069  nmopre  30520  nmlnop0iALT  30645  nmophmi  30681  leoprf2  30777  stlesi  30891  disjdifprg  31201  disjun0  31221  fsuppcurry1  31347  fsuppcurry2  31348  fpwrelmap  31355  fzspl  31398  dfmgc2lem  31560  pwrssmgc  31565  xrge0tsmsd  31604  ogrpaddlt  31630  ogrpsublt  31634  psgnfzto1stlem  31654  fzto1st1  31656  evpmid  31702  pnfinf  31724  rmfsupp2  31779  ornglmullt  31806  orngrmullt  31807  orngmullt  31808  ofldlt1  31812  isarchiofld  31816  nsgmgc  31894  lbsdiflsp0  32005  fedgmul  32010  fldexttr  32031  fldextid  32032  qtopt1  32083  reff  32087  locfinreflem  32088  metideq  32141  metider  32142  pstmxmet  32145  qqhval2lem  32229  qqhcn  32239  qqhucn  32240  pwsiga  32396  prsiga  32397  measle0  32474  mbfmcst  32526  1stmbfm  32527  2ndmbfm  32528  imambfm  32529  cnmbfm  32530  mbfmco  32531  mbfmco2  32532  0elcarsg  32574  carsgclctun  32588  sibfof  32607  oddpwdc  32621  eulerpartlemmf  32642  eulerpartlemgs2  32647  0rrv  32718  ballotlemfc0  32759  ballotlemfcc  32760  signstfveq0  32856  breprexplemc  32912  bnj1452  33331  usgrgt2cycl  33391  acycgr1v  33410  derangen  33433  subfacval3  33450  cvmseu  33537  cvmliftmolem2  33543  cvmliftlem7  33552  cvmliftlem15  33559  cvmlift2lem9a  33564  cvmlift2lem9  33572  cvmlift2lem10  33573  cvmlift2lem11  33574  cvmlift2lem12  33575  cvmlift3lem6  33585  cvmlift3lem8  33587  ex-sategoelel  33682  ex-sategoelelomsuc  33687  mclsppslem  33844  mclspps  33845  wsuclem  34098  cofcutrtime  34189  fness  34634  fnetr  34636  fnessref  34642  refssfne  34643  neibastop1  34644  neibastop2  34646  tailfb  34662  filnetlem3  34665  bj-finsumval0  35569  bj-rvecvec  35583  dfgcd3  35608  lindsadd  35883  poimirlem13  35903  poimirlem15  35905  poimirlem24  35914  poimirlem28  35918  mblfinlem2  35928  ovoliunnfl  35932  volsupnfl  35935  mbfresfi  35936  iblabsnc  35954  iblmulc2nc  35955  ftc1cnnclem  35961  ftc1cnnc  35962  ftc1anc  35971  sdclem2  36013  metf1o  36026  ismtyhmeolem  36075  ismtyres  36079  heibor1lem  36080  bfplem2  36094  bfp  36095  rrncmslem  36103  iccbnd  36111  icccmpALT  36112  rngogrphom  36242  rngoisoco  36253  keridl  36303  lsmcv2  37304  lsatcv0  37306  lcvexchlem4  37312  lcvexchlem5  37313  l1cvpat  37329  lfl0f  37344  lfladdcl  37346  lflnegcl  37350  lkrlss  37370  eqlkr  37374  lkrlsp  37377  lkrlsp2  37378  lshpkrcl  37391  lkrin  37439  1cvrjat  37751  llni  37784  llnle  37794  lplni  37808  lplnle  37816  llncvrlpln2  37833  2atmat  37837  lvoli  37851  lplncvrlvol2  37891  elpaddri  38078  paddclN  38118  pclclN  38167  pclfinN  38176  0psubclN  38219  1psubclN  38220  atpsubclN  38221  pmapsubclN  38222  osumclN  38243  pexmidN  38245  pexmidlem6N  38251  lhp2lt  38277  lautcnv  38366  idlaut  38372  lautco  38373  idldil  38390  ldilcnv  38391  ldilco  38392  ltrncnv  38422  idltrn  38426  cdleme16d  38557  cdleme50laut  38823  cdleme50ldil  38824  cdleme50ltrn  38833  ltrnco  38995  dian0  39315  dia0eldmN  39316  dia1eldmN  39317  dialss  39322  diaintclN  39334  docaclN  39400  doca2N  39402  djajN  39413  dibintclN  39443  diblss  39446  dicvaddcl  39466  dicvscacl  39467  dicn0  39468  cdlemn11a  39483  dihord2cN  39497  dihord11b  39498  dihord6apre  39532  dihmeetlem1N  39566  dihglblem5apreN  39567  dihpN  39612  dihjatcclem4  39697  dochkr1  39754  islpoldN  39760  lcfrlem31  39849  mapdpglem18  39965  mapdheq2  40005  mapdheq4  40008  mapdh6aN  40011  hdmap1l6a  40085  hdmap14lem4a  40147  lcmineqlem4  40302  isfsuppd  40477  frlmfzoccat  40498  drnginvmuld  40522  fsuppind  40547  fsuppssind  40550  prjspvs  40717  irrapxlem4  40917  pell1234qrdich  40953  pell1qr1  40963  pell14qrgap  40967  pellqrexplicit  40969  rmspecfund  41001  fzmaxdif  41074  acongeq  41076  jm2.23  41089  jm3.1  41113  lmhmlnmsplit  41183  hbt  41226  dgrsub2  41231  proot1ex  41297  naddcnff  41337  naddcnffo  41339  naddcnfid1  41342  naddcnfid2  41343  clublem  41548  dftrcl3  41658  mnugrud  42232  hashnzfz2  42269  dvconstbi  42282  ubelsupr  42893  restopn3  43035  wessf1ornlem  43058  lefldiveq  43175  iccintsng  43406  climsuse  43494  mullimc  43502  limcdm0  43504  limccog  43506  mullimcf  43509  constlimc  43510  idlimc  43512  limcperiod  43514  limsupre  43527  limcleqr  43530  neglimc  43533  addlimc  43534  0ellimcdiv  43535  xlimliminflimsup  43748  cncfshift  43760  cncfperiod  43765  cncfuni  43772  icccncfext  43773  cncfiooicclem1  43779  fperdvper  43805  ioodvbdlimc1lem2  43818  ioodvbdlimc2lem  43820  mbfres2cn  43844  iblsplit  43852  stoweidlem7  43893  stoweidlem13  43899  stoweidlem26  43912  wallispilem3  43953  stirlinglem6  43965  stirlinglem10  43969  dirkercncf  43993  fourierdlem6  43999  fourierdlem11  44004  fourierdlem12  44005  fourierdlem15  44008  fourierdlem26  44019  fourierdlem42  44035  fourierdlem50  44042  fourierdlem51  44043  fourierdlem52  44044  fourierdlem54  44046  fourierdlem62  44054  fourierdlem79  44071  fourierdlem102  44094  fourierdlem114  44106  etransclem23  44143  zgeltp1eq  45161  setsnidel  45189  preimafvsnel  45191  iccpartres  45230  prpair  45313  fpprel2  45553  rabsubmgmd  45705  submgmid  45707  subsubmgm  45711  mgmhmima  45716  mgmhmeql  45717  isassintop  45764  rnghmsscmap2  45891  rnghmsscmap  45892  rnghmsubcsetc  45895  zrzeroorngc  45920  rhmsscmap2  45937  rhmsscmap  45938  rhmsubcsetc  45941  rhmsscrnghm  45944  rhmsubcrngc  45947  srhmsubc  45994  fldhmsubc  46002  rhmsubc  46008  srhmsubcALTV  46012  fldhmsubcALTV  46020  rhmsubcALTV  46026  rmfsupp  46070  mndpfsupp  46072  scmfsupp  46074  mptcfsupp  46076  lcoel0  46129  lincsumcl  46132  lincscmcl  46133  lcoss  46137  lindsrng01  46169  lincreslvec3  46183  lindssnlvec  46187  zgtp1leeq  46222  lubsscl  46614  glbsscl  46615  idmon  46657  idepi  46658  thinciso  46701