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  2755  pm13.181  3014  opabss  5183  axprlem4OLD  5399  axprlem5OLD  5400  euotd  5488  brcogw  5848  somin1  6122  xpdifid  6157  funfni  6643  fnssres  6660  fn0  6668  fnimadisj  6669  fnimaeq0  6670  foimacnv  6834  fvelimab  6950  dffv2  6973  fvopab3ig  6981  dff3  7089  dffo4  7092  fpr2g  7202  ralima  7228  f1eqcocnv  7293  isomin  7329  f1ocnv2d  7658  fnexALT  7947  xp1st  8018  xp2nd  8019  frrlem3  8285  fpr2  8301  wfr3g  8319  wfrlem3OLD  8322  wfrlem4OLD  8324  wfr2  8348  iinon  8352  tfr3  8411  oawordri  8560  oaass  8571  omeulem1  8592  oeoa  8607  oeoe  8609  oeeulem  8611  ecelqsg  8784  elqsn0  8798  pwdom  9141  enfii  9198  phpeqd  9224  ominf  9264  findcard3  9288  marypha1lem  9443  wofib  9557  cantnff  9686  cantnfp1  9693  cantnf  9705  cnfcomlem  9711  ttrcltr  9728  frr3g  9768  r1sscl  9797  rankval3b  9838  infxpidm2  10029  numdom  10050  onssnum  10052  acni  10057  acni2  10058  dfac5  10141  djulepw  10205  infunsdom1  10224  infunsdom  10225  cofsmo  10281  cfsmolem  10282  fin1ai  10305  fin2i  10307  isf34lem1  10384  fin67  10407  itunisuc  10431  axdc3lem4  10465  zornn0g  10517  ttukeylem6  10526  brdom3  10540  tsken  10766  tskcard  10793  r1tskina  10794  intgru  10826  prlem934  11045  ltexprlem7  11054  supaddc  12207  mul2lt0rlt0  13109  xrmaxeq  13193  xrmineq  13194  xmulneg1  13283  ixxun  13376  difelfzle  13656  ssfzoulel  13774  elfznelfzo  13786  ico01fl0  13834  btwnzge0  13843  ltdifltdiv  13849  ioopnfsup  13879  icopnfsup  13880  modifeq2int  13949  suppssfz  14010  expmordi  14183  zzlesq  14222  faclbnd4lem4  14312  hasheni  14364  hashgt0  14404  hashge1  14405  hashprb  14413  lennncl  14550  wrdsymb0  14565  ccatsymb  14598  ccatlid  14602  ccatass  14604  ccatswrd  14684  swrdccat2  14685  ccatpfx  14717  swrdccatfn  14740  swrdccat  14751  revccat  14782  2cshw  14829  cnpart  15257  resqreu  15269  recval  15339  abs1m  15352  abslem2  15356  fzomaxdiflem  15359  sqreulem  15376  sqreu  15377  limsupgre  15495  rlimdiv  15660  fsumparts  15820  climcnds  15865  expcnv  15878  ntrivcvg  15911  mod2eq1n2dvds  16364  ndvdssub  16426  sadcaddlem  16474  rplpwr  16575  dvdssqlem  16583  algcvgblem  16594  eucalgcvga  16603  isprm2lem  16698  powm2modprm  16821  coprimeprodsq  16826  pythagtriplem11  16843  pythagtriplem13  16845  pcadd2  16908  4sqlem11  16973  vdwlem6  17004  vdwlem8  17006  vdwlem10  17008  ramval  17026  ramcl2  17034  ramlb  17037  ram0  17040  mreintcl  17605  mrcval  17620  mrccl  17621  mrcuni  17631  mrcun  17632  acsfiel  17664  rescabs  17844  funcres  17907  setcmon  18098  setcepi  18099  fullestrcsetc  18161  funcsetcestrclem8  18172  fullsetcestrc  18176  yonffthlem  18292  pleval2i  18344  pospo  18353  poslubdg  18422  acsdrsel  18551  acsdrscl  18554  acsficl  18555  psss  18588  grpidd  18647  ismndd  18732  gsumsgrpccat  18816  gsumwmhm  18821  mulgaddcom  19079  subgmulg  19121  resghm  19213  conjnsg  19235  ghmqusker  19268  f1otrspeq  19426  pmtrval  19430  pmtrrn  19436  pmtrfinv  19440  pmtrprfval  19466  psgnunilem1  19472  psgnunilem5  19473  psgnunilem4  19476  psgneldm2i  19484  lsmelvalix  19620  pj1ghm  19682  efgredlemc  19724  frgp0  19739  qusabl  19844  cycsubgcyg  19880  gsumval3  19886  gsumcllem  19887  ablfac1c  20052  pgpfac1lem5  20060  isrngd  20131  isringd  20249  01eq0ring  20488  lspsneq0b  20968  lmodindp1  20969  lmhmf1o  21002  lmhmpreima  21004  reslmhm  21008  pwssplit3  21017  lspsncmp  21075  lspsneq  21081  znf1o  21510  dsmmlss  21702  frlmlbs  21755  frlmup1  21756  psrgrp  21914  mpfind  22063  psdmul  22102  ply1scleq  22241  mat1  22383  chfacfisf  22790  chfacfisfcpmat  22791  uniopn  22833  ntrval  22972  clsval  22973  neival  23038  neiptopreu  23069  lpval  23075  restdis  23114  lmbrf  23196  cnpnei  23200  1stcrest  23389  hauspwdom  23437  lfinpfin  23460  txcnpi  23544  ptrescn  23575  xkococnlem  23595  qtopeu  23652  kqreglem1  23677  ptuncnv  23743  filss  23789  fsubbas  23803  fbasrn  23820  cfinfil  23829  ufinffr  23865  elfm3  23886  rnelfmlem  23888  rnelfm  23889  flimclslem  23920  flfval  23926  isfcf  23970  cnextfvval  24001  cnextf  24002  cnextcn  24003  ustelimasn  24159  trust  24166  restutop  24174  ustuqtop2  24179  utop2nei  24187  ucncn  24221  trcfilu  24230  cnextucn  24239  met1stc  24458  metustexhalf  24493  cfilucfil  24496  psmetutop  24504  nmoix  24666  nmoeq0  24673  idnghm  24680  blcvx  24735  xrsxmet  24747  iccntr  24759  icccmp  24763  iihalf1  24874  iihalf2  24877  xrhmeo  24893  cnheibor  24903  ipcau2  25184  lmmbrf  25212  iscauf  25230  cmetcaulem  25238  bcthlem4  25277  cmetcusp  25304  rrxcph  25342  minveclem4  25382  evthicc2  25411  cniccbdd  25412  ovollb2  25440  ovolunlem1a  25447  ovolunlem1  25448  voliun  25505  icombl  25515  ioombl  25516  iccvolcl  25518  ioovolcl  25521  mbfss  25597  mbfposb  25604  itg2const2  25692  itg2splitlem  25699  itg2gt0  25711  iblss2  25757  itgioo  25767  dvaddf  25895  dvmulf  25896  dvcobr  25899  dvcobrOLD  25900  dvcof  25902  rolle  25944  dvlip  25948  c1lip1  25952  dvivthlem1  25963  lhop1lem  25968  dvfsumlem1  25982  ftc1lem4  25996  ftc1lem5  25997  ply1divmo  26091  coe1termlem  26213  plydiveu  26256  taylplem1  26320  pserulm  26381  abelth  26401  abscxp2  26652  abscxpbnd  26713  logbgt0b  26753  ang180lem2  26770  ang180lem3  26771  isosctrlem1  26778  angpieqvd  26791  atandmtan  26880  birthdaylem3  26913  wilthlem2  27029  wilthimp  27032  isppw  27074  isppw2  27075  dvdsflsumcom  27148  chteq0  27170  perfectlem2  27191  dchrval  27195  dchrinvcl  27214  dchrptlem1  27225  bposlem3  27247  lgslem4  27261  lgsmod  27284  lgsdilem  27285  lgsdir2lem2  27287  lgsdir2  27291  lgsne0  27296  lgsmulsqcoprm  27304  lgseisenlem1  27336  2lgsoddprm  27377  2sqlem4  27382  chpo1ubb  27442  dchrisumn0  27482  pntrsumbnd2  27528  ostthlem1  27588  ostth3  27599  nosupbnd2lem1  27677  noinfbnd2lem1  27692  nocvxmin  27740  eqscut2  27768  sltlpss  27862  madefi  27867  absslt  28190  peano5uzs  28307  idmot  28462  tgelrnln  28555  lmimid  28719  lmiisolem  28721  hypcgrlem1  28724  brcgr  28825  colinearalglem4  28834  colinearalg  28835  axlowdimlem14  28880  axcontlem4  28892  cplgrop  29362  lfgriswlk  29614  pthdlem1  29694  crctcshwlkn0  29749  elwspths2on  29888  clwlkclwwlklem2fv2  29923  frgrncvvdeqlem9  30234  nvss  30520  sspn  30663  nmoub3i  30700  nmblolbii  30726  blocnilem  30731  minvecolem4  30807  htthlem  30844  norm1  31176  norm1exi  31177  pjeq  31326  axpjpj  31347  normcan  31503  pjoi0  31644  nmopub2tALT  31836  nmfnleub2  31853  eighmorth  31891  nmbdoplbi  31951  nmcoplbi  31955  nmophmi  31958  nmbdfnlbi  31976  nmcfnlbi  31979  riesz3i  31989  cnlnadjlem7  32000  branmfn  32032  nmopleid  32066  hstle  32157  superpos  32281  cvexchlem  32295  foresf1o  32431  elabreximd  32437  prssad  32456  prssbd  32457  unidifsnne  32463  tpssad  32466  f1o3d  32551  fmptco1f1o  32557  funcnvmpt  32591  fgreu  32596  suppovss  32604  elsuppfnd  32605  fsupprnfi  32615  resf1o  32653  fpwrelmap  32656  argcj  32672  xrofsup  32690  eliccelico  32700  elicoelioo  32701  iocinif  32704  difioo  32705  hashpss  32734  hashne0  32735  elq2  32736  oexpled  32772  indf1ofs  32789  eliccioo  32851  cshf1o  32884  mgcmnt1d  32923  mgcmnt2d  32924  pwrssmgc  32926  chnind  32937  chnub  32938  chnccats1  32941  mndlactf1o  32971  mndractf1o  32972  gsummpt2co  32988  gsumhashmul  33001  submomnd  33024  symgcom  33040  symgcom2  33041  odpmco  33043  pmtrcnel  33046  pmtridf1o  33051  cycpmco2lem6  33088  cycpmco2lem7  33089  cycpmco2  33090  cyc3co2  33097  cycpmconjv  33099  tocyccntz  33101  cyc3evpm  33107  cycpmconjslem2  33112  cycpmconjs  33113  archirngz  33133  unitnz  33180  elrgspnlem1  33183  elrgspnlem2  33184  elrgspnlem4  33186  elrgspnsubrun  33190  rloccring  33211  rlocf1  33214  domnpropd  33217  rrgsubm  33224  isdrng4  33235  sdrgdvcl  33239  sdrginvcl  33240  fracfld  33248  ornglmullt  33275  orngrmullt  33276  lindssn  33339  linds2eq  33342  dvdsrspss  33348  nsgqusf1olem1  33374  nsgqusf1olem3  33376  unitpidl1  33385  elrspunidl  33389  rhmimaidl  33393  drngidlhash  33395  prmidl2  33402  prmidl0  33411  qsidomlem1  33413  ssdifidlprm  33419  mxidlirredi  33432  mxidlirred  33433  ssmxidl  33435  drng0mxidl  33437  opprmxidlabs  33448  qsdrngilem  33455  qsdrngi  33456  qsdrng  33458  rsprprmprmidl  33483  rsprprmprmidlb  33484  rprmasso2  33487  rprmirredlem  33491  rprmirredb  33493  1arithidomlem2  33497  1arithufdlem4  33508  1arithufd  33509  ressply1evls1  33524  ply1asclunit  33533  ply1dg1rt  33538  ply1mulrtss  33540  ply1dg3rt0irred  33541  ply1degltlss  33552  ply1gsumz  33554  lsssra  33574  exsslsb  33582  lbslsat  33602  lindsunlem  33610  lindsun  33611  dimkerim  33613  fedgmullem1  33615  fedgmullem2  33616  fedgmul  33617  dimlssid  33618  lvecendof1f1o  33619  assalactf1o  33621  sdrgfldext  33638  fldsdrgfldext  33649  fldgenfldext  33655  evls1fldgencl  33657  fldextrspunlsp  33661  fldextrspunlem1  33662  fldextrspunfld  33663  irngss  33674  0ringirng  33676  irngnzply1  33678  irngnminplynz  33692  minplyelirng  33695  irredminply  33696  algextdeglem2  33698  algextdeglem4  33700  constrconj  33725  constrextdg2lem  33728  constrext2chnlem  33730  iconstr  33746  constrsdrg  33755  cos9thpiminplylem1  33762  cos9thpiminplylem2  33763  cos9thpiminplylem3  33764  cos9thpiminplylem5  33766  madjusmdetlem2  33805  qtophaus  33813  locfinreflem  33817  zarclssn  33850  zarmxt1  33857  zarcmplem  33858  rhmpreimacn  33862  unitdivcld  33878  tpr2rico  33889  ordtrestNEW  33898  lmxrge0  33929  elzrhunit  33954  qqhf  33963  gsumesum  34036  esumfsup  34047  esumcvg  34063  issgon  34100  sigainb  34113  insiga  34114  isrnmeas  34177  measvunilem  34189  volmeas  34208  ddeval1  34211  ddeval0  34212  imambfm  34240  omssubadd  34278  carsgclctunlem3  34298  eulerpartlemf  34348  eulerpartlemgvv  34354  probun  34397  dstfrvunirn  34453  plymulx  34526  signslema  34540  signstfvn  34547  signsvtn0  34548  signstfvneq0  34550  signstres  34553  signstfveq0a  34554  breprexplemc  34610  logdivsqrle  34628  hgt750lemg  34632  tgoldbachgtda  34639  tgoldbachgt  34641  lpadmax  34660  lpadleft  34661  lpadright  34662  bnj529  34718  bnj548  34874  bnj570  34882  bnj852  34898  bnj929  34913  bnj1097  34958  bnj1118  34961  bnj1145  34970  funen1cnv  35065  spthcycl  35097  acycgr0v  35116  derangen  35140  subfacp1lem2b  35149  subfacp1lem4  35151  subfacp1lem5  35152  derangfmla  35158  ptpconn  35201  mppspstlem  35539  wsuclem  35789  colinearex  36024  btwnconn1lem11  36061  btwnconn1lem12  36062  fwddifnp1  36129  nn0prpwlem  36286  bj-snmoore  37077  bj-imdiridlem  37149  relowlpssretop  37328  fin2so  37577  matunitlindflem2  37587  ptrecube  37590  poimirlem8  37598  poimirlem13  37603  poimirlem15  37605  poimirlem24  37614  poimirlem25  37615  poimirlem26  37616  heicant  37625  mblfinlem2  37628  voliunnfl  37634  mbfresfi  37636  itg2addnclem  37641  itg2addnclem3  37643  itg2gt0cn  37645  ftc1cnnclem  37661  ftc1anclem5  37667  cover2  37685  indexdom  37704  sdclem1  37713  fdc  37715  equivbnd2  37762  heiborlem8  37788  heibor  37791  isdrngo2  37928  iscringd  37968  smprngopr  38022  prnc  38037  eqbrtr  38196  eqeltr  38198  islfld  39026  lkrshpor  39071  lfl1dim  39085  lfl1dim2N  39086  cmtcomlemN  39212  2lplnmN  39524  pmapjat1  39818  trlnid  40144  tendoex  40940  dia1dimid  41028  dibval2  41109  dihmeetlem2N  41264  dochlkr  41350  mapdcv  41625  hdmaplkr  41878  hdmapip0  41880  hlhillcs  41923  aks6d1c6lem4  42132  dvdsexpnn  42329  readvrec  42352  frlmvscadiccat  42476  psrmnd  42515  nacsfix  42682  3rexfrabdioph  42767  4rexfrabdioph  42768  6rexfrabdioph  42769  7rexfrabdioph  42770  eldioph4b  42781  pellexlem2  42800  pellexlem5  42803  jm2.26lem3  42972  numinfctb  43074  ordne0gt0  43232  omge1  43268  omlim2  43270  omord2lim  43271  omord2i  43272  tfsconcatfv  43312  tfsconcatb0  43315  oaun3lem1  43345  ntrclsfv1  44026  ntrneifv1  44050  ntrneifv2  44051  cvgdvgrat  44285  radcnvrat  44286  dvconstbi  44306  bccbc  44317  elpwgded  44537  elpwgdedVD  44889  sspwimpcf  44892  sspwimpcfVD  44893  sspwimpALT2  44900  ax6e2ndeqALT  44903  eliuniin  45071  eliuniin2  45092  qinioo  45512  dfxlim2v  45824  xlimliminflimsup  45839  cncfiooicclem1  45870  ibliooicc  45948  stoweidlem27  46004  stoweidlem28  46005  fourierdlem89  46172  fourierdlem91  46174  fourierdlem92  46175  smflimmpt  46787  odz2prm2pw  47525  perfectALTVlem2  47684  blen1b  48516  naryfvalelfv  48560  itscnhlc0yqe  48687  itsclquadb  48704  lubeldm2  48878  glbeldm2  48879  ipolub  48910  ipoglb  48913  fucofulem1  49169  functhinclem1  49278  thincciso  49287  prsthinc  49298  functermclem  49340  prstchom2ALT  49389  onetansqsecsq  49573  cotsqcscsq  49574  aacllem  49613