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  5150  axprlem4OLD  5368  axprlem5OLD  5369  euotd  5462  brcogw  5818  somin1  6091  xpdifid  6127  funfni  6599  fnssres  6616  fn0  6624  fnimadisj  6625  fnimaeq0  6626  foimacnv  6792  fvelimab  6907  dffv2  6930  fvopab3ig  6938  funcnvmpt  6944  dff3  7047  dffo4  7050  fpr2g  7160  ralima  7186  f1eqcocnv  7250  isomin  7286  f1ocnv2d  7614  fnexALT  7898  xp1st  7968  xp2nd  7969  frrlem3  8232  fpr2  8248  wfr3g  8263  wfr2  8271  iinon  8274  tfr3  8332  oawordri  8479  oaass  8490  omeulem1  8511  oeoa  8527  oeoe  8529  oeeulem  8531  elqsn0  8725  pwdom  9061  enfii  9114  phpeqd  9140  ominf  9168  findcard3  9187  marypha1lem  9340  wofib  9454  cantnff  9589  cantnfp1  9596  cantnf  9608  cnfcomlem  9614  ttrcltr  9631  frr3g  9674  r1sscl  9703  rankval3b  9744  infxpidm2  9933  numdom  9954  onssnum  9956  acni  9961  acni2  9962  dfac5  10045  djulepw  10109  infunsdom1  10128  infunsdom  10129  cofsmo  10185  cfsmolem  10186  fin1ai  10209  fin2i  10211  isf34lem1  10288  fin67  10311  itunisuc  10335  axdc3lem4  10369  zornn0g  10421  ttukeylem6  10430  brdom3  10444  tsken  10671  tskcard  10698  r1tskina  10699  intgru  10731  prlem934  10950  ltexprlem7  10959  supaddc  12117  mul2lt0rlt0  13040  xrmaxeq  13125  xrmineq  13126  xmulneg1  13215  ixxun  13308  difelfzle  13589  ssfzoulel  13709  elfznelfzo  13722  ico01fl0  13772  btwnzge0  13781  ltdifltdiv  13787  ioopnfsup  13817  icopnfsup  13818  modifeq2int  13889  suppssfz  13950  expmordi  14123  zzlesq  14162  faclbnd4lem4  14252  hasheni  14304  hashgt0  14344  hashge1  14345  hashprb  14353  lennncl  14490  wrdsymb0  14505  ccatsymb  14539  ccatlid  14543  ccatass  14545  ccatswrd  14625  swrdccat2  14626  ccatpfx  14657  swrdccatfn  14680  swrdccat  14691  revccat  14722  2cshw  14769  cnpart  15196  resqreu  15208  recval  15279  abs1m  15292  abslem2  15296  fzomaxdiflem  15299  sqreulem  15316  sqreu  15317  limsupgre  15437  rlimdiv  15602  fsumparts  15763  climcnds  15810  expcnv  15823  ntrivcvg  15856  mod2eq1n2dvds  16310  ndvdssub  16372  sadcaddlem  16420  rplpwr  16521  dvdssqlem  16529  algcvgblem  16540  eucalgcvga  16549  isprm2lem  16644  powm2modprm  16768  coprimeprodsq  16773  pythagtriplem11  16790  pythagtriplem13  16792  pcadd2  16855  4sqlem11  16920  vdwlem6  16951  vdwlem8  16953  vdwlem10  16955  ramval  16973  ramcl2  16981  ramlb  16984  ram0  16987  mreintcl  17551  mrcval  17570  mrccl  17571  mrcuni  17581  mrcun  17582  acsfiel  17614  rescabs  17794  funcres  17857  setcmon  18048  setcepi  18049  fullestrcsetc  18111  funcsetcestrclem8  18122  fullsetcestrc  18126  yonffthlem  18242  pleval2i  18294  pospo  18303  poslubdg  18372  acsdrsel  18503  acsdrscl  18506  acsficl  18507  psss  18540  chnind  18581  chnub  18582  chnccats1  18585  chnccat  18586  grpidd  18633  ismndd  18718  gsumsgrpccat  18802  gsumwmhm  18807  mulgaddcom  19068  subgmulg  19110  resghm  19201  conjnsg  19223  ghmqusker  19256  f1otrspeq  19416  pmtrval  19420  pmtrrn  19426  pmtrfinv  19430  pmtrprfval  19456  psgnunilem1  19462  psgnunilem5  19463  psgnunilem4  19466  psgneldm2i  19474  lsmelvalix  19610  pj1ghm  19672  efgredlemc  19714  frgp0  19729  qusabl  19834  cycsubgcyg  19870  gsumval3  19876  gsumcllem  19877  ablfac1c  20042  pgpfac1lem5  20050  submomnd  20101  isrngd  20148  isringd  20266  01eq0ring  20501  ornglmullt  20840  orngrmullt  20841  lspsneq0b  21002  lmodindp1  21003  lmhmf1o  21036  lmhmpreima  21038  reslmhm  21042  pwssplit3  21051  lspsncmp  21109  lspsneq  21115  znf1o  21544  dsmmlss  21737  frlmlbs  21790  frlmup1  21791  psrgrp  21948  mpfind  22106  psdmul  22145  ply1scleq  22283  mat1  22425  chfacfisf  22832  chfacfisfcpmat  22833  uniopn  22875  ntrval  23014  clsval  23015  neival  23080  neiptopreu  23111  lpval  23117  restdis  23156  lmbrf  23238  cnpnei  23242  1stcrest  23431  hauspwdom  23479  lfinpfin  23502  txcnpi  23586  ptrescn  23617  xkococnlem  23637  qtopeu  23694  kqreglem1  23719  ptuncnv  23785  filss  23831  fsubbas  23845  fbasrn  23862  cfinfil  23871  ufinffr  23907  elfm3  23928  rnelfmlem  23930  rnelfm  23931  flimclslem  23962  flfval  23968  isfcf  24012  cnextfvval  24043  cnextf  24044  cnextcn  24045  ustelimasn  24201  trust  24207  restutop  24215  ustuqtop2  24220  utop2nei  24228  ucncn  24262  trcfilu  24271  cnextucn  24280  met1stc  24499  metustexhalf  24534  cfilucfil  24537  psmetutop  24545  nmoix  24707  nmoeq0  24714  idnghm  24721  blcvx  24776  xrsxmet  24788  iccntr  24800  icccmp  24804  iihalf1  24911  iihalf2  24913  xrhmeo  24926  cnheibor  24935  ipcau2  25214  lmmbrf  25242  iscauf  25260  cmetcaulem  25268  bcthlem4  25307  cmetcusp  25334  rrxcph  25372  minveclem4  25412  evthicc2  25440  cniccbdd  25441  ovollb2  25469  ovolunlem1a  25476  ovolunlem1  25477  voliun  25534  icombl  25544  ioombl  25545  iccvolcl  25547  ioovolcl  25550  mbfss  25626  mbfposb  25633  itg2const2  25721  itg2splitlem  25728  itg2gt0  25740  iblss2  25786  itgioo  25796  dvaddf  25922  dvmulf  25923  dvcobr  25926  dvcof  25928  rolle  25970  dvlip  25973  c1lip1  25977  dvivthlem1  25988  lhop1lem  25993  dvfsumlem1  26006  ftc1lem4  26019  ftc1lem5  26020  ply1divmo  26114  coe1termlem  26236  plydiveu  26278  taylplem1  26342  pserulm  26403  abelth  26422  abscxp2  26673  abscxpbnd  26733  logbgt0b  26773  ang180lem2  26790  ang180lem3  26791  isosctrlem1  26798  angpieqvd  26811  atandmtan  26900  birthdaylem3  26933  wilthlem2  27049  wilthimp  27052  isppw  27094  isppw2  27095  dvdsflsumcom  27168  chteq0  27189  perfectlem2  27210  dchrval  27214  dchrinvcl  27233  dchrptlem1  27244  bposlem3  27266  lgslem4  27280  lgsmod  27303  lgsdilem  27304  lgsdir2lem2  27306  lgsdir2  27310  lgsne0  27315  lgsmulsqcoprm  27323  lgseisenlem1  27355  2lgsoddprm  27396  2sqlem4  27401  chpo1ubb  27461  dchrisumn0  27501  pntrsumbnd2  27547  ostthlem1  27607  ostth3  27618  nosupbnd2lem1  27696  noinfbnd2lem1  27711  nocvxmin  27764  eqcuts2  27795  ltslpss  27917  madefi  27922  abslts  28258  eucliddivs  28385  peano5uzs  28413  z12bdaylem1  28479  elreno2  28504  idmot  28622  tgelrnln  28715  lmimid  28879  lmiisolem  28881  hypcgrlem1  28884  brcgr  28986  colinearalglem4  28995  colinearalg  28996  axlowdimlem14  29041  axcontlem4  29053  cplgrop  29523  lfgriswlk  29773  pthdlem1  29852  crctcshwlkn0  29907  elwspths2on  30048  elwspths2onw  30049  clwlkclwwlklem2fv2  30084  frgrncvvdeqlem9  30395  nvss  30682  sspn  30825  nmoub3i  30862  nmblolbii  30888  blocnilem  30893  minvecolem4  30969  htthlem  31006  norm1  31338  norm1exi  31339  pjeq  31488  axpjpj  31509  normcan  31665  pjoi0  31806  nmopub2tALT  31998  nmfnleub2  32015  eighmorth  32053  nmbdoplbi  32113  nmcoplbi  32117  nmophmi  32120  nmbdfnlbi  32138  nmcfnlbi  32141  riesz3i  32151  cnlnadjlem7  32162  branmfn  32194  nmopleid  32228  hstle  32319  superpos  32443  cvexchlem  32457  foresf1o  32592  elabreximd  32598  prssad  32617  prssbd  32618  unidifsnne  32624  tpssad  32627  fresunsn  32716  f1o3d  32717  fmptco1f1o  32724  fgreu  32762  suppovss  32772  elsuppfnd  32773  fsupprnfi  32783  resf1o  32821  fpwrelmap  32824  argcj  32839  xrofsup  32858  eliccelico  32868  elicoelioo  32869  iocinif  32872  difioo  32873  hashpss  32900  hashne0  32901  elq2  32903  oexpled  32938  indf1ofs  32944  eliccioo  33008  cshf1o  33040  mgcmnt1d  33075  mgcmnt2d  33076  pwrssmgc  33078  mndlactf1o  33108  mndractf1o  33109  gsummpt2co  33127  gsumhashmul  33146  gsummulsubdishift1  33147  symgcom  33162  symgcom2  33163  odpmco  33165  pmtrcnel  33168  pmtridf1o  33173  cycpmco2lem6  33210  cycpmco2lem7  33211  cycpmco2  33212  cyc3co2  33219  cycpmconjv  33221  tocyccntz  33223  cyc3evpm  33229  cycpmconjslem2  33234  cycpmconjs  33235  fxpsubm  33251  fxpsubg  33252  fxpsubrg  33253  fxpsdrg  33254  archirngz  33268  unitnz  33318  elrgspnlem1  33321  elrgspnlem2  33322  elrgspnlem4  33324  elrgspnsubrun  33328  rloccring  33349  rlocf1  33352  domnpropd  33356  rrgsubm  33363  isdrng4  33374  sdrgdvcl  33378  sdrginvcl  33379  fracfld  33387  lindssn  33456  linds2eq  33459  dvdsrspss  33465  nsgqusf1olem1  33491  nsgqusf1olem3  33493  unitpidl1  33502  elrspunidl  33506  rhmimaidl  33510  drngidlhash  33512  prmidl2  33519  prmidl0  33528  qsidomlem1  33530  ssdifidlprm  33536  mxidlirredi  33549  mxidlirred  33550  ssmxidl  33552  drng0mxidl  33554  opprmxidlabs  33565  qsdrngilem  33572  qsdrngi  33573  qsdrng  33575  rsprprmprmidl  33600  rsprprmprmidlb  33601  rprmasso2  33604  rprmirredlem  33608  rprmirredb  33610  1arithidomlem2  33614  1arithufdlem4  33625  1arithufd  33626  ressply1evls1  33643  ply1asclunit  33652  ply1dg1rt  33658  ply1mulrtss  33660  ply1dg3rt0irred  33662  ply1degltlss  33674  ply1gsumz  33677  evlextv  33704  esplyfv1  33731  esplyind  33737  vietadeg1  33740  lsssra  33750  exsslsb  33759  lbslsat  33779  lindsunlem  33787  lindsun  33788  dimkerim  33790  fedgmullem1  33792  fedgmullem2  33793  fedgmul  33794  dimlssid  33795  lvecendof1f1o  33796  assalactf1o  33798  sdrgfldext  33813  fldsdrgfldext  33824  fldgenfldext  33831  evls1fldgencl  33833  fldextrspunlsp  33837  fldextrspunlem1  33838  fldextrspunfld  33839  irngss  33850  0ringirng  33852  irngnzply1  33854  extdgfialglem1  33855  irngnminplynz  33875  minplyelirng  33878  irredminply  33879  algextdeglem2  33881  algextdeglem4  33883  constrconj  33908  constrextdg2lem  33911  constrext2chnlem  33913  iconstr  33929  constrsdrg  33938  cos9thpiminplylem1  33945  cos9thpiminplylem2  33946  cos9thpiminplylem3  33947  cos9thpiminplylem5  33949  madjusmdetlem2  33991  qtophaus  33999  locfinreflem  34003  zarclssn  34036  zarmxt1  34043  zarcmplem  34044  rhmpreimacn  34048  unitdivcld  34064  tpr2rico  34075  ordtrestNEW  34084  lmxrge0  34115  elzrhunit  34140  qqhf  34149  gsumesum  34222  esumfsup  34233  esumcvg  34249  issgon  34286  sigainb  34299  insiga  34300  isrnmeas  34363  measvunilem  34375  volmeas  34394  ddeval1  34397  ddeval0  34398  imambfm  34425  omssubadd  34463  carsgclctunlem3  34483  eulerpartlemf  34533  eulerpartlemgvv  34539  probun  34582  dstfrvunirn  34638  plymulx  34711  signslema  34725  signstfvn  34732  signsvtn0  34733  signstfvneq0  34735  signstres  34738  signstfveq0a  34739  breprexplemc  34795  logdivsqrle  34813  hgt750lemg  34817  tgoldbachgtda  34824  tgoldbachgt  34826  lpadmax  34845  lpadleft  34846  lpadright  34847  bnj529  34903  bnj548  35058  bnj570  35066  bnj852  35082  bnj929  35097  bnj1097  35142  bnj1118  35145  bnj1145  35154  funen1cnv  35250  fissorduni  35252  spthcycl  35330  acycgr0v  35349  derangen  35373  subfacp1lem2b  35382  subfacp1lem4  35384  subfacp1lem5  35385  derangfmla  35391  ptpconn  35434  mppspstlem  35772  wsuclem  36024  colinearex  36261  btwnconn1lem11  36298  btwnconn1lem12  36299  fwddifnp1  36366  nn0prpwlem  36523  ttctr  36694  dfttc2g  36707  regsfromregtco  36739  bj-snmoore  37444  bj-imdiridlem  37518  relowlpssretop  37697  fin2so  37945  matunitlindflem2  37955  ptrecube  37958  poimirlem8  37966  poimirlem13  37971  poimirlem15  37973  poimirlem24  37982  poimirlem25  37983  poimirlem26  37984  heicant  37993  mblfinlem2  37996  voliunnfl  38002  mbfresfi  38004  itg2addnclem  38009  itg2addnclem3  38011  itg2gt0cn  38013  ftc1cnnclem  38029  ftc1anclem5  38035  cover2  38053  indexdom  38072  sdclem1  38081  fdc  38083  equivbnd2  38130  heiborlem8  38156  heibor  38159  isdrngo2  38296  iscringd  38336  smprngopr  38390  prnc  38405  eqbrtr  38576  eqeltr  38578  islfld  39525  lkrshpor  39570  lfl1dim  39584  lfl1dim2N  39585  cmtcomlemN  39711  2lplnmN  40022  pmapjat1  40316  trlnid  40642  tendoex  41438  dia1dimid  41526  dibval2  41607  dihmeetlem2N  41762  dochlkr  41848  mapdcv  42123  hdmaplkr  42376  hdmapip0  42378  hlhillcs  42421  aks6d1c6lem4  42629  dvdsexpnn  42782  readvrec  42811  frlmvscadiccat  42968  psrmnd  43005  nacsfix  43161  3rexfrabdioph  43246  4rexfrabdioph  43247  6rexfrabdioph  43248  7rexfrabdioph  43249  eldioph4b  43260  pellexlem2  43279  pellexlem5  43282  jm2.26lem3  43450  numinfctb  43552  ordne0gt0  43710  omge1  43746  omlim2  43748  omord2lim  43749  omord2i  43750  tfsconcatfv  43790  tfsconcatb0  43793  oaun3lem1  43823  ntrclsfv1  44503  ntrneifv1  44527  ntrneifv2  44528  cvgdvgrat  44761  radcnvrat  44762  dvconstbi  44782  bccbc  44793  elpwgded  45012  elpwgdedVD  45364  sspwimpcf  45367  sspwimpcfVD  45368  sspwimpALT2  45375  ax6e2ndeqALT  45378  eliuniin  45550  eliuniin2  45571  qinioo  45986  dfxlim2v  46296  xlimliminflimsup  46311  cncfiooicclem1  46342  ibliooicc  46420  stoweidlem27  46476  stoweidlem28  46477  fourierdlem89  46644  fourierdlem91  46646  fourierdlem92  46647  smflimmpt  47259  odz2prm2pw  48041  perfectALTVlem2  48213  blen1b  49079  naryfvalelfv  49123  itscnhlc0yqe  49250  itsclquadb  49267  lubeldm2  49446  glbeldm2  49447  ipolub  49478  ipoglb  49481  fucofulem1  49800  functhinclem1  49934  thincciso  49943  prsthinc  49954  functermclem  49997  prstchom2ALT  50054  onetansqsecsq  50251  cotsqcscsq  50252  aacllem  50291