Theorem biimpar 477

Description: Importation inference from a logical equivalence. (Contributed by NM, 3-May-1994.)

Hypothesis

Ref	Expression
biimpa.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
biimpar	⊢ ((𝜑 ∧ 𝜒) → 𝜓)

Proof of Theorem biimpar

Step	Hyp	Ref	Expression
1		biimpa.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	biimprd 248	. 2 ⊢ (𝜑 → (𝜒 → 𝜓))
3	2	imp 406	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)

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

This theorem is referenced by:  bitr  804  exbiri  810  biadanid  822  bibiad  839  oplem1  1056  eqtr  2751  pm13.181  3010  opabss  5153  axprlem4OLD  5365  axprlem5OLD  5366  euotd  5451  brcogw  5807  somin1  6079  xpdifid  6115  funfni  6587  fnssres  6604  fn0  6612  fnimadisj  6613  fnimaeq0  6614  foimacnv  6780  fvelimab  6894  dffv2  6917  fvopab3ig  6925  dff3  7033  dffo4  7036  fpr2g  7145  ralima  7171  f1eqcocnv  7235  isomin  7271  f1ocnv2d  7599  fnexALT  7883  xp1st  7953  xp2nd  7954  frrlem3  8218  fpr2  8234  wfr3g  8249  wfr2  8257  iinon  8260  tfr3  8318  oawordri  8465  oaass  8476  omeulem1  8497  oeoa  8512  oeoe  8514  oeeulem  8516  elqsn0  8708  pwdom  9042  enfii  9095  phpeqd  9121  ominf  9148  findcard3  9167  marypha1lem  9317  wofib  9431  cantnff  9564  cantnfp1  9571  cantnf  9583  cnfcomlem  9589  ttrcltr  9606  frr3g  9649  r1sscl  9678  rankval3b  9719  infxpidm2  9908  numdom  9929  onssnum  9931  acni  9936  acni2  9937  dfac5  10020  djulepw  10084  infunsdom1  10103  infunsdom  10104  cofsmo  10160  cfsmolem  10161  fin1ai  10184  fin2i  10186  isf34lem1  10263  fin67  10286  itunisuc  10310  axdc3lem4  10344  zornn0g  10396  ttukeylem6  10405  brdom3  10419  tsken  10645  tskcard  10672  r1tskina  10673  intgru  10705  prlem934  10924  ltexprlem7  10933  supaddc  12089  mul2lt0rlt0  12994  xrmaxeq  13078  xrmineq  13079  xmulneg1  13168  ixxun  13261  difelfzle  13541  ssfzoulel  13660  elfznelfzo  13673  ico01fl0  13723  btwnzge0  13732  ltdifltdiv  13738  ioopnfsup  13768  icopnfsup  13769  modifeq2int  13840  suppssfz  13901  expmordi  14074  zzlesq  14113  faclbnd4lem4  14203  hasheni  14255  hashgt0  14295  hashge1  14296  hashprb  14304  lennncl  14441  wrdsymb0  14456  ccatsymb  14490  ccatlid  14494  ccatass  14496  ccatswrd  14576  swrdccat2  14577  ccatpfx  14608  swrdccatfn  14631  swrdccat  14642  revccat  14673  2cshw  14720  cnpart  15147  resqreu  15159  recval  15230  abs1m  15243  abslem2  15247  fzomaxdiflem  15250  sqreulem  15267  sqreu  15268  limsupgre  15388  rlimdiv  15553  fsumparts  15713  climcnds  15758  expcnv  15771  ntrivcvg  15804  mod2eq1n2dvds  16258  ndvdssub  16320  sadcaddlem  16368  rplpwr  16469  dvdssqlem  16477  algcvgblem  16488  eucalgcvga  16497  isprm2lem  16592  powm2modprm  16715  coprimeprodsq  16720  pythagtriplem11  16737  pythagtriplem13  16739  pcadd2  16802  4sqlem11  16867  vdwlem6  16898  vdwlem8  16900  vdwlem10  16902  ramval  16920  ramcl2  16928  ramlb  16931  ram0  16934  mreintcl  17497  mrcval  17516  mrccl  17517  mrcuni  17527  mrcun  17528  acsfiel  17560  rescabs  17740  funcres  17803  setcmon  17994  setcepi  17995  fullestrcsetc  18057  funcsetcestrclem8  18068  fullsetcestrc  18072  yonffthlem  18188  pleval2i  18240  pospo  18249  poslubdg  18318  acsdrsel  18449  acsdrscl  18452  acsficl  18453  psss  18486  chnind  18527  chnub  18528  chnccats1  18531  chnccat  18532  grpidd  18579  ismndd  18664  gsumsgrpccat  18748  gsumwmhm  18753  mulgaddcom  19011  subgmulg  19053  resghm  19144  conjnsg  19166  ghmqusker  19199  f1otrspeq  19359  pmtrval  19363  pmtrrn  19369  pmtrfinv  19373  pmtrprfval  19399  psgnunilem1  19405  psgnunilem5  19406  psgnunilem4  19409  psgneldm2i  19417  lsmelvalix  19553  pj1ghm  19615  efgredlemc  19657  frgp0  19672  qusabl  19777  cycsubgcyg  19813  gsumval3  19819  gsumcllem  19820  ablfac1c  19985  pgpfac1lem5  19993  submomnd  20044  isrngd  20091  isringd  20209  01eq0ring  20445  ornglmullt  20784  orngrmullt  20785  lspsneq0b  20946  lmodindp1  20947  lmhmf1o  20980  lmhmpreima  20982  reslmhm  20986  pwssplit3  20995  lspsncmp  21053  lspsneq  21059  znf1o  21488  dsmmlss  21681  frlmlbs  21734  frlmup1  21735  psrgrp  21893  mpfind  22042  psdmul  22081  ply1scleq  22220  mat1  22362  chfacfisf  22769  chfacfisfcpmat  22770  uniopn  22812  ntrval  22951  clsval  22952  neival  23017  neiptopreu  23048  lpval  23054  restdis  23093  lmbrf  23175  cnpnei  23179  1stcrest  23368  hauspwdom  23416  lfinpfin  23439  txcnpi  23523  ptrescn  23554  xkococnlem  23574  qtopeu  23631  kqreglem1  23656  ptuncnv  23722  filss  23768  fsubbas  23782  fbasrn  23799  cfinfil  23808  ufinffr  23844  elfm3  23865  rnelfmlem  23867  rnelfm  23868  flimclslem  23899  flfval  23905  isfcf  23949  cnextfvval  23980  cnextf  23981  cnextcn  23982  ustelimasn  24138  trust  24144  restutop  24152  ustuqtop2  24157  utop2nei  24165  ucncn  24199  trcfilu  24208  cnextucn  24217  met1stc  24436  metustexhalf  24471  cfilucfil  24474  psmetutop  24482  nmoix  24644  nmoeq0  24651  idnghm  24658  blcvx  24713  xrsxmet  24725  iccntr  24737  icccmp  24741  iihalf1  24852  iihalf2  24855  xrhmeo  24871  cnheibor  24881  ipcau2  25161  lmmbrf  25189  iscauf  25207  cmetcaulem  25215  bcthlem4  25254  cmetcusp  25281  rrxcph  25319  minveclem4  25359  evthicc2  25388  cniccbdd  25389  ovollb2  25417  ovolunlem1a  25424  ovolunlem1  25425  voliun  25482  icombl  25492  ioombl  25493  iccvolcl  25495  ioovolcl  25498  mbfss  25574  mbfposb  25581  itg2const2  25669  itg2splitlem  25676  itg2gt0  25688  iblss2  25734  itgioo  25744  dvaddf  25872  dvmulf  25873  dvcobr  25876  dvcobrOLD  25877  dvcof  25879  rolle  25921  dvlip  25925  c1lip1  25929  dvivthlem1  25940  lhop1lem  25945  dvfsumlem1  25959  ftc1lem4  25973  ftc1lem5  25974  ply1divmo  26068  coe1termlem  26190  plydiveu  26233  taylplem1  26297  pserulm  26358  abelth  26378  abscxp2  26629  abscxpbnd  26690  logbgt0b  26730  ang180lem2  26747  ang180lem3  26748  isosctrlem1  26755  angpieqvd  26768  atandmtan  26857  birthdaylem3  26890  wilthlem2  27006  wilthimp  27009  isppw  27051  isppw2  27052  dvdsflsumcom  27125  chteq0  27147  perfectlem2  27168  dchrval  27172  dchrinvcl  27191  dchrptlem1  27202  bposlem3  27224  lgslem4  27238  lgsmod  27261  lgsdilem  27262  lgsdir2lem2  27264  lgsdir2  27268  lgsne0  27273  lgsmulsqcoprm  27281  lgseisenlem1  27313  2lgsoddprm  27354  2sqlem4  27359  chpo1ubb  27419  dchrisumn0  27459  pntrsumbnd2  27505  ostthlem1  27565  ostth3  27576  nosupbnd2lem1  27654  noinfbnd2lem1  27669  nocvxmin  27718  eqscut2  27747  sltlpss  27853  madefi  27858  absslt  28187  eucliddivs  28301  peano5uzs  28328  idmot  28515  tgelrnln  28608  lmimid  28772  lmiisolem  28774  hypcgrlem1  28777  brcgr  28878  colinearalglem4  28887  colinearalg  28888  axlowdimlem14  28933  axcontlem4  28945  cplgrop  29415  lfgriswlk  29665  pthdlem1  29744  crctcshwlkn0  29799  elwspths2on  29940  elwspths2onw  29941  clwlkclwwlklem2fv2  29976  frgrncvvdeqlem9  30287  nvss  30573  sspn  30716  nmoub3i  30753  nmblolbii  30779  blocnilem  30784  minvecolem4  30860  htthlem  30897  norm1  31229  norm1exi  31230  pjeq  31379  axpjpj  31400  normcan  31556  pjoi0  31697  nmopub2tALT  31889  nmfnleub2  31906  eighmorth  31944  nmbdoplbi  32004  nmcoplbi  32008  nmophmi  32011  nmbdfnlbi  32029  nmcfnlbi  32032  riesz3i  32042  cnlnadjlem7  32053  branmfn  32085  nmopleid  32119  hstle  32210  superpos  32334  cvexchlem  32348  foresf1o  32484  elabreximd  32490  prssad  32509  prssbd  32510  unidifsnne  32516  tpssad  32519  f1o3d  32608  fmptco1f1o  32615  funcnvmpt  32649  fgreu  32654  suppovss  32662  elsuppfnd  32663  fsupprnfi  32673  resf1o  32713  fpwrelmap  32716  argcj  32732  xrofsup  32750  eliccelico  32760  elicoelioo  32761  iocinif  32764  difioo  32765  hashpss  32791  hashne0  32792  elq2  32794  oexpled  32830  indf1ofs  32847  eliccioo  32911  cshf1o  32943  mgcmnt1d  32978  mgcmnt2d  32979  pwrssmgc  32981  mndlactf1o  33011  mndractf1o  33012  gsummpt2co  33028  gsumhashmul  33041  symgcom  33052  symgcom2  33053  odpmco  33055  pmtrcnel  33058  pmtridf1o  33063  cycpmco2lem6  33100  cycpmco2lem7  33101  cycpmco2  33102  cyc3co2  33109  cycpmconjv  33111  tocyccntz  33113  cyc3evpm  33119  cycpmconjslem2  33124  cycpmconjs  33125  fxpsubm  33141  fxpsubg  33142  fxpsubrg  33143  fxpsdrg  33144  archirngz  33158  unitnz  33206  elrgspnlem1  33209  elrgspnlem2  33210  elrgspnlem4  33212  elrgspnsubrun  33216  rloccring  33237  rlocf1  33240  domnpropd  33243  rrgsubm  33250  isdrng4  33261  sdrgdvcl  33265  sdrginvcl  33266  fracfld  33274  lindssn  33343  linds2eq  33346  dvdsrspss  33352  nsgqusf1olem1  33378  nsgqusf1olem3  33380  unitpidl1  33389  elrspunidl  33393  rhmimaidl  33397  drngidlhash  33399  prmidl2  33406  prmidl0  33415  qsidomlem1  33417  ssdifidlprm  33423  mxidlirredi  33436  mxidlirred  33437  ssmxidl  33439  drng0mxidl  33441  opprmxidlabs  33452  qsdrngilem  33459  qsdrngi  33460  qsdrng  33462  rsprprmprmidl  33487  rsprprmprmidlb  33488  rprmasso2  33491  rprmirredlem  33495  rprmirredb  33497  1arithidomlem2  33501  1arithufdlem4  33512  1arithufd  33513  ressply1evls1  33528  ply1asclunit  33537  ply1dg1rt  33543  ply1mulrtss  33545  ply1dg3rt0irred  33546  ply1degltlss  33557  ply1gsumz  33559  esplyfv1  33590  lsssra  33600  exsslsb  33609  lbslsat  33629  lindsunlem  33637  lindsun  33638  dimkerim  33640  fedgmullem1  33642  fedgmullem2  33643  fedgmul  33644  dimlssid  33645  lvecendof1f1o  33646  assalactf1o  33648  sdrgfldext  33663  fldsdrgfldext  33674  fldgenfldext  33681  evls1fldgencl  33683  fldextrspunlsp  33687  fldextrspunlem1  33688  fldextrspunfld  33689  irngss  33700  0ringirng  33702  irngnzply1  33704  extdgfialglem1  33705  irngnminplynz  33725  minplyelirng  33728  irredminply  33729  algextdeglem2  33731  algextdeglem4  33733  constrconj  33758  constrextdg2lem  33761  constrext2chnlem  33763  iconstr  33779  constrsdrg  33788  cos9thpiminplylem1  33795  cos9thpiminplylem2  33796  cos9thpiminplylem3  33797  cos9thpiminplylem5  33799  madjusmdetlem2  33841  qtophaus  33849  locfinreflem  33853  zarclssn  33886  zarmxt1  33893  zarcmplem  33894  rhmpreimacn  33898  unitdivcld  33914  tpr2rico  33925  ordtrestNEW  33934  lmxrge0  33965  elzrhunit  33990  qqhf  33999  gsumesum  34072  esumfsup  34083  esumcvg  34099  issgon  34136  sigainb  34149  insiga  34150  isrnmeas  34213  measvunilem  34225  volmeas  34244  ddeval1  34247  ddeval0  34248  imambfm  34275  omssubadd  34313  carsgclctunlem3  34333  eulerpartlemf  34383  eulerpartlemgvv  34389  probun  34432  dstfrvunirn  34488  plymulx  34561  signslema  34575  signstfvn  34582  signsvtn0  34583  signstfvneq0  34585  signstres  34588  signstfveq0a  34589  breprexplemc  34645  logdivsqrle  34663  hgt750lemg  34667  tgoldbachgtda  34674  tgoldbachgt  34676  lpadmax  34695  lpadleft  34696  lpadright  34697  bnj529  34753  bnj548  34909  bnj570  34917  bnj852  34933  bnj929  34948  bnj1097  34993  bnj1118  34996  bnj1145  35005  funen1cnv  35100  fissorduni  35101  spthcycl  35173  acycgr0v  35192  derangen  35216  subfacp1lem2b  35225  subfacp1lem4  35227  subfacp1lem5  35228  derangfmla  35234  ptpconn  35277  mppspstlem  35615  wsuclem  35867  colinearex  36104  btwnconn1lem11  36141  btwnconn1lem12  36142  fwddifnp1  36209  nn0prpwlem  36366  bj-snmoore  37157  bj-imdiridlem  37229  relowlpssretop  37408  fin2so  37657  matunitlindflem2  37667  ptrecube  37670  poimirlem8  37678  poimirlem13  37683  poimirlem15  37685  poimirlem24  37694  poimirlem25  37695  poimirlem26  37696  heicant  37705  mblfinlem2  37708  voliunnfl  37714  mbfresfi  37716  itg2addnclem  37721  itg2addnclem3  37723  itg2gt0cn  37725  ftc1cnnclem  37741  ftc1anclem5  37747  cover2  37765  indexdom  37784  sdclem1  37793  fdc  37795  equivbnd2  37842  heiborlem8  37868  heibor  37871  isdrngo2  38008  iscringd  38048  smprngopr  38102  prnc  38117  eqbrtr  38283  eqeltr  38285  islfld  39171  lkrshpor  39216  lfl1dim  39230  lfl1dim2N  39231  cmtcomlemN  39357  2lplnmN  39668  pmapjat1  39962  trlnid  40288  tendoex  41084  dia1dimid  41172  dibval2  41253  dihmeetlem2N  41408  dochlkr  41494  mapdcv  41769  hdmaplkr  42022  hdmapip0  42024  hlhillcs  42067  aks6d1c6lem4  42276  dvdsexpnn  42436  readvrec  42465  frlmvscadiccat  42609  psrmnd  42648  nacsfix  42815  3rexfrabdioph  42900  4rexfrabdioph  42901  6rexfrabdioph  42902  7rexfrabdioph  42903  eldioph4b  42914  pellexlem2  42933  pellexlem5  42936  jm2.26lem3  43104  numinfctb  43206  ordne0gt0  43364  omge1  43400  omlim2  43402  omord2lim  43403  omord2i  43404  tfsconcatfv  43444  tfsconcatb0  43447  oaun3lem1  43477  ntrclsfv1  44158  ntrneifv1  44182  ntrneifv2  44183  cvgdvgrat  44416  radcnvrat  44417  dvconstbi  44437  bccbc  44448  elpwgded  44667  elpwgdedVD  45019  sspwimpcf  45022  sspwimpcfVD  45023  sspwimpALT2  45030  ax6e2ndeqALT  45033  eliuniin  45206  eliuniin2  45227  qinioo  45645  dfxlim2v  45955  xlimliminflimsup  45970  cncfiooicclem1  46001  ibliooicc  46079  stoweidlem27  46135  stoweidlem28  46136  fourierdlem89  46303  fourierdlem91  46305  fourierdlem92  46306  smflimmpt  46918  odz2prm2pw  47673  perfectALTVlem2  47832  blen1b  48699  naryfvalelfv  48743  itscnhlc0yqe  48870  itsclquadb  48887  lubeldm2  49066  glbeldm2  49067  ipolub  49098  ipoglb  49101  fucofulem1  49421  functhinclem1  49555  thincciso  49564  prsthinc  49575  functermclem  49618  prstchom2ALT  49675  onetansqsecsq  49872  cotsqcscsq  49873  aacllem  49912