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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  elpreimad  6829  fveqressseq  6847  fmptsng  6930  fmptsnd  6931  fnprb  6971  fntpb  6972  fdmfifsupp  8843  fczfsuppd  8851  fsuppmptif  8863  fsuppco2  8866  fsuppcor  8867  dffi3  8895  suppr  8935  infpr  8967  ordtypelem7  8988  cantnf0  9138  cantnfp1lem1  9141  cantnfp1lem2  9142  cantnfp1lem3  9143  cantnflem1a  9148  cantnflem1d  9151  cantnflem1  9152  cantnf  9156  rankpwi  9252  carduni  9410  fin23lem32  9766  fpwwe2lem6  10057  fpwwe2lem9  10060  fpwwe2lem12  10063  fpwwe2lem13  10064  fpwwe2  10065  inttsk  10196  grutsk1  10243  add20  11152  supaddc  11608  supadd  11609  supmul  11613  suprzcl  12063  uzwo3  12344  rpnnen1lem5  12381  xrletrid  12549  xrre  12563  xrre3  12565  xleadd1a  12647  xlemul1a  12682  elioc2  12800  elico2  12801  elicc2  12802  elfz1eq  12919  fzadd2  12943  fznatpl1  12962  elfz1uz  12978  nn0fz0  13006  fzctr  13020  fzo1fzo0n0  13089  fzoaddel  13091  elincfzoext  13096  flid  13179  flval3  13186  fladdz  13196  fldiv  13229  modid  13265  seqf1olem1  13410  bcval5  13679  hashf1lem1  13814  pfxccatin12d  14107  repswpfx  14147  2cshw  14175  pfx2  14309  wwlktovf1  14321  sqeqd  14525  sqrlem7  14608  max0add  14670  abs2difabs  14694  rddif  14700  fzomaxdiflem  14702  rexico  14713  icodiamlt  14795  limsupgre  14838  rlim3  14855  icco1  14897  rlimclim  14903  rlimuni  14907  rlimresb  14922  isercolllem2  15022  isercolllem3  15023  isercoll  15024  caucvgrlem  15029  caurcvgr  15030  iseraltlem3  15040  fsum00  15153  o1fsum  15168  bitsfzolem  15783  bitsfzo  15784  bitsmod  15785  bitscmp  15787  gcd0id  15867  gcdneg  15870  bezoutlem4  15890  nn0seqcvgd  15914  lcmneg  15947  lcmfunsnlem2lem2  15983  qredeq  16001  prmind2  16029  hashdvds  16112  eulerthlem2  16119  pcpremul  16180  pcidlem  16208  pcgcd1  16213  fldivp1  16233  pcfaclem  16234  prmreclem5  16256  4sqlem17  16297  vdwlem1  16317  vdwlem6  16322  vdwlem12  16328  vdwlem13  16329  0ram  16356  ram0  16358  ramub1lem1  16362  invco  17041  sectmon  17052  monsect  17053  invid  17057  ssctr  17095  ssceq  17096  0ssc  17107  0subcat  17108  catsubcat  17109  issubc3  17119  fullsubc  17120  funcinv  17143  fthmon  17197  fuccocl  17234  fucidcl  17235  invfuc  17244  2initoinv  17270  2termoinv  17277  elhomai  17293  setcmon  17347  setcepi  17348  catcisolem  17366  curf2cl  17481  yonedalem4c  17527  yonedalem3  17530  yoniso  17535  lublecl  17599  isacs3lem  17776  tsrdir  17848  mnd1  17952  sgrp2nmndlem4  18093  sgrp2nmndlem5  18094  nmznsg  18320  ghmpreima  18380  ghmeql  18381  ghmnsgpreima  18383  cntzsubm  18466  cntzsubg  18467  cntzmhm  18469  symgextfo  18550  symgfixf1  18565  symgfixfolem1  18566  odlem2  18667  gexlem2  18707  gexcl2  18714  sylow1lem5  18727  subgslw  18741  slwhash  18749  fislw  18750  sylow3lem1  18752  lsmsubg  18779  efgredlemd  18870  efgredlem  18873  efgcpbllemb  18881  frgpuplem  18898  cyggeninv  19002  iscygd  19006  iscygodd  19007  gsumzadd  19042  gsumconst  19054  gsumpt  19082  gsum2dlem2  19091  gsum2d  19092  gsum2d2lem  19093  dprdfcntz  19137  eldprdi  19140  subgdmdprd  19156  subgdprd  19157  dprdpr  19172  ablfac1c  19193  ablfac1eu  19195  ablfaclem3  19209  ring1  19352  kerf1ghm  19497  kerf1hrmOLD  19498  issubdrg  19560  rhmeql  19565  rhmima  19566  cntzsubr  19568  isabvd  19591  abvdiv  19608  lsslsp  19787  lmhmima  19819  lmhmpreima  19820  lmhmeql  19827  lsmcl  19855  lspfixed  19900  issubassa  20098  issubassa2  20121  snifpsrbag  20146  psrbaglesupp  20148  psrbaglecl  20149  psrbagaddcl  20150  psrbagcon  20151  mplsubglem  20214  mpllsslem  20215  mplassa  20235  subrgmpl  20241  mplcoe5  20249  mplbas2  20251  mplind  20282  mpfind  20320  mhp0cl  20337  mhpaddcl  20338  mhpinvcl  20339  mhpvscacl  20341  mhplss  20342  ply1assa  20367  coe1tmmul2  20444  coe1tmmul  20445  cply1coe0bi  20468  qsssubdrg  20604  gzrngunit  20611  evpmodpmf1o  20740  ocvpj  20861  dsmm0cl  20884  dsmmacl  20885  dsmmsubg  20887  dsmmlss  20888  frlmsplit2  20917  uvcff  20935  lindfrn  20965  f1lindf  20966  lindsss  20968  mat1rngiso  21095  dmatid  21104  dmatsubcl  21107  dmatscmcl  21112  scmatid  21123  scmataddcl  21125  scmatsubcl  21126  scmatmulcl  21127  smatvscl  21133  scmatrhmcl  21137  scmatrngiso  21145  mat0scmat  21147  mat1scmat  21148  mdet0pr  21201  m2cpmrngiso  21366  pm2mprngiso  21430  chmaidscmat  21456  distop  21603  indistopon  21609  ppttop  21615  epttop  21617  mretopd  21700  toponmre  21701  neiss  21717  opnneissb  21722  ssnei2  21724  innei  21733  neiptoptop  21739  ordtcld1  21805  ordtcld2  21806  lmconst  21869  cnpnei  21872  iscncl  21877  cnss1  21884  cnss2  21885  cncnpi  21886  cncnp  21888  cnconst2  21891  cnrest  21893  cnpresti  21896  cnpdis  21901  paste  21902  lmcnp  21912  cnhaus  21962  hauscmp  22015  2ndcomap  22066  1stcelcls  22069  1stccnp  22070  llyrest  22093  nllyrest  22094  llyidm  22096  nllyidm  22097  ssref  22120  reftr  22122  refun0  22123  dissnref  22136  kgentopon  22146  kgenidm  22155  kgencn3  22166  txcld  22211  neitx  22215  tx1cn  22217  tx2cn  22218  ptcld  22221  xkoccn  22227  txcnp  22228  ptcnp  22230  txcnmpt  22232  ptcn  22235  txdis1cn  22243  ptrescn  22247  txkgen  22260  xkoco1cn  22265  xkoco2cn  22266  xkococn  22268  xkoinjcn  22295  qtoptop2  22307  qtopuni  22310  qtopid  22313  qtopkgen  22318  basqtop  22319  tgqtop  22320  qtopss  22323  qtopeu  22324  qtoprest  22325  kqopn  22342  kqcld  22343  kqreglem2  22350  reghmph  22401  ordthmeolem  22409  qtopf1  22424  opnfbas  22450  isfil2  22464  fbasweak  22473  fsubbas  22475  filconn  22491  fbasrn  22492  rnelfmlem  22560  flimss2  22580  flimss1  22581  hausflim  22589  flimclslem  22592  flimsncls  22594  cnpflfi  22607  flfcnp2  22615  fclsfnflim  22635  cnextfvval  22673  cnextfres1  22676  symgtgp  22714  opnsubg  22716  ghmcnp  22723  qustgpopn  22728  qustgplem  22729  qustgphaus  22731  tsmsfbas  22736  ustfilxp  22821  utoptop  22843  utopbas  22844  restutopopn  22847  iducn  22892  cstucnd  22893  ucncn  22894  fmucnd  22901  cfilufg  22902  trcfilu  22903  cfiluweak  22904  neipcfilu  22905  psmetres2  22924  isxmetd  22936  xmetpsmet  22958  imasf1oxmet  22985  xblss2ps  23011  xblss2  23012  xblcntrps  23020  xblcntr  23021  blcld  23115  metustfbas  23167  cfilucfil  23169  restmetu  23180  ngptgp  23245  tngngpd  23262  nrmtngnrm  23267  tngnrg  23283  nlmvscn  23296  nrginvrcn  23301  nmo0  23344  nmoeq0  23345  nmoid  23351  nghmcn  23354  0nmhm  23364  blcvx  23406  iccntr  23429  xrge0tsms  23442  xmetdcn2  23445  metdstri  23459  metdscn  23464  rescncf  23505  cncfco  23515  oprpiece1res2  23556  cnheibor  23559  cnllycmp  23560  bndth  23562  ishtpyd  23579  isphtpyd  23590  pcoval2  23620  nmhmcn  23724  ipcn  23849  lmnn  23866  cfilss  23873  iscfil3  23876  cfilfcls  23877  cmetcaulem  23891  iscmet3lem2  23895  cfilres  23899  lmcau  23916  flimcfil  23917  cncmet  23925  rlmbn  23964  minveclem3b  24031  pjthlem1  24040  pjth2  24043  ivthlem3  24054  ovolssnul  24088  ovolctb  24091  ovoliunnul  24108  ovolsca  24116  ovolicopnf  24125  voliunlem2  24152  volsup  24157  dyadmaxlem  24198  vitalilem5  24213  mbfres  24245  mbfss  24247  mbfmulc2re  24249  mbfadd  24262  mbfmulc2  24264  mbflim  24269  i1faddlem  24294  i1fmullem  24295  mbfmul  24327  itg2mulc  24348  itg2cnlem1  24362  ibl0  24387  iblposlem  24392  itgreval  24397  iblneg  24403  iblss  24405  iblss2  24406  itgle  24410  iblconst  24418  iblabs  24429  iblabsr  24430  iblmulc2  24431  bddmulibl  24439  limciun  24492  limcun  24493  dvres2lem  24508  dvidlem  24513  dvcnp2  24517  dvcn  24518  cpnres  24534  dvaddbr  24535  dvmulbr  24536  dvcobr  24543  dvcjbr  24546  dvrec  24552  dvcnvlem  24573  dvferm  24585  dvlip2  24592  dveq0  24597  dv11cn  24598  dvivthlem1  24605  lhop1  24611  lhop2  24612  lhop  24613  dvcnvre  24616  dvfsumlem3  24625  dvfsumlem4  24626  dvfsumrlim  24628  dvfsum2  24631  ftc1a  24634  ftc1lem4  24636  ftc1lem6  24638  ftc1  24639  coe1mul3  24693  deg1addle2  24696  deg1sublt  24704  fta1blem  24762  drnguc1p  24764  ig1prsp  24771  plyco0  24782  plyeq0lem  24800  dgrub  24824  dgreq  24834  dgradd2  24858  dgrmul  24860  dgrcolem2  24864  dgrco  24865  plycpn  24878  plydivlem4  24885  plydiveu  24887  vieta1lem2  24900  vieta1  24901  aalioulem2  24922  aalioulem3  24923  aaliou3lem7  24938  tayl0  24950  ulmcn  24987  ulmdvlem3  24990  psercn  25014  abelth  25029  pilem3  25041  efif1olem1  25126  abslogimle  25157  argregt0  25193  argrege0  25194  logf1o2  25233  cxpsqrtlem  25285  cxpcn3  25329  abscxpbnd  25334  logreclem  25340  ang180lem2  25388  ang180lem3  25389  xrlimcnp  25546  harmonicbnd4  25588  fsumharmonic  25589  lgamgulmlem5  25610  lgambdd  25614  basellem3  25660  basellem4  25661  dvdsppwf1o  25763  dvdsflf1o  25764  fsumfldivdiaglem  25766  chpeq0  25784  chteq0  25785  chtub  25788  chpub  25796  dchrelbasd  25815  dchrmulcl  25825  dchrinv  25837  bcmono  25853  bposlem1  25860  bposlem2  25861  lgsdirprm  25907  lgsqrlem2  25923  lgsqrlem3  25924  lgsdchr  25931  lgseisenlem1  25951  lgseisenlem2  25952  lgseisenlem3  25953  lgsquadlem1  25956  2sqlem8  26002  2sqblem  26007  2sqmod  26012  chebbnd1lem1  26045  dchrisumlem1  26065  dchrisumlem2  26066  dchrisumlem3  26067  dchrisum0fno1  26087  pntrmax  26140  pntpbnd1a  26161  pntibndlem3  26168  pntlemn  26176  pntlemi  26180  pntlem3  26185  pntleml  26187  ostth1  26209  ostth2  26213  ostth3  26214  ercgrg  26303  motco  26326  cnvmot  26327  legso  26385  mirmot  26461  colopp  26555  hphl  26557  lmicom  26574  lmimid  26580  lmimot  26584  hypcgrlem1  26585  hypcgrlem2  26586  trgcopyeulem  26591  inagswap  26627  inaghl  26631  cgrg3col4  26639  brbtwn2  26691  axlowdimlem3  26730  axlowdimlem16  26743  axcontlem8  26757  fusgrfis  27112  nbgr2vtx1edg  27132  0vtxrgr  27358  0vtxrusgr  27359  ewlkle  27387  wlk1ewlk  27421  uspgr2wlkeq2  27428  wlkp1lem8  27462  trlontrl  27492  pthonpth  27529  pthdlem2  27549  wlklnwwlkln1  27646  wlknewwlksn  27665  wwlksnred  27670  wwlksnredwwlkn0  27674  2trlond  27718  2pthond  27721  elwwlks2ons3im  27733  clwlkclwwlklem2a1  27770  clwlkclwwlkf1  27788  clwwlkel  27825  clwwlkwwlksb  27833  wwlksext2clwwlk  27836  1ewlk  27894  0trlon  27903  0pthon  27906  1pthond  27923  3trlond  27952  3pthond  27954  3spthond  27956  eupthres  27994  2clwwlk2clwwlk  28129  numclwwlk1lem2foa  28133  numclwwlk1lem2f1  28136  nvabs  28449  vacn  28471  nmcvcn  28472  nmblore  28563  0lno  28567  0blo  28569  nmlno0lem  28570  occl  29081  pjhthlem1  29168  pjpjpre  29196  nmopre  29647  nmlnop0iALT  29772  nmophmi  29808  leoprf2  29904  stlesi  30018  disjdifprg  30325  disjun0  30345  fsuppcurry1  30461  fsuppcurry2  30462  fpwrelmap  30469  fzspl  30513  xrge0tsmsd  30692  ogrpaddlt  30718  ogrpsublt  30722  psgnfzto1stlem  30742  fzto1st1  30744  evpmid  30790  pnfinf  30812  rmfsupp2  30866  ornglmullt  30880  orngrmullt  30881  orngmullt  30882  ofldlt1  30886  isarchiofld  30890  lbsdiflsp0  31022  fedgmul  31027  fldexttr  31048  fldextid  31049  qtopt1  31099  reff  31103  locfinreflem  31104  metideq  31133  metider  31134  pstmxmet  31137  qqhval2lem  31222  qqhcn  31232  qqhucn  31233  pwsiga  31389  prsiga  31390  measle0  31467  mbfmcst  31517  1stmbfm  31518  2ndmbfm  31519  imambfm  31520  cnmbfm  31521  mbfmco  31522  mbfmco2  31523  0elcarsg  31565  carsgclctun  31579  sibfof  31598  oddpwdc  31612  eulerpartlemmf  31633  eulerpartlemgs2  31638  0rrv  31709  ballotlemfc0  31750  ballotlemfcc  31751  signstfveq0  31847  breprexplemc  31903  bnj1452  32324  usgrgt2cycl  32377  acycgr1v  32396  derangen  32419  subfacval3  32436  cvmseu  32523  cvmliftmolem2  32529  cvmliftlem7  32538  cvmliftlem15  32545  cvmlift2lem9a  32550  cvmlift2lem9  32558  cvmlift2lem10  32559  cvmlift2lem11  32560  cvmlift2lem12  32561  cvmlift3lem6  32571  cvmlift3lem8  32573  ex-sategoelel  32668  ex-sategoelelomsuc  32673  mclsppslem  32830  mclspps  32831  wsuclem  33112  fpr3g  33122  frrlem4  33126  nosepon  33172  nolesgn2ores  33179  nosupres  33207  nosupbnd1lem2  33209  nosupbnd2lem1  33215  fness  33697  fnetr  33699  fnessref  33705  refssfne  33706  neibastop1  33707  neibastop2  33709  tailfb  33725  filnetlem3  33728  bj-finsumval0  34570  bj-rvecvec  34583  dfgcd3  34608  lindsadd  34900  poimirlem13  34920  poimirlem15  34922  poimirlem17  34924  poimirlem24  34931  poimirlem28  34935  mblfinlem2  34945  ovoliunnfl  34949  volsupnfl  34952  mbfresfi  34953  itg2addnclem2  34959  iblabsnc  34971  iblmulc2nc  34972  ftc1cnnclem  34980  ftc1cnnc  34981  ftc1anc  34990  sdclem2  35032  metf1o  35045  ismtyhmeolem  35097  ismtyres  35101  heibor1lem  35102  bfplem2  35116  bfp  35117  rrncmslem  35125  iccbnd  35133  icccmpALT  35134  rngogrphom  35264  rngoisoco  35275  keridl  35325  lsmcv2  36180  lsatcv0  36182  lcvexchlem4  36188  lcvexchlem5  36189  l1cvpat  36205  lfl0f  36220  lfladdcl  36222  lflnegcl  36226  lkrlss  36246  eqlkr  36250  lkrlsp  36253  lkrlsp2  36254  lshpkrcl  36267  lkrin  36315  1cvrjat  36626  llni  36659  llnle  36669  lplni  36683  lplnle  36691  llncvrlpln2  36708  2atmat  36712  lvoli  36726  lplncvrlvol2  36766  elpaddri  36953  paddclN  36993  pclclN  37042  pclfinN  37051  0psubclN  37094  1psubclN  37095  atpsubclN  37096  pmapsubclN  37097  osumclN  37118  pexmidN  37120  pexmidlem6N  37126  lhp2lt  37152  lautcnv  37241  idlaut  37247  lautco  37248  idldil  37265  ldilcnv  37266  ldilco  37267  ltrncnv  37297  idltrn  37301  cdleme16d  37432  cdleme50laut  37698  cdleme50ldil  37699  cdleme50ltrn  37708  ltrnco  37870  dian0  38190  dia0eldmN  38191  dia1eldmN  38192  dialss  38197  diaintclN  38209  docaclN  38275  doca2N  38277  djajN  38288  dibintclN  38318  diblss  38321  dicvaddcl  38341  dicvscacl  38342  dicn0  38343  cdlemn11a  38358  dihord2cN  38372  dihord11b  38373  dihord6apre  38407  dihmeetlem1N  38441  dihglblem5apreN  38442  dihpN  38487  dihjatcclem4  38572  dochkr1  38629  islpoldN  38635  lcfrlem31  38724  mapdpglem18  38840  mapdheq2  38880  mapdheq4  38883  mapdh6aN  38886  hdmap1l6a  38960  hdmap14lem4a  39022  frlmfzoccat  39164  prjspvs  39280  fzsplit1nn0  39371  irrapxlem3  39441  irrapxlem4  39442  pell1234qrdich  39478  pell1qr1  39488  pell14qrgap  39492  pellqrexplicit  39494  rmspecfund  39526  fzmaxdif  39598  acongeq  39600  jm2.23  39613  jm3.1  39637  lmhmlnmsplit  39707  hbt  39750  dgrsub2  39755  proot1ex  39821  clublem  39990  dftrcl3  40085  mnugrud  40640  hashnzfz2  40673  dvconstbi  40686  ubelsupr  41297  wessf1ornlem  41465  lefldiveq  41579  iccintsng  41819  fmul01  41881  fmuldfeq  41884  climsuse  41909  mullimc  41917  limcdm0  41919  limccog  41921  mullimcf  41924  constlimc  41925  idlimc  41927  limcperiod  41929  limsupre  41942  limcleqr  41945  neglimc  41948  addlimc  41949  0ellimcdiv  41950  xlimliminflimsup  42163  cncfshift  42177  cncfperiod  42182  cncfuni  42189  icccncfext  42190  cncfiooicclem1  42196  fperdvper  42223  ioodvbdlimc1lem2  42237  ioodvbdlimc2lem  42239  mbfres2cn  42263  iblsplit  42271  stoweidlem7  42312  stoweidlem13  42318  stoweidlem26  42331  wallispilem3  42372  stirlinglem6  42384  stirlinglem10  42388  dirkercncf  42412  fourierdlem6  42418  fourierdlem11  42423  fourierdlem12  42424  fourierdlem15  42427  fourierdlem26  42438  fourierdlem42  42454  fourierdlem50  42461  fourierdlem51  42462  fourierdlem52  42463  fourierdlem54  42465  fourierdlem62  42473  fourierdlem79  42490  fourierdlem102  42513  fourierdlem114  42525  etransclem23  42562  zgeltp1eq  43529  setsnidel  43557  preimafvsnel  43559  iccpartres  43598  prpair  43683  fpprel2  43926  rabsubmgmd  44078  submgmid  44080  subsubmgm  44084  mgmhmima  44089  mgmhmeql  44090  isassintop  44137  rnghmsscmap2  44264  rnghmsscmap  44265  rnghmsubcsetc  44268  zrzeroorngc  44293  rhmsscmap2  44310  rhmsscmap  44311  rhmsubcsetc  44314  rhmsscrnghm  44317  rhmsubcrngc  44320  srhmsubc  44367  fldhmsubc  44375  rhmsubc  44381  srhmsubcALTV  44385  fldhmsubcALTV  44393  rhmsubcALTV  44399  rmfsupp  44442  mndpfsupp  44444  scmfsupp  44446  mptcfsupp  44448  lcoel0  44503  lincsumcl  44506  lincscmcl  44507  lcoss  44511  lindsrng01  44543  lincreslvec3  44557  lindssnlvec  44561  zgtp1leeq  44596