Theorem biimpar 481

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  bitr  814  exbiri  820  biadanid  832  bibiad  850  oplem1  1068  eqtr  2782  pm13.181  3039  opabss  5164  axprlem4OLD  5387  axprlem5OLD  5388  euotd  5482  brcogw  5840  somin1  6120  xpdifid  6153  xpdifcnvepel  6154  funfni  6627  fnssres  6644  fn0  6652  fnimadisj  6653  fnimaeq0  6654  foimacnv  6824  fvelimab  6939  dffv2  6962  fvopab3ig  6971  funcnvmpt  6977  dff3  7081  dffo4  7084  fpr2g  7195  ralima  7221  f1eqcocnv  7285  isomin  7321  f1ocnv2d  7649  fnexALT  7932  xp1st  8002  xp2nd  8003  frrlem3  8269  fpr2  8285  wfr3g  8300  wfr2  8308  iinon  8311  tfr3  8370  oawordri  8519  oaass  8530  omeulem1  8551  oeoa  8567  oeoe  8569  oeeulem  8571  elqsn0  8766  pwdom  9101  enfii  9154  phpeqd  9180  ominf  9208  findcard3  9227  marypha1lem  9379  wofib  9493  cantnff  9629  cantnfp1  9636  cantnf  9648  cnfcomlem  9654  ttrcltr  9671  frr3g  9714  r1sscl  9743  rankval3b  9784  infxpidm2  9973  numdom  9994  onssnum  9996  acni  10001  acni2  10002  dfac5  10085  djulepw  10149  infunsdom1  10168  infunsdom  10169  cofsmo  10226  cfsmolem  10227  fin1ai  10250  fin2i  10252  isf34lem1  10329  fin67  10352  itunisuc  10376  axdc3lem4  10410  zornn0g  10462  ttukeylem6  10471  brdom3  10485  tsken  10712  tskcard  10739  r1tskina  10740  intgru  10772  prlem934  10991  ltexprlem7  11000  supaddc  12159  mul2lt0rlt0  13097  xrmaxeq  13182  xrmineq  13183  xmulneg1  13272  ixxun  13365  difelfzle  13646  ssfzoulel  13766  elfznelfzo  13779  ico01fl0  13829  btwnzge0  13838  ltdifltdiv  13844  ioopnfsup  13874  icopnfsup  13875  modifeq2int  13946  suppssfz  14007  expmordi  14180  zzlesq  14219  faclbnd4lem4  14309  hasheni  14361  hashgt0  14401  hashge1  14402  hashprb  14410  lennncl  14547  wrdsymb0  14562  ccatsymb  14596  ccatlid  14600  ccatass  14602  ccatswrd  14682  swrdccat2  14683  ccatpfx  14714  swrdccatfn  14737  swrdccat  14748  revccat  14779  2cshw  14826  cnpart  15267  resqreu  15279  recval  15350  abs1m  15363  abslem2  15367  fzomaxdiflem  15370  sqreulem  15387  sqreu  15388  limsupgre  15508  rlimdiv  15673  fsumparts  15834  climcnds  15881  expcnv  15894  ntrivcvg  15927  mod2eq1n2dvds  16381  ndvdssub  16443  sadcaddlem  16491  rplpwr  16592  dvdssqlem  16600  algcvgblem  16611  eucalgcvga  16620  isprm2lem  16715  powm2modprm  16839  coprimeprodsq  16844  pythagtriplem11  16861  pythagtriplem13  16863  pcadd2  16926  4sqlem11  16991  vdwlem6  17022  vdwlem8  17024  vdwlem10  17026  ramval  17044  ramcl2  17052  ramlb  17055  ram0  17058  mreintcl  17623  mrcval  17642  mrccl  17643  mrcuni  17653  mrcun  17654  acsfiel  17686  rescabs  17866  funcres  17929  setcmon  18120  setcepi  18121  fullestrcsetc  18183  funcsetcestrclem8  18194  fullsetcestrc  18198  yonffthlem  18314  pleval2i  18366  pospo  18375  poslubdg  18444  acsdrsel  18575  acsdrscl  18578  acsficl  18579  psss  18612  chnind  18653  chnub  18654  chnccats1  18657  chnccat  18658  grpidd  18705  ismndd  18790  gsumsgrpccat  18874  gsumwmhm  18879  mulgaddcom  19140  subgmulg  19182  resghm  19272  conjnsg  19294  ghmqusker  19327  f1otrspeq  19487  pmtrval  19491  pmtrrn  19497  pmtrfinv  19501  pmtrprfval  19527  psgnunilem1  19533  psgnunilem5  19534  psgnunilem4  19537  psgneldm2i  19545  lsmelvalix  19681  pj1ghm  19743  efgredlemc  19785  frgp0  19800  qusabl  19905  cycsubgcyg  19941  gsumval3  19947  gsumcllem  19948  ablfac1c  20113  pgpfac1lem5  20121  submomnd  20172  isrngd  20219  isringd  20341  01eq0ring  20580  ornglmullt  20918  orngrmullt  20919  lspsneq0b  21080  lmodindp1  21081  lmhmf1o  21113  lmhmpreima  21115  reslmhm  21119  pwssplit3  21128  lspsncmp  21186  lspsneq  21192  znf1o  21603  dsmmlss  21796  frlmlbs  21849  frlmup1  21850  psrgrp  22008  mpfind  22168  psdmul  22231  ply1scleq  22368  mat1  22507  chfacfisf  22914  chfacfisfcpmat  22915  uniopn  22957  ntrval  23096  clsval  23097  neival  23162  neiptopreu  23193  lpval  23199  restdis  23238  lmbrf  23320  cnpnei  23324  1stcrest  23513  hauspwdom  23561  lfinpfin  23584  txcnpi  23668  ptrescn  23699  xkococnlem  23719  qtopeu  23776  kqreglem1  23801  ptuncnv  23867  filss  23913  fsubbas  23927  fbasrn  23944  cfinfil  23953  ufinffr  23989  elfm3  24010  rnelfmlem  24012  rnelfm  24013  flimclslem  24044  flfval  24050  isfcf  24094  cnextfvval  24125  cnextf  24126  cnextcn  24127  ustelimasn  24283  trust  24289  restutop  24297  ustuqtop2  24302  utop2nei  24310  ucncn  24344  trcfilu  24353  cnextucn  24362  met1stc  24581  metustexhalf  24616  cfilucfil  24619  psmetutop  24627  nmoix  24789  nmoeq0  24796  idnghm  24803  blcvx  24858  xrsxmet  24870  iccntr  24882  icccmp  24886  iihalf1  24993  iihalf2  24995  xrhmeo  25008  cnheibor  25017  ipcau2  25296  lmmbrf  25324  iscauf  25342  cmetcaulem  25350  bcthlem4  25389  cmetcusp  25416  rrxcph  25454  minveclem4  25494  evthicc2  25522  cniccbdd  25523  ovollb2  25551  ovolunlem1a  25558  ovolunlem1  25559  voliun  25616  icombl  25626  ioombl  25627  iccvolcl  25629  ioovolcl  25632  mbfss  25708  mbfposb  25715  itg2const2  25803  itg2splitlem  25810  itg2gt0  25822  iblss2  25868  itgioo  25878  dvaddf  26004  dvmulf  26005  dvcobr  26008  dvcof  26010  rolle  26052  dvlip  26055  c1lip1  26059  dvivthlem1  26070  lhop1lem  26075  dvfsumlem1  26088  ftc1lem4  26101  ftc1lem5  26102  ply1divmo  26196  coe1termlem  26318  plymulidp  26346  plydiveu  26362  taylplem1  26426  pserulm  26485  abelth  26504  abscxp2  26758  abscxpbnd  26818  logbgt0b  26858  ang180lem2  26875  ang180lem3  26876  isosctrlem1  26883  angpieqvd  26896  atandmtan  26985  birthdaylem3  27018  wilthlem2  27133  wilthimp  27136  isppw  27178  isppw2  27179  dvdsflsumcom  27252  chteq0  27273  perfectlem2  27294  dchrval  27298  dchrinvcl  27317  dchrptlem1  27328  bposlem3  27350  lgslem4  27364  lgsmod  27387  lgsdilem  27388  lgsdir2lem2  27390  lgsdir2  27394  lgsne0  27399  lgsmulsqcoprm  27407  lgseisenlem1  27439  2lgsoddprm  27480  2sqlem4  27485  chpo1ubb  27545  dchrisumn0  27585  pntrsumbnd2  27631  ostthlem1  27691  ostth3  27702  nosupbnd2lem1  27779  noinfbnd2lem1  27794  nocvxmin  27848  eqcuts2  27879  ltslpss  28001  madefi  28006  abslts  28342  eucliddivs  28469  peano5uzs  28497  z12bdaylem1  28563  elreno2  28588  idmot  28706  tgelrnln  28799  lmimid  28967  lmiisolem  28969  hypcgrlem1  28972  lnincplng  28991  brcgr  29101  colinearalglem4  29110  colinearalg  29111  axlowdimlem14  29156  axcontlem4  29168  cplgrop  29638  lfgriswlk  29887  pthdlem1  29966  crctcshwlkn0  30021  elwspths2on  30162  elwspths2onw  30163  clwlkclwwlklem2fv2  30198  frgrncvvdeqlem9  30509  nvss  30796  sspn  30939  nmoub3i  30976  nmblolbii  31002  blocnilem  31007  minvecolem4  31083  htthlem  31120  norm1  31452  norm1exi  31453  pjeq  31602  axpjpj  31623  normcan  31779  pjoi0  31920  nmopub2tALT  32112  nmfnleub2  32129  eighmorth  32167  nmbdoplbi  32227  nmcoplbi  32231  nmophmi  32234  nmbdfnlbi  32252  nmcfnlbi  32255  riesz3i  32265  cnlnadjlem7  32276  branmfn  32308  nmopleid  32342  hstle  32433  superpos  32557  cvexchlem  32571  foresf1o  32703  elabreximd  32709  prssad  32728  prssbd  32729  unidifsnne  32735  tpssad  32738  fresunsn  32827  f1o3d  32828  fmptco1f1o  32835  fgreu  32873  suppovss  32883  elsuppfnd  32884  fsupprnfi  32894  resf1o  32932  fpwrelmap  32935  argcj  32950  xrofsup  32969  eliccelico  32979  elicoelioo  32980  iocinif  32983  difioo  32984  hashpss  33011  hashne0  33012  elq2  33014  oexpled  33038  indf1ofs  33044  eliccioo  33108  cshf1o  33140  mgcmnt1d  33175  mgcmnt2d  33176  pwrssmgc  33178  mndlactf1o  33208  mndractf1o  33209  gsummpt2co  33228  gsumhashmul  33247  gsummulsubdishift1  33248  symgcom  33263  symgcom2  33264  odpmco  33266  pmtrcnel  33269  pmtridf1o  33274  cycpmco2lem6  33311  cycpmco2lem7  33312  cycpmco2  33313  cyc3co2  33320  cycpmconjv  33322  tocyccntz  33324  cyc3evpm  33330  cycpmconjslem2  33335  cycpmconjs  33336  fxpsubm  33352  fxpsubg  33353  fxpsubrg  33354  fxpsdrg  33355  archirngz  33369  unitnz  33419  elrgspnlem1  33423  elrgspnlem2  33424  elrgspnlem4  33426  elrgspnsubrun  33430  rloccring  33452  rlocf1  33455  rlocisunit  33457  domnpropd  33461  rrgsubm  33468  isdrng4  33482  sdrgdvcl  33486  sdrginvcl  33487  fracfld  33495  lindssn  33564  linds2eq  33567  dvdsrspss  33573  nsgqusf1olem1  33599  nsgqusf1olem3  33601  unitpidl1  33610  elrspunidl  33614  rhmimaidl  33618  drngidlhash  33620  prmidl2  33627  prmidl0  33637  qsidomlem1  33639  ssdifidlprm  33645  prmidlsubm  33646  mxidlirredi  33659  mxidlirred  33660  ssmxidl  33662  drng0mxidl  33664  opprmxidlabs  33675  qsdrngilem  33682  qsdrngi  33683  qsdrng  33685  drnglring  33688  dflring2  33689  dflringlem  33690  dflringlem3  33692  dflring4  33694  fldlring  33695  rsprprmprmidl  33718  rsprprmprmidlb  33719  rprmasso2  33722  rprmirredlem  33726  rprmirredb  33728  1arithidomlem2  33732  1arithufdlem4  33743  1arithufd  33744  ressply1evls1  33761  ply1asclunit  33770  ply1dg1rt  33776  ply1mulrtss  33778  ply1dg3rt0irred  33780  ply1degltlss  33792  ply1gsumz  33795  mplidomlem  33824  evlextv  33839  esplyfv1  33866  esplyind  33872  vietadeg1  33875  lsssra  33885  exsslsb  33894  lbslsat  33913  lindsunlem  33921  lindsun  33922  dimkerim  33924  fedgmullem1  33926  fedgmullem2  33927  fedgmul  33928  dimlssid  33929  lvecendof1f1o  33930  assalactf1o  33932  sdrgfldext  33947  fldsdrgfldext  33958  fldgenfldext  33965  evls1fldgencl  33967  fldextrspunlsp  33971  fldextrspunlem1  33972  fldextrspunfld  33973  irngss  33984  0ringirng  33986  irngnzply1  33988  extdgfialglem1  33989  irngnminplynz  34009  minplyelirng  34012  irredminply  34013  algextdeglem2  34015  algextdeglem4  34017  constrconj  34042  constrextdg2lem  34045  constrext2chnlem  34047  iconstr  34063  constrsdrg  34072  cos9thpiminplylem1  34079  cos9thpiminplylem2  34080  cos9thpiminplylem3  34081  cos9thpiminplylem5  34083  madjusmdetlem2  34125  qtophaus  34133  locfinreflem  34137  zarclssn  34170  zarmxt1  34177  zarcmplem  34178  rhmpreimacn  34182  unitdivcld  34198  tpr2rico  34209  ordtrestNEW  34218  lmxrge0  34249  elzrhunit  34274  qqhf  34283  gsumesum  34356  esumfsup  34367  esumcvg  34383  issgon  34420  sigainb  34433  insiga  34434  isrnmeas  34497  measvunilem  34509  volmeas  34528  ddeval1  34531  ddeval0  34532  imambfm  34559  omssubadd  34597  carsgclctunlem3  34617  eulerpartlemf  34667  eulerpartlemgvv  34673  probun  34716  dstfrvunirn  34772  signslema  34856  signstfvn  34863  signsvtn0  34864  signstfvneq0  34866  signstres  34869  signstfveq0a  34870  breprexplemc  34926  logdivsqrle  34944  hgt750lemg  34948  tgoldbachgtda  34955  tgoldbachgt  34957  lpadmax  34979  lpadleft  34980  lpadright  34981  bnj529  35037  bnj548  35192  bnj570  35200  bnj852  35216  bnj929  35231  bnj1097  35276  bnj1118  35279  bnj1145  35288  funen1cnv  35382  fissorduni  35385  vonf1oonfo  35458  spthcycl  35479  acycgr0v  35498  derangen  35522  subfacp1lem2b  35531  subfacp1lem4  35533  subfacp1lem5  35534  derangfmla  35540  ptpconn  35583  mppspstlem  35921  wsuclem  36173  colinearex  36410  btwnconn1lem11  36447  btwnconn1lem12  36448  fwddifnp1  36515  nn0prpwlem  36682  ttctr  36853  dfttc2g  36866  regsfromregtco  36898  bj-snmoore  37603  bj-imdiridlem  37677  relowlpssretop  37858  fin2so  38106  matunitlindflem2  38116  ptrecube  38119  poimirlem8  38127  poimirlem13  38132  poimirlem15  38134  poimirlem24  38143  poimirlem25  38144  poimirlem26  38145  heicant  38154  mblfinlem2  38157  voliunnfl  38163  mbfresfi  38165  itg2addnclem  38170  itg2addnclem3  38172  itg2gt0cn  38174  ftc1cnnclem  38190  ftc1anclem5  38196  cover2  38214  indexdom  38233  sdclem1  38242  fdc  38244  equivbnd2  38291  heiborlem8  38317  heibor  38320  isdrngo2  38457  iscringd  38497  smprngopr  38551  prnc  38566  eqbrtr  38737  eqeltr  38739  islfld  39686  lkrshpor  39731  lfl1dim  39745  lfl1dim2N  39746  cmtcomlemN  39872  2lplnmN  40183  pmapjat1  40477  trlnid  40803  tendoex  41599  dia1dimid  41687  dibval2  41768  dihmeetlem2N  41923  dochlkr  42009  mapdcv  42284  hdmaplkr  42537  hdmapip0  42539  hlhillcs  42582  aks6d1c6lem4  42790  dvdsexpnn  42942  readvrec  42971  frlmvscadiccat  43128  psrmnd  43161  nacsfix  43293  3rexfrabdioph  43374  4rexfrabdioph  43375  6rexfrabdioph  43376  7rexfrabdioph  43377  eldioph4b  43388  pellexlem2  43407  pellexlem5  43410  jm2.26lem3  43578  numinfctb  43680  ordne0gt0  43838  omge1  43874  omlim2  43876  omord2lim  43877  omord2i  43878  tfsconcatfv  43918  tfsconcatb0  43921  oaun3lem1  43951  ntrclsfv1  44631  ntrneifv1  44655  ntrneifv2  44656  cvgdvgrat  44889  radcnvrat  44890  dvconstbi  44910  bccbc  44921  elpwgded  45140  elpwgdedVD  45492  sspwimpcf  45495  sspwimpcfVD  45496  sspwimpALT2  45503  ax6e2ndeqALT  45506  eliuniin  45677  eliuniin2  45698  qinioo  46111  dfxlim2v  46421  xlimliminflimsup  46436  cncfiooicclem1  46467  ibliooicc  46545  stoweidlem27  46601  stoweidlem28  46602  fourierdlem89  46769  fourierdlem91  46771  fourierdlem92  46772  smflimmpt  47384  odz2prm2pw  48172  perfectALTVlem2  48344  blen1b  49210  naryfvalelfv  49254  itscnhlc0yqe  49381  itsclquadb  49398  lubeldm2  49577  glbeldm2  49578  ipolub  49609  ipoglb  49612  fucofulem1  49931  functhinclem1  50065  thincciso  50074  prsthinc  50085  functermclem  50128  prstchom2ALT  50185  onetansqsecsq  50382  cotsqcscsq  50383  aacllem  50422