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  2749  pm13.181  3007  opabss  5156  axprlem4OLD  5368  axprlem5OLD  5369  euotd  5456  brcogw  5811  somin1  6082  xpdifid  6117  funfni  6588  fnssres  6605  fn0  6613  fnimadisj  6614  fnimaeq0  6615  foimacnv  6781  fvelimab  6895  dffv2  6918  fvopab3ig  6926  dff3  7034  dffo4  7037  fpr2g  7147  ralima  7173  f1eqcocnv  7238  isomin  7274  f1ocnv2d  7602  fnexALT  7886  xp1st  7956  xp2nd  7957  frrlem3  8221  fpr2  8237  wfr3g  8252  wfr2  8260  iinon  8263  tfr3  8321  oawordri  8468  oaass  8479  omeulem1  8500  oeoa  8515  oeoe  8517  oeeulem  8519  elqsn0  8711  pwdom  9046  enfii  9100  phpeqd  9126  ominf  9153  findcard3  9172  marypha1lem  9323  wofib  9437  cantnff  9570  cantnfp1  9577  cantnf  9589  cnfcomlem  9595  ttrcltr  9612  frr3g  9652  r1sscl  9681  rankval3b  9722  infxpidm2  9911  numdom  9932  onssnum  9934  acni  9939  acni2  9940  dfac5  10023  djulepw  10087  infunsdom1  10106  infunsdom  10107  cofsmo  10163  cfsmolem  10164  fin1ai  10187  fin2i  10189  isf34lem1  10266  fin67  10289  itunisuc  10313  axdc3lem4  10347  zornn0g  10399  ttukeylem6  10408  brdom3  10422  tsken  10648  tskcard  10675  r1tskina  10676  intgru  10708  prlem934  10927  ltexprlem7  10936  supaddc  12092  mul2lt0rlt0  12997  xrmaxeq  13081  xrmineq  13082  xmulneg1  13171  ixxun  13264  difelfzle  13544  ssfzoulel  13663  elfznelfzo  13675  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  14489  ccatlid  14493  ccatass  14495  ccatswrd  14575  swrdccat2  14576  ccatpfx  14607  swrdccatfn  14630  swrdccat  14641  revccat  14672  2cshw  14719  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  grpidd  18545  ismndd  18630  gsumsgrpccat  18714  gsumwmhm  18719  mulgaddcom  18977  subgmulg  19019  resghm  19111  conjnsg  19133  ghmqusker  19166  f1otrspeq  19326  pmtrval  19330  pmtrrn  19336  pmtrfinv  19340  pmtrprfval  19366  psgnunilem1  19372  psgnunilem5  19373  psgnunilem4  19376  psgneldm2i  19384  lsmelvalix  19520  pj1ghm  19582  efgredlemc  19624  frgp0  19639  qusabl  19744  cycsubgcyg  19780  gsumval3  19786  gsumcllem  19787  ablfac1c  19952  pgpfac1lem5  19960  submomnd  20011  isrngd  20058  isringd  20176  01eq0ring  20415  ornglmullt  20754  orngrmullt  20755  lspsneq0b  20916  lmodindp1  20917  lmhmf1o  20950  lmhmpreima  20952  reslmhm  20956  pwssplit3  20965  lspsncmp  21023  lspsneq  21029  znf1o  21458  dsmmlss  21651  frlmlbs  21704  frlmup1  21705  psrgrp  21863  mpfind  22012  psdmul  22051  ply1scleq  22190  mat1  22332  chfacfisf  22739  chfacfisfcpmat  22740  uniopn  22782  ntrval  22921  clsval  22922  neival  22987  neiptopreu  23018  lpval  23024  restdis  23063  lmbrf  23145  cnpnei  23149  1stcrest  23338  hauspwdom  23386  lfinpfin  23409  txcnpi  23493  ptrescn  23524  xkococnlem  23544  qtopeu  23601  kqreglem1  23626  ptuncnv  23692  filss  23738  fsubbas  23752  fbasrn  23769  cfinfil  23778  ufinffr  23814  elfm3  23835  rnelfmlem  23837  rnelfm  23838  flimclslem  23869  flfval  23875  isfcf  23919  cnextfvval  23950  cnextf  23951  cnextcn  23952  ustelimasn  24108  trust  24115  restutop  24123  ustuqtop2  24128  utop2nei  24136  ucncn  24170  trcfilu  24179  cnextucn  24188  met1stc  24407  metustexhalf  24442  cfilucfil  24445  psmetutop  24453  nmoix  24615  nmoeq0  24622  idnghm  24629  blcvx  24684  xrsxmet  24696  iccntr  24708  icccmp  24712  iihalf1  24823  iihalf2  24826  xrhmeo  24842  cnheibor  24852  ipcau2  25132  lmmbrf  25160  iscauf  25178  cmetcaulem  25186  bcthlem4  25225  cmetcusp  25252  rrxcph  25290  minveclem4  25330  evthicc2  25359  cniccbdd  25360  ovollb2  25388  ovolunlem1a  25395  ovolunlem1  25396  voliun  25453  icombl  25463  ioombl  25464  iccvolcl  25466  ioovolcl  25469  mbfss  25545  mbfposb  25552  itg2const2  25640  itg2splitlem  25647  itg2gt0  25659  iblss2  25705  itgioo  25715  dvaddf  25843  dvmulf  25844  dvcobr  25847  dvcobrOLD  25848  dvcof  25850  rolle  25892  dvlip  25896  c1lip1  25900  dvivthlem1  25911  lhop1lem  25916  dvfsumlem1  25930  ftc1lem4  25944  ftc1lem5  25945  ply1divmo  26039  coe1termlem  26161  plydiveu  26204  taylplem1  26268  pserulm  26329  abelth  26349  abscxp2  26600  abscxpbnd  26661  logbgt0b  26701  ang180lem2  26718  ang180lem3  26719  isosctrlem1  26726  angpieqvd  26739  atandmtan  26828  birthdaylem3  26861  wilthlem2  26977  wilthimp  26980  isppw  27022  isppw2  27023  dvdsflsumcom  27096  chteq0  27118  perfectlem2  27139  dchrval  27143  dchrinvcl  27162  dchrptlem1  27173  bposlem3  27195  lgslem4  27209  lgsmod  27232  lgsdilem  27233  lgsdir2lem2  27235  lgsdir2  27239  lgsne0  27244  lgsmulsqcoprm  27252  lgseisenlem1  27284  2lgsoddprm  27325  2sqlem4  27330  chpo1ubb  27390  dchrisumn0  27430  pntrsumbnd2  27476  ostthlem1  27536  ostth3  27547  nosupbnd2lem1  27625  noinfbnd2lem1  27640  nocvxmin  27689  eqscut2  27717  sltlpss  27822  madefi  27827  absslt  28156  eucliddivs  28270  peano5uzs  28297  idmot  28482  tgelrnln  28575  lmimid  28739  lmiisolem  28741  hypcgrlem1  28744  brcgr  28845  colinearalglem4  28854  colinearalg  28855  axlowdimlem14  28900  axcontlem4  28912  cplgrop  29382  lfgriswlk  29632  pthdlem1  29711  crctcshwlkn0  29766  elwspths2on  29905  clwlkclwwlklem2fv2  29940  frgrncvvdeqlem9  30251  nvss  30537  sspn  30680  nmoub3i  30717  nmblolbii  30743  blocnilem  30748  minvecolem4  30824  htthlem  30861  norm1  31193  norm1exi  31194  pjeq  31343  axpjpj  31364  normcan  31520  pjoi0  31661  nmopub2tALT  31853  nmfnleub2  31870  eighmorth  31908  nmbdoplbi  31968  nmcoplbi  31972  nmophmi  31975  nmbdfnlbi  31993  nmcfnlbi  31996  riesz3i  32006  cnlnadjlem7  32017  branmfn  32049  nmopleid  32083  hstle  32174  superpos  32298  cvexchlem  32312  foresf1o  32448  elabreximd  32454  prssad  32473  prssbd  32474  unidifsnne  32480  tpssad  32483  f1o3d  32569  fmptco1f1o  32576  funcnvmpt  32610  fgreu  32615  suppovss  32623  elsuppfnd  32624  fsupprnfi  32634  resf1o  32673  fpwrelmap  32676  argcj  32692  xrofsup  32710  eliccelico  32720  elicoelioo  32721  iocinif  32724  difioo  32725  hashpss  32754  hashne0  32755  elq2  32756  oexpled  32792  indf1ofs  32809  eliccioo  32871  cshf1o  32904  mgcmnt1d  32939  mgcmnt2d  32940  pwrssmgc  32942  chnind  32953  chnub  32954  chnccats1  32957  mndlactf1o  32984  mndractf1o  32985  gsummpt2co  33001  gsumhashmul  33014  symgcom  33025  symgcom2  33026  odpmco  33028  pmtrcnel  33031  pmtridf1o  33036  cycpmco2lem6  33073  cycpmco2lem7  33074  cycpmco2  33075  cyc3co2  33082  cycpmconjv  33084  tocyccntz  33086  cyc3evpm  33092  cycpmconjslem2  33097  cycpmconjs  33098  fxpsubm  33114  fxpsubg  33115  fxpsubrg  33116  fxpsdrg  33117  archirngz  33131  unitnz  33179  elrgspnlem1  33182  elrgspnlem2  33183  elrgspnlem4  33185  elrgspnsubrun  33189  rloccring  33210  rlocf1  33213  domnpropd  33216  rrgsubm  33223  isdrng4  33234  sdrgdvcl  33238  sdrginvcl  33239  fracfld  33247  lindssn  33315  linds2eq  33318  dvdsrspss  33324  nsgqusf1olem1  33350  nsgqusf1olem3  33352  unitpidl1  33361  elrspunidl  33365  rhmimaidl  33369  drngidlhash  33371  prmidl2  33378  prmidl0  33387  qsidomlem1  33389  ssdifidlprm  33395  mxidlirredi  33408  mxidlirred  33409  ssmxidl  33411  drng0mxidl  33413  opprmxidlabs  33424  qsdrngilem  33431  qsdrngi  33432  qsdrng  33434  rsprprmprmidl  33459  rsprprmprmidlb  33460  rprmasso2  33463  rprmirredlem  33467  rprmirredb  33469  1arithidomlem2  33473  1arithufdlem4  33484  1arithufd  33485  ressply1evls1  33500  ply1asclunit  33509  ply1dg1rt  33515  ply1mulrtss  33517  ply1dg3rt0irred  33518  ply1degltlss  33529  ply1gsumz  33531  lsssra  33554  exsslsb  33563  lbslsat  33583  lindsunlem  33591  lindsun  33592  dimkerim  33594  fedgmullem1  33596  fedgmullem2  33597  fedgmul  33598  dimlssid  33599  lvecendof1f1o  33600  assalactf1o  33602  sdrgfldext  33617  fldsdrgfldext  33628  fldgenfldext  33635  evls1fldgencl  33637  fldextrspunlsp  33641  fldextrspunlem1  33642  fldextrspunfld  33643  irngss  33654  0ringirng  33656  irngnzply1  33658  extdgfialglem1  33659  irngnminplynz  33679  minplyelirng  33682  irredminply  33683  algextdeglem2  33685  algextdeglem4  33687  constrconj  33712  constrextdg2lem  33715  constrext2chnlem  33717  iconstr  33733  constrsdrg  33742  cos9thpiminplylem1  33749  cos9thpiminplylem2  33750  cos9thpiminplylem3  33751  cos9thpiminplylem5  33753  madjusmdetlem2  33795  qtophaus  33803  locfinreflem  33807  zarclssn  33840  zarmxt1  33847  zarcmplem  33848  rhmpreimacn  33852  unitdivcld  33868  tpr2rico  33879  ordtrestNEW  33888  lmxrge0  33919  elzrhunit  33944  qqhf  33953  gsumesum  34026  esumfsup  34037  esumcvg  34053  issgon  34090  sigainb  34103  insiga  34104  isrnmeas  34167  measvunilem  34179  volmeas  34198  ddeval1  34201  ddeval0  34202  imambfm  34230  omssubadd  34268  carsgclctunlem3  34288  eulerpartlemf  34338  eulerpartlemgvv  34344  probun  34387  dstfrvunirn  34443  plymulx  34516  signslema  34530  signstfvn  34537  signsvtn0  34538  signstfvneq0  34540  signstres  34543  signstfveq0a  34544  breprexplemc  34600  logdivsqrle  34618  hgt750lemg  34622  tgoldbachgtda  34629  tgoldbachgt  34631  lpadmax  34650  lpadleft  34651  lpadright  34652  bnj529  34708  bnj548  34864  bnj570  34872  bnj852  34888  bnj929  34903  bnj1097  34948  bnj1118  34951  bnj1145  34960  funen1cnv  35055  spthcycl  35106  acycgr0v  35125  derangen  35149  subfacp1lem2b  35158  subfacp1lem4  35160  subfacp1lem5  35161  derangfmla  35167  ptpconn  35210  mppspstlem  35548  wsuclem  35803  colinearex  36038  btwnconn1lem11  36075  btwnconn1lem12  36076  fwddifnp1  36143  nn0prpwlem  36300  bj-snmoore  37091  bj-imdiridlem  37163  relowlpssretop  37342  fin2so  37591  matunitlindflem2  37601  ptrecube  37604  poimirlem8  37612  poimirlem13  37617  poimirlem15  37619  poimirlem24  37628  poimirlem25  37629  poimirlem26  37630  heicant  37639  mblfinlem2  37642  voliunnfl  37648  mbfresfi  37650  itg2addnclem  37655  itg2addnclem3  37657  itg2gt0cn  37659  ftc1cnnclem  37675  ftc1anclem5  37681  cover2  37699  indexdom  37718  sdclem1  37727  fdc  37729  equivbnd2  37776  heiborlem8  37802  heibor  37805  isdrngo2  37942  iscringd  37982  smprngopr  38036  prnc  38051  eqbrtr  38210  eqeltr  38212  islfld  39045  lkrshpor  39090  lfl1dim  39104  lfl1dim2N  39105  cmtcomlemN  39231  2lplnmN  39542  pmapjat1  39836  trlnid  40162  tendoex  40958  dia1dimid  41046  dibval2  41127  dihmeetlem2N  41282  dochlkr  41368  mapdcv  41643  hdmaplkr  41896  hdmapip0  41898  hlhillcs  41941  aks6d1c6lem4  42150  dvdsexpnn  42310  readvrec  42339  frlmvscadiccat  42483  psrmnd  42522  nacsfix  42689  3rexfrabdioph  42774  4rexfrabdioph  42775  6rexfrabdioph  42776  7rexfrabdioph  42777  eldioph4b  42788  pellexlem2  42807  pellexlem5  42810  jm2.26lem3  42978  numinfctb  43080  ordne0gt0  43238  omge1  43274  omlim2  43276  omord2lim  43277  omord2i  43278  tfsconcatfv  43318  tfsconcatb0  43321  oaun3lem1  43351  ntrclsfv1  44032  ntrneifv1  44056  ntrneifv2  44057  cvgdvgrat  44290  radcnvrat  44291  dvconstbi  44311  bccbc  44322  elpwgded  44542  elpwgdedVD  44894  sspwimpcf  44897  sspwimpcfVD  44898  sspwimpALT2  44905  ax6e2ndeqALT  44908  eliuniin  45081  eliuniin2  45102  qinioo  45520  dfxlim2v  45832  xlimliminflimsup  45847  cncfiooicclem1  45878  ibliooicc  45956  stoweidlem27  46012  stoweidlem28  46013  fourierdlem89  46180  fourierdlem91  46182  fourierdlem92  46183  smflimmpt  46795  odz2prm2pw  47551  perfectALTVlem2  47710  blen1b  48577  naryfvalelfv  48621  itscnhlc0yqe  48748  itsclquadb  48765  lubeldm2  48944  glbeldm2  48945  ipolub  48976  ipoglb  48979  fucofulem1  49299  functhinclem1  49433  thincciso  49442  prsthinc  49453  functermclem  49496  prstchom2ALT  49553  onetansqsecsq  49750  cotsqcscsq  49751  aacllem  49790