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  804  exbiri  810  biadanid  822  bibiad  839  oplem1  1056  eqtr  2749  pm13.181  3007  opabss  5166  axprlem4OLD  5379  axprlem5OLD  5380  euotd  5468  brcogw  5822  somin1  6094  xpdifid  6129  funfni  6606  fnssres  6623  fn0  6631  fnimadisj  6632  fnimaeq0  6633  foimacnv  6799  fvelimab  6915  dffv2  6938  fvopab3ig  6946  dff3  7054  dffo4  7057  fpr2g  7167  ralima  7193  f1eqcocnv  7258  isomin  7294  f1ocnv2d  7622  fnexALT  7909  xp1st  7979  xp2nd  7980  frrlem3  8244  fpr2  8260  wfr3g  8275  wfr2  8283  iinon  8286  tfr3  8344  oawordri  8491  oaass  8502  omeulem1  8523  oeoa  8538  oeoe  8540  oeeulem  8542  elqsn0  8734  pwdom  9070  enfii  9127  phpeqd  9153  ominf  9181  findcard3  9205  marypha1lem  9360  wofib  9474  cantnff  9603  cantnfp1  9610  cantnf  9622  cnfcomlem  9628  ttrcltr  9645  frr3g  9685  r1sscl  9714  rankval3b  9755  infxpidm2  9946  numdom  9967  onssnum  9969  acni  9974  acni2  9975  dfac5  10058  djulepw  10122  infunsdom1  10141  infunsdom  10142  cofsmo  10198  cfsmolem  10199  fin1ai  10222  fin2i  10224  isf34lem1  10301  fin67  10324  itunisuc  10348  axdc3lem4  10382  zornn0g  10434  ttukeylem6  10443  brdom3  10457  tsken  10683  tskcard  10710  r1tskina  10711  intgru  10743  prlem934  10962  ltexprlem7  10971  supaddc  12126  mul2lt0rlt0  13031  xrmaxeq  13115  xrmineq  13116  xmulneg1  13205  ixxun  13298  difelfzle  13578  ssfzoulel  13697  elfznelfzo  13709  ico01fl0  13757  btwnzge0  13766  ltdifltdiv  13772  ioopnfsup  13802  icopnfsup  13803  modifeq2int  13874  suppssfz  13935  expmordi  14108  zzlesq  14147  faclbnd4lem4  14237  hasheni  14289  hashgt0  14329  hashge1  14330  hashprb  14338  lennncl  14475  wrdsymb0  14490  ccatsymb  14523  ccatlid  14527  ccatass  14529  ccatswrd  14609  swrdccat2  14610  ccatpfx  14642  swrdccatfn  14665  swrdccat  14676  revccat  14707  2cshw  14754  cnpart  15182  resqreu  15194  recval  15265  abs1m  15278  abslem2  15282  fzomaxdiflem  15285  sqreulem  15302  sqreu  15303  limsupgre  15423  rlimdiv  15588  fsumparts  15748  climcnds  15793  expcnv  15806  ntrivcvg  15839  mod2eq1n2dvds  16293  ndvdssub  16355  sadcaddlem  16403  rplpwr  16504  dvdssqlem  16512  algcvgblem  16523  eucalgcvga  16532  isprm2lem  16627  powm2modprm  16750  coprimeprodsq  16755  pythagtriplem11  16772  pythagtriplem13  16774  pcadd2  16837  4sqlem11  16902  vdwlem6  16933  vdwlem8  16935  vdwlem10  16937  ramval  16955  ramcl2  16963  ramlb  16966  ram0  16969  mreintcl  17532  mrcval  17551  mrccl  17552  mrcuni  17562  mrcun  17563  acsfiel  17595  rescabs  17775  funcres  17838  setcmon  18029  setcepi  18030  fullestrcsetc  18092  funcsetcestrclem8  18103  fullsetcestrc  18107  yonffthlem  18223  pleval2i  18275  pospo  18284  poslubdg  18353  acsdrsel  18484  acsdrscl  18487  acsficl  18488  psss  18521  grpidd  18580  ismndd  18665  gsumsgrpccat  18749  gsumwmhm  18754  mulgaddcom  19012  subgmulg  19054  resghm  19146  conjnsg  19168  ghmqusker  19201  f1otrspeq  19361  pmtrval  19365  pmtrrn  19371  pmtrfinv  19375  pmtrprfval  19401  psgnunilem1  19407  psgnunilem5  19408  psgnunilem4  19411  psgneldm2i  19419  lsmelvalix  19555  pj1ghm  19617  efgredlemc  19659  frgp0  19674  qusabl  19779  cycsubgcyg  19815  gsumval3  19821  gsumcllem  19822  ablfac1c  19987  pgpfac1lem5  19995  submomnd  20046  isrngd  20093  isringd  20211  01eq0ring  20450  ornglmullt  20789  orngrmullt  20790  lspsneq0b  20951  lmodindp1  20952  lmhmf1o  20985  lmhmpreima  20987  reslmhm  20991  pwssplit3  21000  lspsncmp  21058  lspsneq  21064  znf1o  21493  dsmmlss  21686  frlmlbs  21739  frlmup1  21740  psrgrp  21898  mpfind  22047  psdmul  22086  ply1scleq  22225  mat1  22367  chfacfisf  22774  chfacfisfcpmat  22775  uniopn  22817  ntrval  22956  clsval  22957  neival  23022  neiptopreu  23053  lpval  23059  restdis  23098  lmbrf  23180  cnpnei  23184  1stcrest  23373  hauspwdom  23421  lfinpfin  23444  txcnpi  23528  ptrescn  23559  xkococnlem  23579  qtopeu  23636  kqreglem1  23661  ptuncnv  23727  filss  23773  fsubbas  23787  fbasrn  23804  cfinfil  23813  ufinffr  23849  elfm3  23870  rnelfmlem  23872  rnelfm  23873  flimclslem  23904  flfval  23910  isfcf  23954  cnextfvval  23985  cnextf  23986  cnextcn  23987  ustelimasn  24143  trust  24150  restutop  24158  ustuqtop2  24163  utop2nei  24171  ucncn  24205  trcfilu  24214  cnextucn  24223  met1stc  24442  metustexhalf  24477  cfilucfil  24480  psmetutop  24488  nmoix  24650  nmoeq0  24657  idnghm  24664  blcvx  24719  xrsxmet  24731  iccntr  24743  icccmp  24747  iihalf1  24858  iihalf2  24861  xrhmeo  24877  cnheibor  24887  ipcau2  25167  lmmbrf  25195  iscauf  25213  cmetcaulem  25221  bcthlem4  25260  cmetcusp  25287  rrxcph  25325  minveclem4  25365  evthicc2  25394  cniccbdd  25395  ovollb2  25423  ovolunlem1a  25430  ovolunlem1  25431  voliun  25488  icombl  25498  ioombl  25499  iccvolcl  25501  ioovolcl  25504  mbfss  25580  mbfposb  25587  itg2const2  25675  itg2splitlem  25682  itg2gt0  25694  iblss2  25740  itgioo  25750  dvaddf  25878  dvmulf  25879  dvcobr  25882  dvcobrOLD  25883  dvcof  25885  rolle  25927  dvlip  25931  c1lip1  25935  dvivthlem1  25946  lhop1lem  25951  dvfsumlem1  25965  ftc1lem4  25979  ftc1lem5  25980  ply1divmo  26074  coe1termlem  26196  plydiveu  26239  taylplem1  26303  pserulm  26364  abelth  26384  abscxp2  26635  abscxpbnd  26696  logbgt0b  26736  ang180lem2  26753  ang180lem3  26754  isosctrlem1  26761  angpieqvd  26774  atandmtan  26863  birthdaylem3  26896  wilthlem2  27012  wilthimp  27015  isppw  27057  isppw2  27058  dvdsflsumcom  27131  chteq0  27153  perfectlem2  27174  dchrval  27178  dchrinvcl  27197  dchrptlem1  27208  bposlem3  27230  lgslem4  27244  lgsmod  27267  lgsdilem  27268  lgsdir2lem2  27270  lgsdir2  27274  lgsne0  27279  lgsmulsqcoprm  27287  lgseisenlem1  27319  2lgsoddprm  27360  2sqlem4  27365  chpo1ubb  27425  dchrisumn0  27465  pntrsumbnd2  27511  ostthlem1  27571  ostth3  27582  nosupbnd2lem1  27660  noinfbnd2lem1  27675  nocvxmin  27724  eqscut2  27752  sltlpss  27857  madefi  27862  absslt  28191  eucliddivs  28305  peano5uzs  28332  idmot  28517  tgelrnln  28610  lmimid  28774  lmiisolem  28776  hypcgrlem1  28779  brcgr  28880  colinearalglem4  28889  colinearalg  28890  axlowdimlem14  28935  axcontlem4  28947  cplgrop  29417  lfgriswlk  29667  pthdlem1  29746  crctcshwlkn0  29801  elwspths2on  29940  clwlkclwwlklem2fv2  29975  frgrncvvdeqlem9  30286  nvss  30572  sspn  30715  nmoub3i  30752  nmblolbii  30778  blocnilem  30783  minvecolem4  30859  htthlem  30896  norm1  31228  norm1exi  31229  pjeq  31378  axpjpj  31399  normcan  31555  pjoi0  31696  nmopub2tALT  31888  nmfnleub2  31905  eighmorth  31943  nmbdoplbi  32003  nmcoplbi  32007  nmophmi  32010  nmbdfnlbi  32028  nmcfnlbi  32031  riesz3i  32041  cnlnadjlem7  32052  branmfn  32084  nmopleid  32118  hstle  32209  superpos  32333  cvexchlem  32347  foresf1o  32483  elabreximd  32489  prssad  32508  prssbd  32509  unidifsnne  32515  tpssad  32518  f1o3d  32601  fmptco1f1o  32607  funcnvmpt  32641  fgreu  32646  suppovss  32654  elsuppfnd  32655  fsupprnfi  32665  resf1o  32703  fpwrelmap  32706  argcj  32722  xrofsup  32740  eliccelico  32750  elicoelioo  32751  iocinif  32754  difioo  32755  hashpss  32784  hashne0  32785  elq2  32786  oexpled  32822  indf1ofs  32839  eliccioo  32901  cshf1o  32934  mgcmnt1d  32969  mgcmnt2d  32970  pwrssmgc  32972  chnind  32983  chnub  32984  chnccats1  32987  mndlactf1o  33014  mndractf1o  33015  gsummpt2co  33031  gsumhashmul  33044  symgcom  33055  symgcom2  33056  odpmco  33058  pmtrcnel  33061  pmtridf1o  33066  cycpmco2lem6  33103  cycpmco2lem7  33104  cycpmco2  33105  cyc3co2  33112  cycpmconjv  33114  tocyccntz  33116  cyc3evpm  33122  cycpmconjslem2  33127  cycpmconjs  33128  fxpsubm  33144  archirngz  33158  unitnz  33206  elrgspnlem1  33209  elrgspnlem2  33210  elrgspnlem4  33212  elrgspnsubrun  33216  rloccring  33237  rlocf1  33240  domnpropd  33243  rrgsubm  33250  isdrng4  33261  sdrgdvcl  33265  sdrginvcl  33266  fracfld  33274  lindssn  33342  linds2eq  33345  dvdsrspss  33351  nsgqusf1olem1  33377  nsgqusf1olem3  33379  unitpidl1  33388  elrspunidl  33392  rhmimaidl  33396  drngidlhash  33398  prmidl2  33405  prmidl0  33414  qsidomlem1  33416  ssdifidlprm  33422  mxidlirredi  33435  mxidlirred  33436  ssmxidl  33438  drng0mxidl  33440  opprmxidlabs  33451  qsdrngilem  33458  qsdrngi  33459  qsdrng  33461  rsprprmprmidl  33486  rsprprmprmidlb  33487  rprmasso2  33490  rprmirredlem  33494  rprmirredb  33496  1arithidomlem2  33500  1arithufdlem4  33511  1arithufd  33512  ressply1evls1  33527  ply1asclunit  33536  ply1dg1rt  33541  ply1mulrtss  33543  ply1dg3rt0irred  33544  ply1degltlss  33555  ply1gsumz  33557  lsssra  33577  exsslsb  33585  lbslsat  33605  lindsunlem  33613  lindsun  33614  dimkerim  33616  fedgmullem1  33618  fedgmullem2  33619  fedgmul  33620  dimlssid  33621  lvecendof1f1o  33622  assalactf1o  33624  sdrgfldext  33639  fldsdrgfldext  33650  fldgenfldext  33656  evls1fldgencl  33658  fldextrspunlsp  33662  fldextrspunlem1  33663  fldextrspunfld  33664  irngss  33675  0ringirng  33677  irngnzply1  33679  irngnminplynz  33695  minplyelirng  33698  irredminply  33699  algextdeglem2  33701  algextdeglem4  33703  constrconj  33728  constrextdg2lem  33731  constrext2chnlem  33733  iconstr  33749  constrsdrg  33758  cos9thpiminplylem1  33765  cos9thpiminplylem2  33766  cos9thpiminplylem3  33767  cos9thpiminplylem5  33769  madjusmdetlem2  33811  qtophaus  33819  locfinreflem  33823  zarclssn  33856  zarmxt1  33863  zarcmplem  33864  rhmpreimacn  33868  unitdivcld  33884  tpr2rico  33895  ordtrestNEW  33904  lmxrge0  33935  elzrhunit  33960  qqhf  33969  gsumesum  34042  esumfsup  34053  esumcvg  34069  issgon  34106  sigainb  34119  insiga  34120  isrnmeas  34183  measvunilem  34195  volmeas  34214  ddeval1  34217  ddeval0  34218  imambfm  34246  omssubadd  34284  carsgclctunlem3  34304  eulerpartlemf  34354  eulerpartlemgvv  34360  probun  34403  dstfrvunirn  34459  plymulx  34532  signslema  34546  signstfvn  34553  signsvtn0  34554  signstfvneq0  34556  signstres  34559  signstfveq0a  34560  breprexplemc  34616  logdivsqrle  34634  hgt750lemg  34638  tgoldbachgtda  34645  tgoldbachgt  34647  lpadmax  34666  lpadleft  34667  lpadright  34668  bnj529  34724  bnj548  34880  bnj570  34888  bnj852  34904  bnj929  34919  bnj1097  34964  bnj1118  34967  bnj1145  34976  funen1cnv  35071  spthcycl  35109  acycgr0v  35128  derangen  35152  subfacp1lem2b  35161  subfacp1lem4  35163  subfacp1lem5  35164  derangfmla  35170  ptpconn  35213  mppspstlem  35551  wsuclem  35806  colinearex  36041  btwnconn1lem11  36078  btwnconn1lem12  36079  fwddifnp1  36146  nn0prpwlem  36303  bj-snmoore  37094  bj-imdiridlem  37166  relowlpssretop  37345  fin2so  37594  matunitlindflem2  37604  ptrecube  37607  poimirlem8  37615  poimirlem13  37620  poimirlem15  37622  poimirlem24  37631  poimirlem25  37632  poimirlem26  37633  heicant  37642  mblfinlem2  37645  voliunnfl  37651  mbfresfi  37653  itg2addnclem  37658  itg2addnclem3  37660  itg2gt0cn  37662  ftc1cnnclem  37678  ftc1anclem5  37684  cover2  37702  indexdom  37721  sdclem1  37730  fdc  37732  equivbnd2  37779  heiborlem8  37805  heibor  37808  isdrngo2  37945  iscringd  37985  smprngopr  38039  prnc  38054  eqbrtr  38213  eqeltr  38215  islfld  39048  lkrshpor  39093  lfl1dim  39107  lfl1dim2N  39108  cmtcomlemN  39234  2lplnmN  39546  pmapjat1  39840  trlnid  40166  tendoex  40962  dia1dimid  41050  dibval2  41131  dihmeetlem2N  41286  dochlkr  41372  mapdcv  41647  hdmaplkr  41900  hdmapip0  41902  hlhillcs  41945  aks6d1c6lem4  42154  dvdsexpnn  42314  readvrec  42343  frlmvscadiccat  42487  psrmnd  42526  nacsfix  42693  3rexfrabdioph  42778  4rexfrabdioph  42779  6rexfrabdioph  42780  7rexfrabdioph  42781  eldioph4b  42792  pellexlem2  42811  pellexlem5  42814  jm2.26lem3  42983  numinfctb  43085  ordne0gt0  43243  omge1  43279  omlim2  43281  omord2lim  43282  omord2i  43283  tfsconcatfv  43323  tfsconcatb0  43326  oaun3lem1  43356  ntrclsfv1  44037  ntrneifv1  44061  ntrneifv2  44062  cvgdvgrat  44295  radcnvrat  44296  dvconstbi  44316  bccbc  44327  elpwgded  44547  elpwgdedVD  44899  sspwimpcf  44902  sspwimpcfVD  44903  sspwimpALT2  44910  ax6e2ndeqALT  44913  eliuniin  45086  eliuniin2  45107  qinioo  45526  dfxlim2v  45838  xlimliminflimsup  45853  cncfiooicclem1  45884  ibliooicc  45962  stoweidlem27  46018  stoweidlem28  46019  fourierdlem89  46186  fourierdlem91  46188  fourierdlem92  46189  smflimmpt  46801  odz2prm2pw  47557  perfectALTVlem2  47716  blen1b  48570  naryfvalelfv  48614  itscnhlc0yqe  48741  itsclquadb  48758  lubeldm2  48937  glbeldm2  48938  ipolub  48969  ipoglb  48972  fucofulem1  49292  functhinclem1  49426  thincciso  49435  prsthinc  49446  functermclem  49489  prstchom2ALT  49546  onetansqsecsq  49743  cotsqcscsq  49744  aacllem  49783