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  805  exbiri  811  biadanid  823  bibiad  840  oplem1  1057  eqtr  2757  pm13.181  3015  opabss  5164  axprlem4OLD  5376  axprlem5OLD  5377  euotd  5469  brcogw  5825  somin1  6098  xpdifid  6134  funfni  6606  fnssres  6623  fn0  6631  fnimadisj  6632  fnimaeq0  6633  foimacnv  6799  fvelimab  6914  dffv2  6937  fvopab3ig  6945  funcnvmpt  6951  dff3  7054  dffo4  7057  fpr2g  7167  ralima  7193  f1eqcocnv  7257  isomin  7293  f1ocnv2d  7621  fnexALT  7905  xp1st  7975  xp2nd  7976  frrlem3  8240  fpr2  8256  wfr3g  8271  wfr2  8279  iinon  8282  tfr3  8340  oawordri  8487  oaass  8498  omeulem1  8519  oeoa  8535  oeoe  8537  oeeulem  8539  elqsn0  8733  pwdom  9069  enfii  9122  phpeqd  9148  ominf  9176  findcard3  9195  marypha1lem  9348  wofib  9462  cantnff  9595  cantnfp1  9602  cantnf  9614  cnfcomlem  9620  ttrcltr  9637  frr3g  9680  r1sscl  9709  rankval3b  9750  infxpidm2  9939  numdom  9960  onssnum  9962  acni  9967  acni2  9968  dfac5  10051  djulepw  10115  infunsdom1  10134  infunsdom  10135  cofsmo  10191  cfsmolem  10192  fin1ai  10215  fin2i  10217  isf34lem1  10294  fin67  10317  itunisuc  10341  axdc3lem4  10375  zornn0g  10427  ttukeylem6  10436  brdom3  10450  tsken  10677  tskcard  10704  r1tskina  10705  intgru  10737  prlem934  10956  ltexprlem7  10965  supaddc  12121  mul2lt0rlt0  13021  xrmaxeq  13106  xrmineq  13107  xmulneg1  13196  ixxun  13289  difelfzle  13569  ssfzoulel  13688  elfznelfzo  13701  ico01fl0  13751  btwnzge0  13760  ltdifltdiv  13766  ioopnfsup  13796  icopnfsup  13797  modifeq2int  13868  suppssfz  13929  expmordi  14102  zzlesq  14141  faclbnd4lem4  14231  hasheni  14283  hashgt0  14323  hashge1  14324  hashprb  14332  lennncl  14469  wrdsymb0  14484  ccatsymb  14518  ccatlid  14522  ccatass  14524  ccatswrd  14604  swrdccat2  14605  ccatpfx  14636  swrdccatfn  14659  swrdccat  14670  revccat  14701  2cshw  14748  cnpart  15175  resqreu  15187  recval  15258  abs1m  15271  abslem2  15275  fzomaxdiflem  15278  sqreulem  15295  sqreu  15296  limsupgre  15416  rlimdiv  15581  fsumparts  15741  climcnds  15786  expcnv  15799  ntrivcvg  15832  mod2eq1n2dvds  16286  ndvdssub  16348  sadcaddlem  16396  rplpwr  16497  dvdssqlem  16505  algcvgblem  16516  eucalgcvga  16525  isprm2lem  16620  powm2modprm  16743  coprimeprodsq  16748  pythagtriplem11  16765  pythagtriplem13  16767  pcadd2  16830  4sqlem11  16895  vdwlem6  16926  vdwlem8  16928  vdwlem10  16930  ramval  16948  ramcl2  16956  ramlb  16959  ram0  16962  mreintcl  17526  mrcval  17545  mrccl  17546  mrcuni  17556  mrcun  17557  acsfiel  17589  rescabs  17769  funcres  17832  setcmon  18023  setcepi  18024  fullestrcsetc  18086  funcsetcestrclem8  18097  fullsetcestrc  18101  yonffthlem  18217  pleval2i  18269  pospo  18278  poslubdg  18347  acsdrsel  18478  acsdrscl  18481  acsficl  18482  psss  18515  chnind  18556  chnub  18557  chnccats1  18560  chnccat  18561  grpidd  18608  ismndd  18693  gsumsgrpccat  18777  gsumwmhm  18782  mulgaddcom  19043  subgmulg  19085  resghm  19176  conjnsg  19198  ghmqusker  19231  f1otrspeq  19391  pmtrval  19395  pmtrrn  19401  pmtrfinv  19405  pmtrprfval  19431  psgnunilem1  19437  psgnunilem5  19438  psgnunilem4  19441  psgneldm2i  19449  lsmelvalix  19585  pj1ghm  19647  efgredlemc  19689  frgp0  19704  qusabl  19809  cycsubgcyg  19845  gsumval3  19851  gsumcllem  19852  ablfac1c  20017  pgpfac1lem5  20025  submomnd  20076  isrngd  20123  isringd  20241  01eq0ring  20478  ornglmullt  20817  orngrmullt  20818  lspsneq0b  20979  lmodindp1  20980  lmhmf1o  21013  lmhmpreima  21015  reslmhm  21019  pwssplit3  21028  lspsncmp  21086  lspsneq  21092  znf1o  21521  dsmmlss  21714  frlmlbs  21767  frlmup1  21768  psrgrp  21927  mpfind  22085  psdmul  22124  ply1scleq  22264  mat1  22406  chfacfisf  22813  chfacfisfcpmat  22814  uniopn  22856  ntrval  22995  clsval  22996  neival  23061  neiptopreu  23092  lpval  23098  restdis  23137  lmbrf  23219  cnpnei  23223  1stcrest  23412  hauspwdom  23460  lfinpfin  23483  txcnpi  23567  ptrescn  23598  xkococnlem  23618  qtopeu  23675  kqreglem1  23700  ptuncnv  23766  filss  23812  fsubbas  23826  fbasrn  23843  cfinfil  23852  ufinffr  23888  elfm3  23909  rnelfmlem  23911  rnelfm  23912  flimclslem  23943  flfval  23949  isfcf  23993  cnextfvval  24024  cnextf  24025  cnextcn  24026  ustelimasn  24182  trust  24188  restutop  24196  ustuqtop2  24201  utop2nei  24209  ucncn  24243  trcfilu  24252  cnextucn  24261  met1stc  24480  metustexhalf  24515  cfilucfil  24518  psmetutop  24526  nmoix  24688  nmoeq0  24695  idnghm  24702  blcvx  24757  xrsxmet  24769  iccntr  24781  icccmp  24785  iihalf1  24896  iihalf2  24899  xrhmeo  24915  cnheibor  24925  ipcau2  25205  lmmbrf  25233  iscauf  25251  cmetcaulem  25259  bcthlem4  25298  cmetcusp  25325  rrxcph  25363  minveclem4  25403  evthicc2  25432  cniccbdd  25433  ovollb2  25461  ovolunlem1a  25468  ovolunlem1  25469  voliun  25526  icombl  25536  ioombl  25537  iccvolcl  25539  ioovolcl  25542  mbfss  25618  mbfposb  25625  itg2const2  25713  itg2splitlem  25720  itg2gt0  25732  iblss2  25778  itgioo  25788  dvaddf  25916  dvmulf  25917  dvcobr  25920  dvcobrOLD  25921  dvcof  25923  rolle  25965  dvlip  25969  c1lip1  25973  dvivthlem1  25984  lhop1lem  25989  dvfsumlem1  26003  ftc1lem4  26017  ftc1lem5  26018  ply1divmo  26112  coe1termlem  26234  plydiveu  26277  taylplem1  26341  pserulm  26402  abelth  26422  abscxp2  26673  abscxpbnd  26734  logbgt0b  26774  ang180lem2  26791  ang180lem3  26792  isosctrlem1  26799  angpieqvd  26812  atandmtan  26901  birthdaylem3  26934  wilthlem2  27050  wilthimp  27053  isppw  27095  isppw2  27096  dvdsflsumcom  27169  chteq0  27191  perfectlem2  27212  dchrval  27216  dchrinvcl  27235  dchrptlem1  27246  bposlem3  27268  lgslem4  27282  lgsmod  27305  lgsdilem  27306  lgsdir2lem2  27308  lgsdir2  27312  lgsne0  27317  lgsmulsqcoprm  27325  lgseisenlem1  27357  2lgsoddprm  27398  2sqlem4  27403  chpo1ubb  27463  dchrisumn0  27503  pntrsumbnd2  27549  ostthlem1  27609  ostth3  27620  nosupbnd2lem1  27698  noinfbnd2lem1  27713  nocvxmin  27766  eqcuts2  27797  ltslpss  27919  madefi  27924  abslts  28260  eucliddivs  28387  peano5uzs  28415  z12bdaylem1  28481  elreno2  28506  idmot  28625  tgelrnln  28718  lmimid  28882  lmiisolem  28884  hypcgrlem1  28887  brcgr  28989  colinearalglem4  28998  colinearalg  28999  axlowdimlem14  29044  axcontlem4  29056  cplgrop  29526  lfgriswlk  29776  pthdlem1  29855  crctcshwlkn0  29910  elwspths2on  30051  elwspths2onw  30052  clwlkclwwlklem2fv2  30087  frgrncvvdeqlem9  30398  nvss  30685  sspn  30828  nmoub3i  30865  nmblolbii  30891  blocnilem  30896  minvecolem4  30972  htthlem  31009  norm1  31341  norm1exi  31342  pjeq  31491  axpjpj  31512  normcan  31668  pjoi0  31809  nmopub2tALT  32001  nmfnleub2  32018  eighmorth  32056  nmbdoplbi  32116  nmcoplbi  32120  nmophmi  32123  nmbdfnlbi  32141  nmcfnlbi  32144  riesz3i  32154  cnlnadjlem7  32165  branmfn  32197  nmopleid  32231  hstle  32322  superpos  32446  cvexchlem  32460  foresf1o  32595  elabreximd  32601  prssad  32620  prssbd  32621  unidifsnne  32627  tpssad  32630  fresunsn  32719  f1o3d  32720  fmptco1f1o  32727  fgreu  32765  suppovss  32775  elsuppfnd  32776  fsupprnfi  32786  resf1o  32824  fpwrelmap  32827  argcj  32843  xrofsup  32862  eliccelico  32872  elicoelioo  32873  iocinif  32876  difioo  32877  hashpss  32904  hashne0  32905  elq2  32907  oexpled  32943  indf1ofs  32963  eliccioo  33027  cshf1o  33059  mgcmnt1d  33094  mgcmnt2d  33095  pwrssmgc  33097  mndlactf1o  33127  mndractf1o  33128  gsummpt2co  33146  gsumhashmul  33165  gsummulsubdishift1  33166  symgcom  33181  symgcom2  33182  odpmco  33184  pmtrcnel  33187  pmtridf1o  33192  cycpmco2lem6  33229  cycpmco2lem7  33230  cycpmco2  33231  cyc3co2  33238  cycpmconjv  33240  tocyccntz  33242  cyc3evpm  33248  cycpmconjslem2  33253  cycpmconjs  33254  fxpsubm  33270  fxpsubg  33271  fxpsubrg  33272  fxpsdrg  33273  archirngz  33287  unitnz  33337  elrgspnlem1  33340  elrgspnlem2  33341  elrgspnlem4  33343  elrgspnsubrun  33347  rloccring  33368  rlocf1  33371  domnpropd  33375  rrgsubm  33382  isdrng4  33393  sdrgdvcl  33397  sdrginvcl  33398  fracfld  33406  lindssn  33475  linds2eq  33478  dvdsrspss  33484  nsgqusf1olem1  33510  nsgqusf1olem3  33512  unitpidl1  33521  elrspunidl  33525  rhmimaidl  33529  drngidlhash  33531  prmidl2  33538  prmidl0  33547  qsidomlem1  33549  ssdifidlprm  33555  mxidlirredi  33568  mxidlirred  33569  ssmxidl  33571  drng0mxidl  33573  opprmxidlabs  33584  qsdrngilem  33591  qsdrngi  33592  qsdrng  33594  rsprprmprmidl  33619  rsprprmprmidlb  33620  rprmasso2  33623  rprmirredlem  33627  rprmirredb  33629  1arithidomlem2  33633  1arithufdlem4  33644  1arithufd  33645  ressply1evls1  33662  ply1asclunit  33671  ply1dg1rt  33677  ply1mulrtss  33679  ply1dg3rt0irred  33681  ply1degltlss  33693  ply1gsumz  33696  evlextv  33723  esplyfv1  33750  esplyind  33756  vietadeg1  33759  lsssra  33769  exsslsb  33778  lbslsat  33798  lindsunlem  33806  lindsun  33807  dimkerim  33809  fedgmullem1  33811  fedgmullem2  33812  fedgmul  33813  dimlssid  33814  lvecendof1f1o  33815  assalactf1o  33817  sdrgfldext  33832  fldsdrgfldext  33843  fldgenfldext  33850  evls1fldgencl  33852  fldextrspunlsp  33856  fldextrspunlem1  33857  fldextrspunfld  33858  irngss  33869  0ringirng  33871  irngnzply1  33873  extdgfialglem1  33874  irngnminplynz  33894  minplyelirng  33897  irredminply  33898  algextdeglem2  33900  algextdeglem4  33902  constrconj  33927  constrextdg2lem  33930  constrext2chnlem  33932  iconstr  33948  constrsdrg  33957  cos9thpiminplylem1  33964  cos9thpiminplylem2  33965  cos9thpiminplylem3  33966  cos9thpiminplylem5  33968  madjusmdetlem2  34010  qtophaus  34018  locfinreflem  34022  zarclssn  34055  zarmxt1  34062  zarcmplem  34063  rhmpreimacn  34067  unitdivcld  34083  tpr2rico  34094  ordtrestNEW  34103  lmxrge0  34134  elzrhunit  34159  qqhf  34168  gsumesum  34241  esumfsup  34252  esumcvg  34268  issgon  34305  sigainb  34318  insiga  34319  isrnmeas  34382  measvunilem  34394  volmeas  34413  ddeval1  34416  ddeval0  34417  imambfm  34444  omssubadd  34482  carsgclctunlem3  34502  eulerpartlemf  34552  eulerpartlemgvv  34558  probun  34601  dstfrvunirn  34657  plymulx  34730  signslema  34744  signstfvn  34751  signsvtn0  34752  signstfvneq0  34754  signstres  34757  signstfveq0a  34758  breprexplemc  34814  logdivsqrle  34832  hgt750lemg  34836  tgoldbachgtda  34843  tgoldbachgt  34845  lpadmax  34864  lpadleft  34865  lpadright  34866  bnj529  34922  bnj548  35077  bnj570  35085  bnj852  35101  bnj929  35116  bnj1097  35161  bnj1118  35164  bnj1145  35173  funen1cnv  35269  fissorduni  35271  spthcycl  35349  acycgr0v  35368  derangen  35392  subfacp1lem2b  35401  subfacp1lem4  35403  subfacp1lem5  35404  derangfmla  35410  ptpconn  35453  mppspstlem  35791  wsuclem  36043  colinearex  36280  btwnconn1lem11  36317  btwnconn1lem12  36318  fwddifnp1  36385  nn0prpwlem  36542  regsfromregtr  36694  bj-snmoore  37370  bj-imdiridlem  37444  relowlpssretop  37623  fin2so  37862  matunitlindflem2  37872  ptrecube  37875  poimirlem8  37883  poimirlem13  37888  poimirlem15  37890  poimirlem24  37899  poimirlem25  37900  poimirlem26  37901  heicant  37910  mblfinlem2  37913  voliunnfl  37919  mbfresfi  37921  itg2addnclem  37926  itg2addnclem3  37928  itg2gt0cn  37930  ftc1cnnclem  37946  ftc1anclem5  37952  cover2  37970  indexdom  37989  sdclem1  37998  fdc  38000  equivbnd2  38047  heiborlem8  38073  heibor  38076  isdrngo2  38213  iscringd  38253  smprngopr  38307  prnc  38322  eqbrtr  38493  eqeltr  38495  islfld  39442  lkrshpor  39487  lfl1dim  39501  lfl1dim2N  39502  cmtcomlemN  39628  2lplnmN  39939  pmapjat1  40233  trlnid  40559  tendoex  41355  dia1dimid  41443  dibval2  41524  dihmeetlem2N  41679  dochlkr  41765  mapdcv  42040  hdmaplkr  42293  hdmapip0  42295  hlhillcs  42338  aks6d1c6lem4  42547  dvdsexpnn  42707  readvrec  42736  frlmvscadiccat  42880  psrmnd  42917  nacsfix  43073  3rexfrabdioph  43158  4rexfrabdioph  43159  6rexfrabdioph  43160  7rexfrabdioph  43161  eldioph4b  43172  pellexlem2  43191  pellexlem5  43194  jm2.26lem3  43362  numinfctb  43464  ordne0gt0  43622  omge1  43658  omlim2  43660  omord2lim  43661  omord2i  43662  tfsconcatfv  43702  tfsconcatb0  43705  oaun3lem1  43735  ntrclsfv1  44415  ntrneifv1  44439  ntrneifv2  44440  cvgdvgrat  44673  radcnvrat  44674  dvconstbi  44694  bccbc  44705  elpwgded  44924  elpwgdedVD  45276  sspwimpcf  45279  sspwimpcfVD  45280  sspwimpALT2  45287  ax6e2ndeqALT  45290  eliuniin  45462  eliuniin2  45483  qinioo  45899  dfxlim2v  46209  xlimliminflimsup  46224  cncfiooicclem1  46255  ibliooicc  46333  stoweidlem27  46389  stoweidlem28  46390  fourierdlem89  46557  fourierdlem91  46559  fourierdlem92  46560  smflimmpt  47172  odz2prm2pw  47927  perfectALTVlem2  48086  blen1b  48952  naryfvalelfv  48996  itscnhlc0yqe  49123  itsclquadb  49140  lubeldm2  49319  glbeldm2  49320  ipolub  49351  ipoglb  49354  fucofulem1  49673  functhinclem1  49807  thincciso  49816  prsthinc  49827  functermclem  49870  prstchom2ALT  49927  onetansqsecsq  50124  cotsqcscsq  50125  aacllem  50164