Theorem biimpar 482

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 411	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  bitr  816  exbiri  822  biadanid  834  bibiad  852  oplem1  1070  eqtr  2789  pm13.181  3046  opabss  5179  axprlem4OLD  5402  axprlem5OLD  5403  euotd  5497  brcogw  5855  somin1  6134  xpdifid  6166  xpdifcnvepel  6167  funfni  6642  fnssres  6659  fn0  6667  fnimadisj  6668  fnimaeq0  6669  foimacnv  6839  fvelimab  6954  dffv2  6977  fvopab3ig  6986  funcnvmpt  6992  dff3  7096  dffo4  7099  fpr2g  7210  ralima  7236  f1eqcocnv  7300  isomin  7336  f1ocnv2d  7664  fnexALT  7948  xp1st  8018  xp2nd  8019  frrlem3  8285  fpr2  8301  wfr3g  8316  wfr2  8324  iinon  8327  tfr3  8386  oawordri  8535  oaass  8546  omeulem1  8567  oeoa  8583  oeoe  8585  oeeulem  8587  elqsn0  8782  pwdom  9117  enfii  9170  phpeqd  9196  ominf  9224  findcard3  9243  marypha1lem  9393  wofib  9507  cantnff  9643  cantnfp1  9650  cantnf  9662  cnfcomlem  9668  ttrcltr  9685  frr3g  9728  r1sscl  9757  rankval3b  9798  infxpidm2  10001  numdom  10022  onssnum  10024  acni  10029  acni2  10030  dfac5  10112  djulepw  10176  infunsdom1  10195  infunsdom  10196  cofsmo  10253  cfsmolem  10254  fin1ai  10277  fin2i  10279  isf34lem1  10356  fin67  10379  itunisuc  10403  axdc3lem4  10437  zornn0g  10489  ttukeylem6  10498  brdom3  10512  tsken  10739  tskcard  10766  r1tskina  10767  intgru  10799  prlem934  11018  ltexprlem7  11027  supaddc  12182  mul2lt0rlt0  13120  xrmaxeq  13205  xrmineq  13206  xmulneg1  13295  ixxun  13388  difelfzle  13669  ssfzoulel  13789  elfznelfzo  13802  ico01fl0  13852  btwnzge0  13861  ltdifltdiv  13867  ioopnfsup  13897  icopnfsup  13898  modifeq2int  13969  suppssfz  14030  expmordi  14203  zzlesq  14242  faclbnd4lem4  14332  hasheni  14384  hashgt0  14424  hashge1  14425  hashprb  14433  hashpss  14446  lennncl  14571  wrdsymb0  14586  ccatsymb  14620  ccatlid  14624  ccatass  14626  ccatswrd  14706  swrdccat2  14707  ccatpfx  14738  swrdccatfn  14761  swrdccat  14772  revccat  14803  2cshw  14850  cnpart  15291  resqreu  15303  recval  15374  abs1m  15387  abslem2  15391  fzomaxdiflem  15394  sqreulem  15411  sqreu  15412  limsupgre  15532  rlimdiv  15697  fsumparts  15858  climcnds  15905  expcnv  15918  ntrivcvg  15951  mod2eq1n2dvds  16405  ndvdssub  16467  sadcaddlem  16515  rplpwr  16616  dvdssqlem  16624  algcvgblem  16635  eucalgcvga  16644  isprm2lem  16739  powm2modprm  16863  coprimeprodsq  16868  pythagtriplem11  16885  pythagtriplem13  16887  pcadd2  16950  4sqlem11  17015  vdwlem6  17046  vdwlem8  17048  vdwlem10  17050  ramval  17068  ramcl2  17076  ramlb  17079  ram0  17082  mreintcl  17647  mrcval  17666  mrccl  17667  mrcuni  17677  mrcun  17678  acsfiel  17710  rescabs  17890  funcres  17953  setcmon  18144  setcepi  18145  fullestrcsetc  18207  funcsetcestrclem8  18218  fullsetcestrc  18222  yonffthlem  18338  pleval2i  18390  pospo  18399  poslubdg  18468  acsdrsel  18599  acsdrscl  18602  acsficl  18603  psss  18636  chnind  18677  chnub  18678  chnccats1  18681  chnccat  18682  grpidd  18729  ismndd  18814  gsumsgrpccat  18899  gsumwmhm  18904  mulgaddcom  19164  subgmulg  19207  resghm  19302  conjnsg  19324  ghmqusker  19357  f1otrspeq  19517  pmtrval  19521  pmtrrn  19527  pmtrfinv  19531  pmtrprfval  19557  psgnunilem1  19563  psgnunilem5  19564  psgnunilem4  19567  psgneldm2i  19575  lsmelvalix  19711  pj1ghm  19773  efgredlemc  19815  frgp0  19830  qusabl  19935  cycsubgcyg  19971  gsumval3  19977  gsumcllem  19978  ablfac1c  20143  pgpfac1lem5  20151  submomnd  20202  isrngd  20251  isringd  20374  01eq0ring  20614  ornglmullt  20950  orngrmullt  20951  lspsneq0b  21112  lmodindp1  21113  lmhmf1o  21145  lmhmpreima  21147  reslmhm  21151  pwssplit3  21160  lspsncmp  21218  lspsneq  21224  prmidl2  21437  prmidl0  21447  qsidomlem1  21449  ssdifidlprm  21455  prmidlsubm  21456  znf1o  21670  dsmmlss  21863  frlmlbs  21916  frlmup1  21917  psrgrp  22075  mpfind  22235  psdmul  22298  ply1scleq  22434  mat1  22573  chfacfisf  22980  chfacfisfcpmat  22981  uniopn  23023  ntrval  23162  clsval  23163  neival  23228  neiptopreu  23259  lpval  23265  restdis  23304  lmbrf  23386  cnpnei  23390  1stcrest  23579  hauspwdom  23627  lfinpfin  23650  txcnpi  23734  ptrescn  23765  xkococnlem  23785  qtopeu  23842  kqreglem1  23867  ptuncnv  23933  filss  23979  fsubbas  23993  fbasrn  24010  cfinfil  24019  ufinffr  24055  elfm3  24076  rnelfmlem  24078  rnelfm  24079  flimclslem  24110  flfval  24116  isfcf  24160  cnextfvval  24191  cnextf  24192  cnextcn  24193  ustelimasn  24349  trust  24355  restutop  24363  ustuqtop2  24368  utop2nei  24376  ucncn  24410  trcfilu  24419  cnextucn  24428  met1stc  24647  metustexhalf  24682  cfilucfil  24685  psmetutop  24693  nmoix  24855  nmoeq0  24862  idnghm  24869  blcvx  24924  xrsxmet  24936  iccntr  24948  icccmp  24952  iihalf1  25059  iihalf2  25061  xrhmeo  25074  cnheibor  25083  ipcau2  25362  lmmbrf  25390  iscauf  25408  cmetcaulem  25416  bcthlem4  25455  cmetcusp  25482  rrxcph  25520  minveclem4  25560  evthicc2  25588  cniccbdd  25589  ovollb2  25617  ovolunlem1a  25624  ovolunlem1  25625  voliun  25682  icombl  25692  ioombl  25693  iccvolcl  25695  ioovolcl  25698  mbfss  25774  mbfposb  25781  itg2const2  25869  itg2splitlem  25876  itg2gt0  25888  iblss2  25934  itgioo  25944  dvaddf  26070  dvmulf  26071  dvcobr  26074  dvcof  26076  rolle  26118  dvlip  26121  c1lip1  26125  dvivthlem1  26136  lhop1lem  26141  dvfsumlem1  26154  ftc1lem4  26167  ftc1lem5  26168  ply1divmo  26262  coe1termlem  26384  plymulidp  26412  plydiveu  26428  taylplem1  26492  pserulm  26551  abelth  26570  abscxp2  26824  abscxpbnd  26884  logbgt0b  26924  ang180lem2  26941  ang180lem3  26942  isosctrlem1  26949  angpieqvd  26962  atandmtan  27051  birthdaylem3  27084  wilthlem2  27199  wilthimp  27202  isppw  27244  isppw2  27245  dvdsflsumcom  27318  chteq0  27339  perfectlem2  27360  dchrval  27364  dchrinvcl  27383  dchrptlem1  27394  bposlem3  27416  lgslem4  27430  lgsmod  27453  lgsdilem  27454  lgsdir2lem2  27456  lgsdir2  27460  lgsne0  27465  lgsmulsqcoprm  27473  lgseisenlem1  27505  2lgsoddprm  27546  2sqlem4  27551  chpo1ubb  27611  dchrisumn0  27651  pntrsumbnd2  27697  ostthlem1  27757  ostth3  27768  nosupbnd2lem1  27845  noinfbnd2lem1  27860  nocvxmin  27914  eqcuts2  27945  ltslpss  28067  madefi  28072  abslts  28408  eucliddivs  28535  peano5uzs  28563  z12bdaylem1  28629  elreno2  28654  idmot  28772  tgelrnln  28865  lnincplng  29024  plngmiropp  29034  lmimid  29061  lmiisolem  29063  hypcgrlem1  29066  brcgr  29191  colinearalglem4  29200  colinearalg  29201  axlowdimlem14  29246  axcontlem4  29258  cplgrop  29728  lfgriswlk  29977  pthdlem1  30056  crctcshwlkn0  30111  elwspths2on  30252  elwspths2onw  30253  clwlkclwwlklem2fv2  30288  frgrncvvdeqlem9  30599  nvss  30886  sspn  31029  nmoub3i  31066  nmblolbii  31092  blocnilem  31097  minvecolem4  31173  htthlem  31210  norm1  31542  norm1exi  31543  pjeq  31692  axpjpj  31713  normcan  31869  pjoi0  32010  nmopub2tALT  32202  nmfnleub2  32219  eighmorth  32257  nmbdoplbi  32317  nmcoplbi  32321  nmophmi  32324  nmbdfnlbi  32342  nmcfnlbi  32345  riesz3i  32355  cnlnadjlem7  32366  branmfn  32398  nmopleid  32432  hstle  32523  superpos  32647  cvexchlem  32661  foresf1o  32791  elabreximd  32797  prssad  32816  prssbd  32817  unidifsnne  32823  tpssad  32826  fresunsn  32911  f1o3d  32912  fmptco1f1o  32919  fgreu  32957  suppovss  32967  elsuppfnd  32968  fsupprnfi  32978  resf1o  33016  fpwrelmap  33019  argcj  33034  xrofsup  33053  eliccelico  33063  elicoelioo  33064  iocinif  33067  difioo  33068  hashne0  33095  elq2  33097  oexpled  33121  indf1ofs  33127  eliccioo  33191  cshf1o  33223  mgcmnt1d  33258  mgcmnt2d  33259  pwrssmgc  33261  mndlactf1o  33291  mndractf1o  33292  gsummpt2co  33309  gsumhashmul  33328  gsummulsubdishift1  33329  symgcom  33344  symgcom2  33345  odpmco  33347  pmtrcnel  33350  pmtridf1o  33355  cycpmco2lem6  33392  cycpmco2lem7  33393  cycpmco2  33394  cyc3co2  33401  cycpmconjv  33403  tocyccntz  33405  cyc3evpm  33411  cycpmconjslem2  33416  cycpmconjs  33417  fxpsubm  33433  fxpsubg  33434  fxpsubrg  33435  fxpsdrg  33436  archirngz  33450  unitnz  33499  elrgspnlem1  33503  elrgspnlem2  33504  elrgspnlem4  33506  elrgspnsubrun  33510  rloccring  33532  rlocf1  33535  rlocisunit  33537  domnpropd  33541  rrgsubm  33545  isdrng4  33559  sdrgdvcl  33563  sdrginvcl  33564  fracfld  33572  lindssn  33635  linds2eq  33638  dvdsrspss  33644  nsgqusf1olem1  33666  nsgqusf1olem3  33668  unitpidl1  33676  elrspunidl  33680  rhmimaidl  33684  drngidlhash  33686  mxidlirredi  33699  mxidlirred  33700  ssmxidl  33702  drng0mxidl  33703  opprmxidlabs  33714  qsdrngilem  33721  qsdrngi  33722  qsdrng  33724  drnglring  33727  dflring2  33728  dflringlem  33729  dflringlem3  33731  dflring4  33733  fldlring  33734  rsprprmprmidl  33757  rsprprmprmidlb  33758  rprmasso2  33761  rprmirredlem  33765  rprmirredb  33767  1arithidomlem2  33771  1arithufdlem4  33782  1arithufd  33783  ressply1evls1  33800  ply1asclunit  33809  ply1dg1rt  33815  ply1mulrtss  33817  ply1dg3rt0irred  33819  ply1degltlss  33831  ply1gsumz  33834  mplidomlem  33862  evlextv  33877  esplyfv1  33904  esplyind  33910  vietadeg1  33913  lsssra  33923  exsslsb  33932  lbslsat  33951  lindsunlem  33959  lindsun  33960  dimkerim  33962  fedgmullem1  33964  fedgmullem2  33965  fedgmul  33966  dimlssid  33967  lvecendof1f1o  33968  assalactf1o  33970  sdrgfldext  33985  fldsdrgfldext  33996  fldgenfldext  34003  evls1fldgencl  34005  fldextrspunlsp  34009  fldextrspunlem1  34010  fldextrspunfld  34011  irngss  34022  0ringirng  34024  irngnzply1  34026  extdgfialglem1  34027  irngnminplynz  34047  minplyelirng  34050  irredminply  34051  algextdeglem2  34053  algextdeglem4  34055  constrconj  34080  constrextdg2lem  34083  constrext2chnlem  34085  iconstr  34101  constrsdrg  34110  cos9thpiminplylem1  34117  cos9thpiminplylem2  34118  cos9thpiminplylem3  34119  cos9thpiminplylem5  34121  madjusmdetlem2  34163  qtophaus  34171  locfinreflem  34175  zarclssn  34208  zarmxt1  34215  zarcmplem  34216  rhmpreimacn  34220  unitdivcld  34236  tpr2rico  34247  ordtrestNEW  34256  lmxrge0  34287  elzrhunit  34312  qqhf  34321  gsumesum  34394  esumfsup  34405  esumcvg  34421  issgon  34458  sigainb  34471  insiga  34472  isrnmeas  34535  measvunilem  34547  volmeas  34566  ddeval1  34569  ddeval0  34570  imambfm  34597  omssubadd  34635  carsgclctunlem3  34655  eulerpartlemf  34705  eulerpartlemgvv  34711  probun  34754  dstfrvunirn  34810  signslema  34894  signstfvn  34901  signsvtn0  34902  signstfvneq0  34904  signstres  34907  signstfveq0a  34908  breprexplemc  34964  logdivsqrle  34982  hgt750lemg  34986  tgoldbachgtda  34993  tgoldbachgt  34995  lpadmax  35017  lpadleft  35018  lpadright  35019  bnj529  35075  bnj548  35230  bnj570  35238  bnj852  35254  bnj929  35269  bnj1097  35314  bnj1118  35317  bnj1145  35326  funen1cnv  35420  fissorduni  35423  vonf1oonfo  35498  spthcycl  35520  acycgr0v  35539  derangen  35563  subfacp1lem2b  35572  subfacp1lem4  35574  subfacp1lem5  35575  derangfmla  35581  ptpconn  35624  mppspstlem  35962  wsuclem  36214  colinearex  36451  btwnconn1lem11  36488  btwnconn1lem12  36489  fwddifnp1  36556  nn0prpwlem  36722  ttctr  36893  dfttc2g  36906  regsfromregtco  36938  bj-snmoore  37643  bj-imdiridlem  37717  relowlpssretop  37898  fin2so  38146  matunitlindflem2  38156  ptrecube  38159  poimirlem8  38167  poimirlem13  38172  poimirlem15  38174  poimirlem24  38183  poimirlem25  38184  poimirlem26  38185  heicant  38194  mblfinlem2  38197  voliunnfl  38203  mbfresfi  38205  itg2addnclem  38210  itg2addnclem3  38212  itg2gt0cn  38214  ftc1cnnclem  38230  ftc1anclem5  38236  cover2  38254  indexdom  38273  sdclem1  38282  fdc  38284  equivbnd2  38331  heiborlem8  38357  heibor  38360  isdrngo2  38497  iscringd  38537  smprngopr  38591  prnc  38606  eqbrtr  38777  eqeltr  38779  islfld  39726  lkrshpor  39771  lfl1dim  39785  lfl1dim2N  39786  cmtcomlemN  39912  2lplnmN  40223  pmapjat1  40517  trlnid  40843  tendoex  41639  dia1dimid  41727  dibval2  41808  dihmeetlem2N  41963  dochlkr  42049  mapdcv  42324  hdmaplkr  42577  hdmapip0  42579  hlhillcs  42622  aks6d1c6lem4  42830  dvdsexpnn  42984  readvrec  43013  frlmvscadiccat  43170  psrmnd  43203  nacsfix  43335  3rexfrabdioph  43416  4rexfrabdioph  43417  6rexfrabdioph  43418  7rexfrabdioph  43419  eldioph4b  43430  pellexlem2  43449  pellexlem5  43452  jm2.26lem3  43620  numinfctb  43722  ordne0gt0  43880  omge1  43916  omlim2  43918  omord2lim  43919  omord2i  43920  tfsconcatfv  43960  tfsconcatb0  43963  oaun3lem1  43993  ntrclsfv1  44673  ntrneifv1  44697  ntrneifv2  44698  cvgdvgrat  44915  radcnvrat  44916  dvconstbi  44936  bccbc  44947  elpwgded  45165  elpwgdedVD  45517  sspwimpcf  45520  sspwimpcfVD  45521  sspwimpALT2  45528  ax6e2ndeqALT  45531  eliuniin  45709  eliuniin2  45730  qinioo  46143  dfxlim2v  46453  xlimliminflimsup  46468  cncfiooicclem1  46499  ibliooicc  46577  stoweidlem27  46633  stoweidlem28  46634  fourierdlem89  46801  fourierdlem91  46803  fourierdlem92  46804  smflimmpt  47416  odz2prm2pw  48204  perfectALTVlem2  48376  blen1b  49253  naryfvalelfv  49297  itscnhlc0yqe  49424  itsclquadb  49441  lubeldm2  49619  glbeldm2  49620  ipolub  49651  ipoglb  49654  fucofulem1  49973  functhinclem1  50107  thincciso  50116  prsthinc  50127  functermclem  50170  prstchom2ALT  50227  onetansqsecsq  50424  cotsqcscsq  50425  aacllem  50475