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  2785  pm13.181  3042  opabss  5177  axprlem4OLD  5403  axprlem5OLD  5404  euotd  5498  brcogw  5856  somin1  6135  xpdifid  6167  xpdifcnvepel  6168  funfni  6645  fnssres  6662  fn0  6670  fnimadisj  6671  fnimaeq0  6672  foimacnv  6842  fvelimab  6957  dffv2  6980  fvopab3ig  6989  funcnvmpt  6995  dff3  7099  dffo4  7102  fpr2g  7216  ralima  7242  f1eqcocnv  7308  isomin  7344  f1ocnv2d  7673  fnexALT  7954  xp1st  8024  xp2nd  8025  frrlem3  8291  fpr2  8307  wfr3g  8322  wfr2  8330  iinon  8333  tfr3  8392  oawordri  8541  oaass  8552  omeulem1  8573  oeoa  8589  oeoe  8591  oeeulem  8593  elqsn0  8788  funen1cnv  9032  pwdom  9124  enfii  9177  phpeqd  9203  ominf  9231  findcard3  9250  marypha1lem  9400  wofib  9514  cantnff  9650  cantnfp1  9657  cantnf  9669  cnfcomlem  9675  ttrcltr  9692  frr3g  9735  r1sscl  9764  rankval3b  9805  infxpidm2  10017  numdom  10038  onssnum  10040  acni  10045  acni2  10046  dfac5  10128  djulepw  10192  infunsdom1  10211  infunsdom  10212  cofsmo  10268  cfsmolem  10269  fin1ai  10292  fin2i  10294  isf34lem1  10371  fin67  10394  itunisuc  10418  axdc3lem4  10452  zornn0g  10504  ttukeylem6  10513  brdom3  10527  tsken  10756  tskcard  10783  r1tskina  10784  intgru  10816  prlem934  11035  ltexprlem7  11044  supaddc  12199  mul2lt0rlt0  13138  xrmaxeq  13223  xrmineq  13224  xmulneg1  13313  ixxun  13406  difelfzle  13688  ssfzoulel  13808  elfznelfzo  13821  ico01fl0  13872  btwnzge0  13881  ltdifltdiv  13887  ioopnfsup  13917  icopnfsup  13918  modifeq2int  13989  suppssfz  14050  expmordi  14223  zzlesq  14262  faclbnd4lem4  14352  hasheni  14404  hashgt0  14444  hashge1  14445  hashprb  14453  hashpss  14466  lennncl  14591  wrdsymb0  14606  ccatsymb  14640  ccatlid  14644  ccatass  14646  ccatswrd  14730  swrdccat2  14731  ccatpfx  14762  swrdccatfn  14785  swrdccat  14796  revccat  14827  2cshw  14876  cnpart  15317  resqreu  15329  recval  15400  abs1m  15413  abslem2  15417  fzomaxdiflem  15420  sqreulem  15437  sqreu  15438  limsupgre  15558  rlimdiv  15723  fsumparts  15883  climcnds  15930  expcnv  15943  ntrivcvg  15976  mod2eq1n2dvds  16429  ndvdssub  16491  sadcaddlem  16539  rplpwr  16640  dvdssqlem  16648  algcvgblem  16659  eucalgcvga  16668  isprm2lem  16763  powm2modprm  16887  coprimeprodsq  16892  pythagtriplem11  16909  pythagtriplem13  16911  pcadd2  16974  4sqlem11  17039  vdwlem6  17070  vdwlem8  17072  vdwlem10  17074  ramval  17092  ramcl2  17100  ramlb  17103  ram0  17106  mreintcl  17671  mrcval  17690  mrccl  17691  mrcuni  17701  mrcun  17702  acsfiel  17734  rescabs  17914  funcres  17977  setcmon  18168  setcepi  18169  fullestrcsetc  18231  funcsetcestrclem8  18242  fullsetcestrc  18246  yonffthlem  18362  pleval2i  18414  pospo  18423  poslubdg  18492  acsdrsel  18623  acsdrscl  18626  acsficl  18627  psss  18660  chnind  18701  chnub  18702  chnccats1  18705  chnccat  18706  grpidd  18757  ismndd  18849  gsumsgrpccat  18938  gsumwmhm  18943  mulgaddcom  19210  subgmulg  19253  resghm  19348  conjnsg  19370  ghmqusker  19403  f1otrspeq  19563  pmtrval  19567  pmtrrn  19573  pmtrfinv  19577  pmtrprfval  19603  psgnunilem1  19609  psgnunilem5  19610  psgnunilem4  19613  psgneldm2i  19621  lsmelvalix  19757  pj1ghm  19819  efgredlemc  19861  frgp0  19876  qusabl  19981  cycsubgcyg  20017  gsumval3  20023  gsumcllem  20024  ablfac1c  20189  pgpfac1lem5  20197  submomnd  20248  isrngd  20297  isringd  20422  01eq0ring  20680  isdrng4  20891  ornglmullt  21024  orngrmullt  21025  lspsneq0b  21186  lmodindp1  21187  lmhmf1o  21219  lmhmpreima  21221  reslmhm  21225  pwssplit3  21234  lspsncmp  21292  lspsneq  21298  prmidl2  21518  prmidl0  21530  qsidomlem1  21532  ssdifidlprm  21538  prmidlsubm  21539  znf1o  21753  dsmmlss  21946  frlmlbs  21999  frlmup1  22000  psrgrp  22158  mpfind  22318  psdmul  22381  ply1scleq  22517  mat1  22656  chfacfisf  23063  chfacfisfcpmat  23064  uniopn  23106  ntrval  23245  clsval  23246  neival  23311  neiptopreu  23342  lpval  23348  restdis  23387  lmbrf  23469  cnpnei  23473  1stcrest  23662  hauspwdom  23711  lfinpfin  23734  txcnpi  23818  ptrescn  23849  xkococnlem  23869  qtopeu  23926  kqreglem1  23951  ptuncnv  24017  filss  24063  fsubbas  24077  fbasrn  24094  cfinfil  24103  ufinffr  24139  elfm3  24160  rnelfmlem  24162  rnelfm  24163  flimclslem  24194  flfval  24200  isfcf  24244  cnextfvval  24275  cnextf  24276  cnextcn  24277  ustelimasn  24433  trust  24439  restutop  24447  ustuqtop2  24452  utop2nei  24460  ucncn  24494  trcfilu  24503  cnextucn  24512  met1stc  24731  metustexhalf  24766  cfilucfil  24769  psmetutop  24777  nmoix  24939  nmoeq0  24946  idnghm  24953  blcvx  25008  xrsxmet  25020  iccntr  25032  icccmp  25036  iihalf1  25143  iihalf2  25145  xrhmeo  25158  cnheibor  25167  ipcau2  25446  lmmbrf  25474  iscauf  25492  cmetcaulem  25500  bcthlem4  25539  cmetcusp  25566  rrxcph  25604  minveclem4  25644  evthicc2  25672  cniccbdd  25673  ovollb2  25701  ovolunlem1a  25708  ovolunlem1  25709  voliun  25766  icombl  25776  ioombl  25777  iccvolcl  25779  ioovolcl  25782  mbfss  25858  mbfposb  25865  itg2const2  25953  itg2splitlem  25960  itg2gt0  25972  iblss2  26018  itgioo  26028  dvaddf  26154  dvmulf  26155  dvcobr  26158  dvcof  26160  rolle  26202  dvlip  26205  c1lip1  26209  dvivthlem1  26220  lhop1lem  26225  dvfsumlem1  26238  ftc1lem4  26251  ftc1lem5  26252  ply1divmo  26346  coe1termlem  26468  plymulidp  26496  plydiveu  26512  taylplem1  26579  pserulm  26638  abelth  26657  abscxp2  26911  abscxpbnd  26971  logbgt0b  27011  ang180lem2  27028  ang180lem3  27029  isosctrlem1  27036  angpieqvd  27049  atandmtan  27138  birthdaylem3  27171  wilthlem2  27286  wilthimp  27289  isppw  27331  isppw2  27332  dvdsflsumcom  27405  chteq0  27426  perfectlem2  27447  dchrval  27451  dchrinvcl  27470  dchrptlem1  27481  bposlem3  27503  lgslem4  27517  lgsmod  27540  lgsdilem  27541  lgsdir2lem2  27543  lgsdir2  27547  lgsne0  27552  lgsmulsqcoprm  27560  lgseisenlem1  27592  2lgsoddprm  27633  2sqlem4  27638  chpo1ubb  27698  dchrisumn0  27738  pntrsumbnd2  27784  ostthlem1  27844  ostth3  27855  nosupbnd2lem1  27932  noinfbnd2lem1  27947  nocvxmin  28001  eqcuts2  28032  ltslpss  28154  madefi  28159  abslts  28495  eucliddivs  28622  peano5uzs  28650  z12bdaylem1  28716  elreno2  28741  idmot  28859  tgelrnln  28956  lnincplng  29119  plngmiropp  29129  lmimid  29156  lmiisolem  29158  hypcgrlem1  29162  brcgr  29307  colinearalglem4  29316  colinearalg  29317  axlowdimlem14  29362  axcontlem4  29374  cplgrop  29847  lfgriswlk  30100  pthdlem1  30181  spthcycl  30221  crctcshwlkn0  30239  elwspths2on  30380  elwspths2onw  30381  clwlkclwwlklem2fv2  30416  frgrncvvdeqlem9  30731  nvss  31018  sspn  31161  nmoub3i  31198  nmblolbii  31224  blocnilem  31229  minvecolem4  31305  htthlem  31342  norm1  31674  norm1exi  31675  pjeq  31824  axpjpj  31845  normcan  32001  pjoi0  32142  nmopub2tALT  32334  nmfnleub2  32351  eighmorth  32389  nmbdoplbi  32449  nmcoplbi  32453  nmophmi  32456  nmbdfnlbi  32474  nmcfnlbi  32477  riesz3i  32487  cnlnadjlem7  32498  branmfn  32530  nmopleid  32564  hstle  32655  superpos  32779  cvexchlem  32793  foresf1o  32923  elabreximd  32929  prssad  32948  prssbd  32949  unidifsnne  32955  tpssad  32958  fresunsn  33043  f1o3d  33044  fmptco1f1o  33051  fgreu  33089  suppovss  33099  elsuppfnd  33100  fsupprnfi  33110  resf1o  33147  fpwrelmap  33150  argcj  33165  xrofsup  33184  eliccelico  33194  elicoelioo  33195  iocinif  33198  difioo  33199  hashne0  33226  elq2  33228  oexpled  33252  indf1ofs  33258  eliccioo  33322  cshf1o  33348  mgcmnt1d  33383  mgcmnt2d  33384  pwrssmgc  33386  mndlactf1o  33416  mndractf1o  33417  gsummpt2co  33434  gsumhashmul  33453  gsummulsubdishift1  33454  symgcom  33469  symgcom2  33470  odpmco  33472  pmtrcnel  33475  pmtridf1o  33480  cycpmco2lem6  33517  cycpmco2lem7  33518  cycpmco2  33519  cyc3co2  33526  cycpmconjv  33528  tocyccntz  33530  cyc3evpm  33536  cycpmconjslem2  33541  cycpmconjs  33542  fxpsubm  33558  fxpsubg  33559  fxpsubrg  33560  fxpsdrg  33561  archirngz  33575  unitnz  33624  elrgspnlem1  33628  elrgspnlem2  33629  elrgspnlem4  33631  elrgspnsubrun  33635  rloccring  33657  rlocf1  33660  rlocisunit  33662  domnpropd  33666  rrgsubm  33670  sdrgdvcl  33686  sdrginvcl  33687  fracfld  33695  lindssn  33757  linds2eq  33760  dvdsrspss  33766  nsgqusf1olem1  33788  nsgqusf1olem3  33790  unitpidl1  33798  elrspunidl  33802  rhmimaidl  33806  drngidlhash  33807  mxidlirredi  33820  mxidlirred  33821  ssmxidl  33823  drng0mxidl  33824  opprmxidlabs  33835  qsdrngilem  33842  qsdrngi  33843  qsdrng  33845  drnglring  33848  dflring2  33849  dflringlem  33850  dflringlem3  33852  dflring4  33854  fldlring  33855  rsprprmprmidl  33878  rsprprmprmidlb  33879  rprmasso2  33882  rprmirredlem  33886  rprmirredb  33888  1arithidomlem2  33892  1arithufdlem4  33903  1arithufd  33904  ressply1evls1  33921  ply1asclunit  33930  ply1dg1rt  33936  ply1mulrtss  33938  ply1dg3rt0irred  33940  ply1degltlss  33952  ply1gsumz  33955  mplidomlem  33983  evlextv  33998  esplyfv1  34025  esplyind  34031  vietadeg1  34034  lsssra  34044  exsslsb  34053  lbslsat  34072  lindsunlem  34080  lindsun  34081  dimkerim  34083  fedgmullem1  34085  fedgmullem2  34086  fedgmul  34087  dimlssid  34088  lvecendof1f1o  34089  assalactf1o  34091  sdrgfldext  34106  fldsdrgfldext  34117  fldgenfldext  34124  evls1fldgencl  34126  fldextrspunlsp  34130  fldextrspunlem1  34131  fldextrspunfld  34132  irngss  34143  0ringirng  34145  irngnzply1  34147  extdgfialglem1  34148  irngnminplynz  34168  minplyelirng  34171  irredminply  34172  algextdeglem2  34174  algextdeglem4  34176  constrconj  34201  constrextdg2lem  34204  constrext2chnlem  34206  iconstr  34222  constrsdrg  34231  cos9thpiminplylem1  34238  cos9thpiminplylem2  34239  cos9thpiminplylem3  34240  cos9thpiminplylem5  34242  madjusmdetlem2  34284  qtophaus  34292  locfinreflem  34296  zarclssn  34329  zarmxt1  34336  zarcmplem  34337  rhmpreimacn  34341  unitdivcld  34357  tpr2rico  34368  ordtrestNEW  34377  lmxrge0  34408  elzrhunit  34433  qqhf  34442  gsumesum  34515  esumfsup  34526  esumcvg  34542  issgon  34579  sigainb  34593  insiga  34594  isrnmeas  34657  measvunilem  34669  volmeas  34688  ddeval1  34691  ddeval0  34692  imambfm  34719  omssubadd  34757  carsgclctunlem3  34777  eulerpartlemf  34827  eulerpartlemgvv  34833  probun  34876  dstfrvunirn  34932  signslema  35016  signstfvn  35023  signsvtn0  35024  signstfvneq0  35026  signstres  35029  signstfveq0a  35030  breprexplemc  35086  logdivsqrle  35104  hgt750lemg  35108  tgoldbachgtda  35115  tgoldbachgt  35117  lpadmax  35139  lpadleft  35140  lpadright  35141  bnj529  35197  bnj548  35352  bnj570  35360  bnj852  35376  bnj929  35391  bnj1097  35436  bnj1118  35439  bnj1145  35448  fissorduni  35540  vonf1oonfo  35658  acycgr0v  35679  derangen  35703  subfacp1lem2b  35712  subfacp1lem4  35714  subfacp1lem5  35715  derangfmla  35721  ptpconn  35764  mppspstlem  36102  wsuclem  36354  colinearex  36591  btwnconn1lem11  36628  btwnconn1lem12  36629  fwddifnp1  36696  nn0prpwlem  36892  ttctr  37063  dfttc2g  37076  regsfromregtco  37108  bj-snmoore  37814  bj-imdiridlem  37888  relowlpssretop  38069  fin2so  38317  matunitlindflem2  38327  ptrecube  38330  poimirlem8  38338  poimirlem13  38343  poimirlem15  38345  poimirlem24  38354  poimirlem25  38355  poimirlem26  38356  heicant  38365  mblfinlem2  38368  voliunnfl  38374  mbfresfi  38376  itg2addnclem  38381  itg2addnclem3  38383  itg2gt0cn  38385  ftc1cnnclem  38401  ftc1anclem5  38407  cover2  38426  indexdom  38445  sdclem1  38454  fdc  38456  equivbnd2  38503  heiborlem8  38529  heibor  38532  isdrngo2  38669  iscringd  38709  smprngopr  38763  prnc  38778  eqbrtr  38947  eqeltr  38949  islfld  39896  lkrshpor  39941  lfl1dim  39955  lfl1dim2N  39956  cmtcomlemN  40082  2lplnmN  40393  pmapjat1  40687  trlnid  41013  tendoex  41809  dia1dimid  41897  dibval2  41978  dihmeetlem2N  42133  dochlkr  42219  mapdcv  42494  hdmaplkr  42747  hdmapip0  42749  hlhillcs  42792  aks6d1c6lem4  43000  dvdsexpnn  43154  readvrec  43183  frlmvscadiccat  43340  psrmnd  43371  nacsfix  43503  3rexfrabdioph  43584  4rexfrabdioph  43585  6rexfrabdioph  43586  7rexfrabdioph  43587  eldioph4b  43598  pellexlem2  43617  pellexlem5  43620  jm2.26lem3  43788  numinfctb  43890  ordne0gt0  44048  omge1  44084  omlim2  44086  omord2lim  44087  omord2i  44088  tfsconcatfv  44128  tfsconcatb0  44131  oaun3lem1  44161  ntrclsfv1  44841  ntrneifv1  44865  ntrneifv2  44866  cvgdvgrat  45083  radcnvrat  45084  dvconstbi  45104  bccbc  45115  elpwgded  45333  elpwgdedVD  45685  sspwimpcf  45688  sspwimpcfVD  45689  sspwimpALT2  45696  ax6e2ndeqALT  45699  eliuniin  45877  eliuniin2  45898  qinioo  46311  dfxlim2v  46621  xlimliminflimsup  46636  cncfiooicclem1  46667  ibliooicc  46745  stoweidlem27  46801  stoweidlem28  46802  fourierdlem89  46969  fourierdlem91  46971  fourierdlem92  46972  smflimmpt  47584  odz2prm2pw  48375  perfectALTVlem2  48547  blen1b  49427  naryfvalelfv  49471  itscnhlc0yqe  49598  itsclquadb  49615  lubeldm2  49793  glbeldm2  49794  ipolub  49825  ipoglb  49828  fucofulem1  50147  functhinclem1  50281  thincciso  50290  prsthinc  50301  functermclem  50344  prstchom2ALT  50401  onetansqsecsq  50598  cotsqcscsq  50599  aacllem  50680