Theorem biimpar 483

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 251	. 2 ⊢ (𝜑 → (𝜒 → 𝜓))
3	2	imp 412	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  bitr  817  exbiri  823  biadanid  835  bibiad  853  oplem1  1072  eqtr  2783  pm13.181  3040  opabss  5171  euotd  5489  brcogw  5850  somin1  6132  xpdifid  6164  xpdifcnvepel  6165  funfni  6653  fnssres  6670  fn0  6678  fnimadisj  6679  fnimaeq0  6680  foimacnv  6850  fvelimab  6965  dffv2  6988  fvopab3ig  6997  funcnvmpt  7003  dff3  7108  dffo4  7111  fpr2g  7224  ralima  7250  f1eqcocnv  7316  isomin  7352  f1ocnv2d  7681  fnexALT  7970  xp1st  8040  xp2nd  8041  frrlem3  8317  fpr2  8333  wfr3g  8348  wfr2  8356  iinon  8359  tfr3  8418  oawordri  8569  oaass  8580  omeulem1  8601  oeoa  8617  oeoe  8619  oeeulem  8621  elqsn0  8816  funen1cnv  9067  pwdom  9159  enfii  9212  phpeqd  9238  ominf  9266  findcard3  9285  fissorduni  9293  marypha1lem  9435  wofib  9549  cantnff  9685  cantnfp1  9692  cantnf  9704  cnfcomlem  9710  ttrcltr  9727  frr3g  9770  r1sscl  9802  rankval3b  9846  infxpidm2  10106  numdom  10127  onssnum  10129  acni  10134  acni2  10135  dfac5  10217  djulepw  10281  infunsdom1  10300  infunsdom  10301  cofsmo  10357  cfsmolem  10358  fin1ai  10381  fin2i  10383  isf34lem1  10460  fin67  10483  itunisuc  10507  axdc3lem4  10541  zornn0g  10593  ttukeylem6  10602  brdom3  10617  tsken  10849  tskcard  10876  r1tskina  10877  intgru  10909  prlem934  11128  ltexprlem7  11137  supaddc  12294  mul2lt0rlt0  13234  xrmaxeq  13319  xrmineq  13320  xmulneg1  13409  ixxun  13502  difelfzle  13785  ssfzoulel  13905  elfznelfzo  13918  ico01fl0  13969  btwnzge0  13978  ltdifltdiv  13984  ioopnfsup  14014  icopnfsup  14015  modifeq2int  14086  suppssfz  14147  expmordi  14320  zzlesq  14360  faclbnd4lem4  14450  hasheni  14502  hashgt0  14542  hashge1  14543  hashprb  14551  hashpss  14564  lennncl  14689  wrdsymb0  14704  ccatsymb  14738  ccatlid  14742  ccatass  14744  ccatswrd  14829  swrdccat2  14830  ccatpfx  14861  swrdccatfn  14884  swrdccat  14895  revccat  14926  2cshw  14975  cnpart  15419  resqreu  15431  recval  15502  abs1m  15515  abslem2  15519  fzomaxdiflem  15522  sqreulem  15539  sqreu  15540  limsupgre  15660  rlimdiv  15825  fsumparts  15985  climcnds  16032  expcnv  16045  ntrivcvg  16078  mod2eq1n2dvds  16529  ndvdssub  16591  sadcaddlem  16639  rplpwr  16744  dvdsexpnn  16752  algcvgblem  16764  eucalgcvga  16773  isprm2lem  16868  powm2modprm  16993  coprimeprodsq  16998  pythagtriplem11  17015  pythagtriplem13  17017  pcadd2  17080  4sqlem11  17145  vdwlem6  17176  vdwlem8  17178  vdwlem10  17180  ramval  17198  ramcl2  17206  ramlb  17209  ram0  17212  mreintcl  17777  mrcval  17796  mrccl  17797  mrcuni  17807  mrcun  17808  acsfiel  17840  rescabs  18020  funcres  18083  setcmon  18274  setcepi  18275  fullestrcsetc  18337  funcsetcestrclem8  18348  fullsetcestrc  18352  yonffthlem  18468  pleval2i  18520  pospo  18529  poslubdg  18598  acsdrsel  18729  acsdrscl  18732  acsficl  18733  psss  18766  chnind  18807  chnub  18808  chnccats1  18811  chnccat  18812  grpidd  18864  ismndd  18958  gsumsgrpccat  19048  gsumwmhm  19053  mulgaddcom  19320  subgmulg  19363  resghm  19458  conjnsg  19480  ghmqusker  19513  f1otrspeq  19673  pmtrval  19677  pmtrrn  19683  pmtrfinv  19687  pmtrprfval  19713  psgnunilem1  19719  psgnunilem5  19720  psgnunilem4  19723  psgneldm2i  19731  lsmelvalix  19867  pj1ghm  19929  efgredlemc  19971  frgp0  19986  qusabl  20091  cycsubgcyg  20127  gsumval3  20133  gsumcllem  20134  ablfac1c  20299  pgpfac1lem5  20307  submomnd  20358  isrngd  20407  isringd  20534  01eq0ring  20793  isdrng4  21004  ornglmullt  21138  orngrmullt  21139  lspsneq0b  21300  lmodindp1  21301  lmhmf1o  21333  lmhmpreima  21335  reslmhm  21339  pwssplit3  21348  lspsncmp  21406  lspsneq  21412  prmidl2  21634  prmidl0  21646  qsidomlem1  21648  ssdifidlprm  21654  prmidlsubm  21655  znf1o  21869  dsmmlss  22062  frlmlbs  22115  frlmup1  22116  psrgrp  22276  mpfind  22436  psdmul  22499  ply1scleq  22635  mat1  22774  matunitlindflem2  23007  chfacfisf  23184  chfacfisfcpmat  23185  uniopn  23227  ntrval  23366  clsval  23367  neival  23432  neiptopreu  23463  lpval  23469  restdis  23508  lmbrf  23590  cnpnei  23594  1stcrest  23783  hauspwdom  23832  lfinpfin  23855  txcnpi  23939  ptrescn  23970  xkococnlem  23990  qtopeu  24047  kqreglem1  24072  ptuncnv  24138  filss  24184  fsubbas  24198  fbasrn  24215  cfinfil  24224  ufinffr  24260  elfm3  24281  rnelfmlem  24283  rnelfm  24284  flimclslem  24315  flfval  24321  isfcf  24365  cnextfvval  24396  cnextf  24397  cnextcn  24398  ustelimasn  24554  trust  24560  restutop  24568  ustuqtop2  24573  utop2nei  24581  ucncn  24615  trcfilu  24624  cnextucn  24633  met1stc  24852  metustexhalf  24887  cfilucfil  24890  psmetutop  24898  nmoix  25060  nmoeq0  25067  idnghm  25074  blcvx  25129  xrsxmet  25141  iccntr  25153  icccmp  25157  iihalf1  25264  iihalf2  25266  xrhmeo  25279  cnheibor  25288  ipcau2  25567  lmmbrf  25595  iscauf  25613  cmetcaulem  25621  bcthlem4  25660  cmetcusp  25687  rrxcph  25725  minveclem4  25765  evthicc2  25793  cniccbdd  25794  ovollb2  25822  ovolunlem1a  25829  ovolunlem1  25830  voliun  25887  icombl  25897  ioombl  25898  iccvolcl  25900  ioovolcl  25903  mbfss  25979  mbfposb  25986  itg2const2  26074  itg2splitlem  26081  itg2gt0  26093  iblss2  26138  itgioo  26148  dvaddf  26274  dvmulf  26275  dvcobr  26278  dvcof  26280  rolle  26322  dvlip  26325  c1lip1  26329  dvivthlem1  26340  lhop1lem  26345  dvfsumlem1  26358  ftc1lem4  26371  ftc1lem5  26372  ply1divmo  26466  coe1termlem  26589  plymulidp  26615  plydiveu  26631  taylplem1  26702  pserulm  26761  abelth  26780  abscxp2  27033  abscxpbnd  27093  logbgt0b  27133  ang180lem2  27150  ang180lem3  27151  isosctrlem1  27158  angpieqvd  27171  atandmtan  27260  birthdaylem3  27293  wilthlem2  27408  wilthimp  27411  isppw  27453  isppw2  27454  dvdsflsumcom  27527  chteq0  27548  perfectlem2  27569  dchrval  27573  dchrinvcl  27592  dchrptlem1  27603  bposlem3  27625  lgslem4  27639  lgsmod  27662  lgsdilem  27663  lgsdir2lem2  27665  lgsdir2  27669  lgsne0  27674  lgsmulsqcoprm  27682  lgseisenlem1  27714  2lgsoddprm  27755  2sqlem4  27760  chpo1ubb  27820  dchrisumn0  27860  pntrsumbnd2  27906  ostthlem1  27966  ostth3  27977  nosupbnd2lem1  28084  noinfbnd2lem1  28099  nocvxmin  28153  eqcuts2  28184  ltslpss  28306  madefi  28311  abslts  28647  eucliddivs  28774  peano5uzs  28802  z12bdaylem1  28868  elreno2  28893  idmot  29012  tgelrnln  29110  lnincplng  29274  plngmiropp  29284  lmimid  29311  lmiisolem  29313  hypcgrlem1  29317  brcgr  29490  colinearalglem4  29499  colinearalg  29500  axlowdimlem14  29545  axcontlem4  29557  cplgrop  30030  lfgriswlk  30283  pthdlem1  30364  spthcycl  30404  crctcshwlkn0  30422  elwspths2on  30563  elwspths2onw  30564  clwlkclwwlklem2fv2  30599  frgrncvvdeqlem9  30920  nvss  31207  sspn  31350  nmoub3i  31387  nmblolbii  31413  blocnilem  31418  minvecolem4  31494  htthlem  31531  norm1  31863  norm1exi  31864  pjeq  32013  axpjpj  32034  normcan  32190  pjoi0  32331  nmopub2tALT  32523  nmfnleub2  32540  eighmorth  32578  nmbdoplbi  32638  nmcoplbi  32642  nmophmi  32645  nmbdfnlbi  32663  nmcfnlbi  32666  riesz3i  32676  cnlnadjlem7  32687  branmfn  32719  nmopleid  32753  hstle  32844  superpos  32968  cvexchlem  32982  foresf1o  33154  elabreximd  33160  prssad  33179  prssbd  33180  unidifsnne  33186  tpssad  33189  fresunsn  33273  f1o3d  33274  fmptco1f1o  33281  fgreu  33319  suppovss  33328  elsuppfnd  33329  fsupprnfi  33339  resf1o  33375  fpwrelmap  33378  argcj  33393  xrofsup  33412  eliccelico  33422  elicoelioo  33423  iocinif  33426  difioo  33427  hashne0  33454  elq2  33456  oexpled  33480  indf1ofs  33486  eliccioo  33550  cshf1o  33576  mgcmnt1d  33611  mgcmnt2d  33612  pwrssmgc  33614  mndlactf1o  33644  mndractf1o  33645  gsummpt2co  33662  gsumhashmul  33681  gsummulsubdishift1  33682  symgcom  33697  symgcom2  33698  odpmco  33700  pmtrcnel  33703  pmtridf1o  33708  cycpmco2lem6  33745  cycpmco2lem7  33746  cycpmco2  33747  cyc3co2  33754  cycpmconjv  33756  tocyccntz  33758  cyc3evpm  33764  cycpmconjslem2  33769  cycpmconjs  33770  fxpsubm  33786  fxpsubg  33787  fxpsubrg  33788  fxpsdrg  33789  archirngz  33803  unitnz  33852  elrgspnlem1  33856  elrgspnlem2  33857  elrgspnlem4  33859  elrgspnsubrun  33863  rloccring  33885  rlocf1  33888  rlocisunit  33890  domnpropd  33894  rrgsubm  33898  sdrgdvcl  33914  sdrginvcl  33915  fracfld  33923  lindssn  33986  linds2eq  33989  dvdsrspss  33995  nsgqusf1olem1  34017  nsgqusf1olem3  34019  unitpidl1  34027  elrspunidl  34031  rhmimaidl  34035  drngidlhash  34036  mxidlirredi  34049  mxidlirred  34050  ssmxidl  34052  drng0mxidl  34053  opprmxidlabs  34064  qsdrngilem  34071  qsdrngi  34072  qsdrng  34074  drnglring  34077  dflring2  34078  dflringlem  34079  dflringlem3  34081  dflring4  34083  fldlring  34084  rsprprmprmidl  34107  rsprprmprmidlb  34108  rprmasso2  34111  rprmirredlem  34115  rprmirredb  34117  1arithidomlem2  34121  1arithufdlem4  34132  1arithufd  34133  ressply1evls1  34150  ply1asclunit  34159  ply1dg1rt  34165  ply1mulrtss  34167  ply1dg3rt0irred  34169  ply1degltlss  34181  ply1gsumz  34184  mplidomlem  34212  evlextv  34227  esplyfv1  34254  esplyind  34260  vietadeg1  34263  lsssra  34273  exsslsb  34282  lbslsat  34301  lindsunlem  34309  lindsun  34310  dimkerim  34312  fedgmullem1  34314  fedgmullem2  34315  fedgmul  34316  dimlssid  34317  lvecendof1f1o  34318  assalactf1o  34320  sdrgfldext  34335  fldsdrgfldext  34346  fldgenfldext  34353  evls1fldgencl  34355  fldextrspunlsp  34359  fldextrspunlem1  34360  fldextrspunfld  34361  irngss  34372  0ringirng  34374  irngnzply1  34376  extdgfialglem1  34377  irngnminplynz  34397  minplyelirng  34400  irredminply  34401  algextdeglem2  34403  algextdeglem4  34405  constrconj  34430  constrextdg2lem  34433  constrext2chnlem  34435  iconstr  34451  constrsdrg  34460  cos9thpiminplylem1  34467  cos9thpiminplylem2  34468  cos9thpiminplylem3  34469  cos9thpiminplylem5  34471  madjusmdetlem2  34513  qtophaus  34521  locfinreflem  34525  zarclssn  34558  zarmxt1  34565  zarcmplem  34566  rhmpreimacn  34570  unitdivcld  34586  tpr2rico  34597  ordtrestNEW  34606  lmxrge0  34637  elzrhunit  34662  qqhf  34671  gsumesum  34744  esumfsup  34755  esumcvg  34771  issgon  34808  sigainb  34822  insiga  34823  isrnmeas  34886  measvunilem  34898  volmeas  34917  ddeval1  34920  ddeval0  34921  imambfm  34947  omssubadd  34985  carsgclctunlem3  35005  eulerpartlemf  35055  eulerpartlemgvv  35061  probun  35104  dstfrvunirn  35160  signslema  35244  signstfvn  35251  signsvtn0  35252  signstfvneq0  35254  signstres  35257  signstfveq0a  35258  breprexplemc  35314  logdivsqrle  35332  hgt750lemg  35336  tgoldbachgtda  35343  tgoldbachgt  35345  lpadmax  35367  lpadleft  35368  lpadright  35369  bnj529  35425  bnj548  35580  bnj570  35588  bnj852  35604  bnj929  35619  bnj1097  35664  bnj1118  35667  bnj1145  35676  ecscottd  35823  acwer1prclem  35830  vonf1oonfo  36003  acycgr0v  36024  derangen  36058  subfacp1lem2b  36067  subfacp1lem4  36069  subfacp1lem5  36070  derangfmla  36076  ptpconn  36119  mppspstlem  36457  wsuclem  36714  colinearex  36952  btwnconn1lem11  36989  btwnconn1lem12  36990  fwddifnp1  37057  nn0prpwlem  37237  ttctr  37408  dfttc2g  37421  regsfromregtco  37453  bj-snmoore  38173  bj-imdiridlem  38246  relowlpssretop  38427  fin2so  38670  ptrecube  38678  poimirlem8  38686  poimirlem13  38691  poimirlem15  38693  poimirlem24  38702  poimirlem25  38703  poimirlem26  38704  heicant  38713  mblfinlem2  38716  voliunnfl  38722  mbfresfi  38724  itg2addnclem  38729  itg2addnclem3  38731  itg2gt0cn  38733  ftc1cnnclem  38749  ftc1anclem5  38755  cover2  38789  indexdom  38808  sdclem1  38817  fdc  38819  equivbnd2  38866  heiborlem8  38892  heibor  38895  isdrngo2  39032  iscringd  39072  smprngopr  39126  prnc  39141  eqbrtr  39310  eqeltr  39312  islfld  40259  lkrshpor  40304  lfl1dim  40318  lfl1dim2N  40319  cmtcomlemN  40445  2lplnmN  40756  pmapjat1  41050  trlnid  41376  tendoex  42172  dia1dimid  42260  dibval2  42341  dihmeetlem2N  42496  dochlkr  42582  mapdcv  42857  hdmaplkr  43110  hdmapip0  43112  hlhillcs  43155  aks6d1c6lem4  43363  readvrec  43553  frlmvscadiccat  43713  psrmnd  43747  nacsfix  43863  3rexfrabdioph  43944  4rexfrabdioph  43945  6rexfrabdioph  43946  7rexfrabdioph  43947  eldioph4b  43958  pellexlem2  43977  pellexlem5  43980  jm2.26lem3  44148  numinfctb  44245  ordne0gt0  44403  omge1  44439  omlim2  44441  omord2lim  44442  omord2i  44443  tfsconcatfv  44483  tfsconcatb0  44486  oaun3lem1  44516  ntrclsfv1  45195  ntrneifv1  45219  ntrneifv2  45220  cvgdvgrat  45437  radcnvrat  45438  dvconstbi  45458  bccbc  45469  elpwgded  45686  elpwgdedVD  46038  sspwimpcf  46041  sspwimpcfVD  46042  sspwimpALT2  46049  ax6e2ndeqALT  46052  eliuniin  46253  eliuniin2  46274  qinioo  46686  dfxlim2v  46996  xlimliminflimsup  47011  cncfiooicclem1  47042  ibliooicc  47120  stoweidlem27  47176  stoweidlem28  47177  fourierdlem89  47344  fourierdlem91  47346  fourierdlem92  47347  smflimmpt  47959  tmachlem-agreesn  48096  odz2prm2pw  48787  perfectALTVlem2  48959  blen1b  49839  naryfvalelfv  49883  itscnhlc0yqe  50010  itsclquadb  50027  lubeldm2  50209  glbeldm2  50210  ipolub  50241  ipoglb  50244  fucofulem1  50571  functhinclem1  50718  thincciso  50727  prsthinc  50738  functermclem  50781  prstchom2ALT  50841  onetansqsecsq  51068  cotsqcscsq  51069  aacllem  51153