Theorem biimpar 478

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  bitr  810  exbiri  816  biadanid  828  bibiad  845  oplem1  1062  eqtr  2759  pm13.181  3016  opabss  5136  axprlem4OLD  5359  axprlem5OLD  5360  euotd  5454  brcogw  5810  somin1  6083  xpdifid  6119  funfni  6591  fnssres  6608  fn0  6616  fnimadisj  6617  fnimaeq0  6618  foimacnv  6784  fvelimab  6899  dffv2  6922  fvopab3ig  6931  funcnvmpt  6937  dff3  7041  dffo4  7044  fpr2g  7155  ralima  7181  f1eqcocnv  7245  isomin  7281  f1ocnv2d  7609  fnexALT  7893  xp1st  7963  xp2nd  7964  frrlem3  8228  fpr2  8244  wfr3g  8259  wfr2  8267  iinon  8270  tfr3  8328  oawordri  8475  oaass  8486  omeulem1  8507  oeoa  8523  oeoe  8525  oeeulem  8527  elqsn0  8721  pwdom  9057  enfii  9110  phpeqd  9136  ominf  9164  findcard3  9183  marypha1lem  9336  wofib  9450  cantnff  9586  cantnfp1  9593  cantnf  9605  cnfcomlem  9611  ttrcltr  9628  frr3g  9671  r1sscl  9700  rankval3b  9741  infxpidm2  9930  numdom  9951  onssnum  9953  acni  9958  acni2  9959  dfac5  10042  djulepw  10106  infunsdom1  10125  infunsdom  10126  cofsmo  10182  cfsmolem  10183  fin1ai  10206  fin2i  10208  isf34lem1  10285  fin67  10308  itunisuc  10332  axdc3lem4  10366  zornn0g  10418  ttukeylem6  10427  brdom3  10441  tsken  10668  tskcard  10695  r1tskina  10696  intgru  10728  prlem934  10947  ltexprlem7  10956  supaddc  12114  mul2lt0rlt0  13037  xrmaxeq  13122  xrmineq  13123  xmulneg1  13212  ixxun  13305  difelfzle  13586  ssfzoulel  13706  elfznelfzo  13719  ico01fl0  13769  btwnzge0  13778  ltdifltdiv  13784  ioopnfsup  13814  icopnfsup  13815  modifeq2int  13886  suppssfz  13947  expmordi  14120  zzlesq  14159  faclbnd4lem4  14249  hasheni  14301  hashgt0  14341  hashge1  14342  hashprb  14350  lennncl  14487  wrdsymb0  14502  ccatsymb  14536  ccatlid  14540  ccatass  14542  ccatswrd  14622  swrdccat2  14623  ccatpfx  14654  swrdccatfn  14677  swrdccat  14688  revccat  14719  2cshw  14766  cnpart  15193  resqreu  15205  recval  15276  abs1m  15289  abslem2  15293  fzomaxdiflem  15296  sqreulem  15313  sqreu  15314  limsupgre  15434  rlimdiv  15599  fsumparts  15760  climcnds  15807  expcnv  15820  ntrivcvg  15853  mod2eq1n2dvds  16307  ndvdssub  16369  sadcaddlem  16417  rplpwr  16518  dvdssqlem  16526  algcvgblem  16537  eucalgcvga  16546  isprm2lem  16641  powm2modprm  16765  coprimeprodsq  16770  pythagtriplem11  16787  pythagtriplem13  16789  pcadd2  16852  4sqlem11  16917  vdwlem6  16948  vdwlem8  16950  vdwlem10  16952  ramval  16970  ramcl2  16978  ramlb  16981  ram0  16984  mreintcl  17548  mrcval  17567  mrccl  17568  mrcuni  17578  mrcun  17579  acsfiel  17611  rescabs  17791  funcres  17854  setcmon  18045  setcepi  18046  fullestrcsetc  18108  funcsetcestrclem8  18119  fullsetcestrc  18123  yonffthlem  18239  pleval2i  18291  pospo  18300  poslubdg  18369  acsdrsel  18500  acsdrscl  18503  acsficl  18504  psss  18537  chnind  18578  chnub  18579  chnccats1  18582  chnccat  18583  grpidd  18630  ismndd  18715  gsumsgrpccat  18799  gsumwmhm  18804  mulgaddcom  19065  subgmulg  19107  resghm  19198  conjnsg  19220  ghmqusker  19253  f1otrspeq  19413  pmtrval  19417  pmtrrn  19423  pmtrfinv  19427  pmtrprfval  19453  psgnunilem1  19459  psgnunilem5  19460  psgnunilem4  19463  psgneldm2i  19471  lsmelvalix  19607  pj1ghm  19669  efgredlemc  19711  frgp0  19726  qusabl  19831  cycsubgcyg  19867  gsumval3  19873  gsumcllem  19874  ablfac1c  20039  pgpfac1lem5  20047  submomnd  20098  isrngd  20145  isringd  20263  01eq0ring  20502  ornglmullt  20841  orngrmullt  20842  lspsneq0b  21003  lmodindp1  21004  lmhmf1o  21036  lmhmpreima  21038  reslmhm  21042  pwssplit3  21051  lspsncmp  21109  lspsneq  21115  znf1o  21526  dsmmlss  21719  frlmlbs  21772  frlmup1  21773  psrgrp  21931  mpfind  22091  psdmul  22154  ply1scleq  22291  mat1  22430  chfacfisf  22837  chfacfisfcpmat  22838  uniopn  22880  ntrval  23019  clsval  23020  neival  23085  neiptopreu  23116  lpval  23122  restdis  23161  lmbrf  23243  cnpnei  23247  1stcrest  23436  hauspwdom  23484  lfinpfin  23507  txcnpi  23591  ptrescn  23622  xkococnlem  23642  qtopeu  23699  kqreglem1  23724  ptuncnv  23790  filss  23836  fsubbas  23850  fbasrn  23867  cfinfil  23876  ufinffr  23912  elfm3  23933  rnelfmlem  23935  rnelfm  23936  flimclslem  23967  flfval  23973  isfcf  24017  cnextfvval  24048  cnextf  24049  cnextcn  24050  ustelimasn  24206  trust  24212  restutop  24220  ustuqtop2  24225  utop2nei  24233  ucncn  24267  trcfilu  24276  cnextucn  24285  met1stc  24504  metustexhalf  24539  cfilucfil  24542  psmetutop  24550  nmoix  24712  nmoeq0  24719  idnghm  24726  blcvx  24781  xrsxmet  24793  iccntr  24805  icccmp  24809  iihalf1  24916  iihalf2  24918  xrhmeo  24931  cnheibor  24940  ipcau2  25219  lmmbrf  25247  iscauf  25265  cmetcaulem  25273  bcthlem4  25312  cmetcusp  25339  rrxcph  25377  minveclem4  25417  evthicc2  25445  cniccbdd  25446  ovollb2  25474  ovolunlem1a  25481  ovolunlem1  25482  voliun  25539  icombl  25549  ioombl  25550  iccvolcl  25552  ioovolcl  25555  mbfss  25631  mbfposb  25638  itg2const2  25726  itg2splitlem  25733  itg2gt0  25745  iblss2  25791  itgioo  25801  dvaddf  25927  dvmulf  25928  dvcobr  25931  dvcof  25933  rolle  25975  dvlip  25978  c1lip1  25982  dvivthlem1  25993  lhop1lem  25998  dvfsumlem1  26011  ftc1lem4  26024  ftc1lem5  26025  ply1divmo  26119  coe1termlem  26241  plydiveu  26282  taylplem1  26346  pserulm  26405  abelth  26424  abscxp2  26675  abscxpbnd  26735  logbgt0b  26775  ang180lem2  26792  ang180lem3  26793  isosctrlem1  26800  angpieqvd  26813  atandmtan  26902  birthdaylem3  26935  wilthlem2  27050  wilthimp  27053  isppw  27095  isppw2  27096  dvdsflsumcom  27169  chteq0  27190  perfectlem2  27211  dchrval  27215  dchrinvcl  27234  dchrptlem1  27245  bposlem3  27267  lgslem4  27281  lgsmod  27304  lgsdilem  27305  lgsdir2lem2  27307  lgsdir2  27311  lgsne0  27316  lgsmulsqcoprm  27324  lgseisenlem1  27356  2lgsoddprm  27397  2sqlem4  27402  chpo1ubb  27462  dchrisumn0  27502  pntrsumbnd2  27548  ostthlem1  27608  ostth3  27619  nosupbnd2lem1  27697  noinfbnd2lem1  27712  nocvxmin  27765  eqcuts2  27796  ltslpss  27918  madefi  27923  abslts  28259  eucliddivs  28386  peano5uzs  28414  z12bdaylem1  28480  elreno2  28505  idmot  28623  tgelrnln  28716  lmimid  28880  lmiisolem  28882  hypcgrlem1  28885  brcgr  28987  colinearalglem4  28996  colinearalg  28997  axlowdimlem14  29042  axcontlem4  29054  cplgrop  29524  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  32717  f1o3d  32718  fmptco1f1o  32725  fgreu  32763  suppovss  32773  elsuppfnd  32774  fsupprnfi  32784  resf1o  32822  fpwrelmap  32825  argcj  32840  xrofsup  32859  eliccelico  32869  elicoelioo  32870  iocinif  32873  difioo  32874  hashpss  32901  hashne0  32902  elq2  32904  oexpled  32939  indf1ofs  32945  eliccioo  33009  cshf1o  33041  mgcmnt1d  33076  mgcmnt2d  33077  pwrssmgc  33079  mndlactf1o  33109  mndractf1o  33110  gsummpt2co  33129  gsumhashmul  33148  gsummulsubdishift1  33149  symgcom  33164  symgcom2  33165  odpmco  33167  pmtrcnel  33170  pmtridf1o  33175  cycpmco2lem6  33212  cycpmco2lem7  33213  cycpmco2  33214  cyc3co2  33221  cycpmconjv  33223  tocyccntz  33225  cyc3evpm  33231  cycpmconjslem2  33236  cycpmconjs  33237  fxpsubm  33253  fxpsubg  33254  fxpsubrg  33255  fxpsdrg  33256  archirngz  33270  unitnz  33320  elrgspnlem1  33323  elrgspnlem2  33324  elrgspnlem4  33326  elrgspnsubrun  33330  rloccring  33351  rlocf1  33354  domnpropd  33358  rrgsubm  33365  isdrng4  33379  sdrgdvcl  33383  sdrginvcl  33384  fracfld  33392  lindssn  33461  linds2eq  33464  dvdsrspss  33470  nsgqusf1olem1  33496  nsgqusf1olem3  33498  unitpidl1  33507  elrspunidl  33511  rhmimaidl  33515  drngidlhash  33517  prmidl2  33524  prmidl0  33533  qsidomlem1  33535  ssdifidlprm  33541  mxidlirredi  33554  mxidlirred  33555  ssmxidl  33557  drng0mxidl  33559  opprmxidlabs  33570  qsdrngilem  33577  qsdrngi  33578  qsdrng  33580  rsprprmprmidl  33605  rsprprmprmidlb  33606  rprmasso2  33609  rprmirredlem  33613  rprmirredb  33615  1arithidomlem2  33619  1arithufdlem4  33630  1arithufd  33631  ressply1evls1  33648  ply1asclunit  33657  ply1dg1rt  33663  ply1mulrtss  33665  ply1dg3rt0irred  33667  ply1degltlss  33679  ply1gsumz  33682  mplidomlem  33711  evlextv  33726  esplyfv1  33753  esplyind  33759  vietadeg1  33762  lsssra  33772  exsslsb  33781  lbslsat  33800  lindsunlem  33808  lindsun  33809  dimkerim  33811  fedgmullem1  33813  fedgmullem2  33814  fedgmul  33815  dimlssid  33816  lvecendof1f1o  33817  assalactf1o  33819  sdrgfldext  33834  fldsdrgfldext  33845  fldgenfldext  33852  evls1fldgencl  33854  fldextrspunlsp  33858  fldextrspunlem1  33859  fldextrspunfld  33860  irngss  33871  0ringirng  33873  irngnzply1  33875  extdgfialglem1  33876  irngnminplynz  33896  minplyelirng  33899  irredminply  33900  algextdeglem2  33902  algextdeglem4  33904  constrconj  33929  constrextdg2lem  33932  constrext2chnlem  33934  iconstr  33950  constrsdrg  33959  cos9thpiminplylem1  33966  cos9thpiminplylem2  33967  cos9thpiminplylem3  33968  cos9thpiminplylem5  33970  madjusmdetlem2  34012  qtophaus  34020  locfinreflem  34024  zarclssn  34057  zarmxt1  34064  zarcmplem  34065  rhmpreimacn  34069  unitdivcld  34085  tpr2rico  34096  ordtrestNEW  34105  lmxrge0  34136  elzrhunit  34161  qqhf  34170  gsumesum  34243  esumfsup  34254  esumcvg  34270  issgon  34307  sigainb  34320  insiga  34321  isrnmeas  34384  measvunilem  34396  volmeas  34415  ddeval1  34418  ddeval0  34419  imambfm  34446  omssubadd  34484  carsgclctunlem3  34504  eulerpartlemf  34554  eulerpartlemgvv  34560  probun  34603  dstfrvunirn  34659  plymulx  34732  signslema  34746  signstfvn  34753  signsvtn0  34754  signstfvneq0  34756  signstres  34759  signstfveq0a  34760  breprexplemc  34816  logdivsqrle  34834  hgt750lemg  34838  tgoldbachgtda  34845  tgoldbachgt  34847  lpadmax  34866  lpadleft  34867  lpadright  34868  bnj529  34924  bnj548  35079  bnj570  35087  bnj852  35103  bnj929  35118  bnj1097  35163  bnj1118  35166  bnj1145  35175  funen1cnv  35269  fissorduni  35271  spthcycl  35357  acycgr0v  35376  derangen  35400  subfacp1lem2b  35409  subfacp1lem4  35411  subfacp1lem5  35412  derangfmla  35418  ptpconn  35461  mppspstlem  35799  wsuclem  36051  colinearex  36288  btwnconn1lem11  36325  btwnconn1lem12  36326  fwddifnp1  36393  nn0prpwlem  36550  ttctr  36721  dfttc2g  36734  regsfromregtco  36766  bj-snmoore  37471  bj-imdiridlem  37545  relowlpssretop  37726  fin2so  37974  matunitlindflem2  37984  ptrecube  37987  poimirlem8  37995  poimirlem13  38000  poimirlem15  38002  poimirlem24  38011  poimirlem25  38012  poimirlem26  38013  heicant  38022  mblfinlem2  38025  voliunnfl  38031  mbfresfi  38033  itg2addnclem  38038  itg2addnclem3  38040  itg2gt0cn  38042  ftc1cnnclem  38058  ftc1anclem5  38064  cover2  38082  indexdom  38101  sdclem1  38110  fdc  38112  equivbnd2  38159  heiborlem8  38185  heibor  38188  isdrngo2  38325  iscringd  38365  smprngopr  38419  prnc  38434  eqbrtr  38605  eqeltr  38607  islfld  39554  lkrshpor  39599  lfl1dim  39613  lfl1dim2N  39614  cmtcomlemN  39740  2lplnmN  40051  pmapjat1  40345  trlnid  40671  tendoex  41467  dia1dimid  41555  dibval2  41636  dihmeetlem2N  41791  dochlkr  41877  mapdcv  42152  hdmaplkr  42405  hdmapip0  42407  hlhillcs  42450  aks6d1c6lem4  42658  dvdsexpnn  42810  readvrec  42839  frlmvscadiccat  42996  psrmnd  43029  nacsfix  43161  3rexfrabdioph  43242  4rexfrabdioph  43243  6rexfrabdioph  43244  7rexfrabdioph  43245  eldioph4b  43256  pellexlem2  43275  pellexlem5  43278  jm2.26lem3  43446  numinfctb  43548  ordne0gt0  43706  omge1  43742  omlim2  43744  omord2lim  43745  omord2i  43746  tfsconcatfv  43786  tfsconcatb0  43789  oaun3lem1  43819  ntrclsfv1  44499  ntrneifv1  44523  ntrneifv2  44524  cvgdvgrat  44757  radcnvrat  44758  dvconstbi  44778  bccbc  44789  elpwgded  45008  elpwgdedVD  45360  sspwimpcf  45363  sspwimpcfVD  45364  sspwimpALT2  45371  ax6e2ndeqALT  45374  eliuniin  45546  eliuniin2  45567  qinioo  45980  dfxlim2v  46290  xlimliminflimsup  46305  cncfiooicclem1  46336  ibliooicc  46414  stoweidlem27  46470  stoweidlem28  46471  fourierdlem89  46638  fourierdlem91  46640  fourierdlem92  46641  smflimmpt  47253  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