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  2756  pm13.181  3014  opabss  5162  axprlem4OLD  5374  axprlem5OLD  5375  euotd  5461  brcogw  5817  somin1  6090  xpdifid  6126  funfni  6598  fnssres  6615  fn0  6623  fnimadisj  6624  fnimaeq0  6625  foimacnv  6791  fvelimab  6906  dffv2  6929  fvopab3ig  6937  dff3  7045  dffo4  7048  fpr2g  7157  ralima  7183  f1eqcocnv  7247  isomin  7283  f1ocnv2d  7611  fnexALT  7895  xp1st  7965  xp2nd  7966  frrlem3  8230  fpr2  8246  wfr3g  8261  wfr2  8269  iinon  8272  tfr3  8330  oawordri  8477  oaass  8488  omeulem1  8509  oeoa  8525  oeoe  8527  oeeulem  8529  elqsn0  8721  pwdom  9057  enfii  9110  phpeqd  9136  ominf  9164  findcard3  9183  marypha1lem  9336  wofib  9450  cantnff  9583  cantnfp1  9590  cantnf  9602  cnfcomlem  9608  ttrcltr  9625  frr3g  9668  r1sscl  9697  rankval3b  9738  infxpidm2  9927  numdom  9948  onssnum  9950  acni  9955  acni2  9956  dfac5  10039  djulepw  10103  infunsdom1  10122  infunsdom  10123  cofsmo  10179  cfsmolem  10180  fin1ai  10203  fin2i  10205  isf34lem1  10282  fin67  10305  itunisuc  10329  axdc3lem4  10363  zornn0g  10415  ttukeylem6  10424  brdom3  10438  tsken  10665  tskcard  10692  r1tskina  10693  intgru  10725  prlem934  10944  ltexprlem7  10953  supaddc  12109  mul2lt0rlt0  13009  xrmaxeq  13094  xrmineq  13095  xmulneg1  13184  ixxun  13277  difelfzle  13557  ssfzoulel  13676  elfznelfzo  13689  ico01fl0  13739  btwnzge0  13748  ltdifltdiv  13754  ioopnfsup  13784  icopnfsup  13785  modifeq2int  13856  suppssfz  13917  expmordi  14090  zzlesq  14129  faclbnd4lem4  14219  hasheni  14271  hashgt0  14311  hashge1  14312  hashprb  14320  lennncl  14457  wrdsymb0  14472  ccatsymb  14506  ccatlid  14510  ccatass  14512  ccatswrd  14592  swrdccat2  14593  ccatpfx  14624  swrdccatfn  14647  swrdccat  14658  revccat  14689  2cshw  14736  cnpart  15163  resqreu  15175  recval  15246  abs1m  15259  abslem2  15263  fzomaxdiflem  15266  sqreulem  15283  sqreu  15284  limsupgre  15404  rlimdiv  15569  fsumparts  15729  climcnds  15774  expcnv  15787  ntrivcvg  15820  mod2eq1n2dvds  16274  ndvdssub  16336  sadcaddlem  16384  rplpwr  16485  dvdssqlem  16493  algcvgblem  16504  eucalgcvga  16513  isprm2lem  16608  powm2modprm  16731  coprimeprodsq  16736  pythagtriplem11  16753  pythagtriplem13  16755  pcadd2  16818  4sqlem11  16883  vdwlem6  16914  vdwlem8  16916  vdwlem10  16918  ramval  16936  ramcl2  16944  ramlb  16947  ram0  16950  mreintcl  17514  mrcval  17533  mrccl  17534  mrcuni  17544  mrcun  17545  acsfiel  17577  rescabs  17757  funcres  17820  setcmon  18011  setcepi  18012  fullestrcsetc  18074  funcsetcestrclem8  18085  fullsetcestrc  18089  yonffthlem  18205  pleval2i  18257  pospo  18266  poslubdg  18335  acsdrsel  18466  acsdrscl  18469  acsficl  18470  psss  18503  chnind  18544  chnub  18545  chnccats1  18548  chnccat  18549  grpidd  18596  ismndd  18681  gsumsgrpccat  18765  gsumwmhm  18770  mulgaddcom  19028  subgmulg  19070  resghm  19161  conjnsg  19183  ghmqusker  19216  f1otrspeq  19376  pmtrval  19380  pmtrrn  19386  pmtrfinv  19390  pmtrprfval  19416  psgnunilem1  19422  psgnunilem5  19423  psgnunilem4  19426  psgneldm2i  19434  lsmelvalix  19570  pj1ghm  19632  efgredlemc  19674  frgp0  19689  qusabl  19794  cycsubgcyg  19830  gsumval3  19836  gsumcllem  19837  ablfac1c  20002  pgpfac1lem5  20010  submomnd  20061  isrngd  20108  isringd  20226  01eq0ring  20463  ornglmullt  20802  orngrmullt  20803  lspsneq0b  20964  lmodindp1  20965  lmhmf1o  20998  lmhmpreima  21000  reslmhm  21004  pwssplit3  21013  lspsncmp  21071  lspsneq  21077  znf1o  21506  dsmmlss  21699  frlmlbs  21752  frlmup1  21753  psrgrp  21912  mpfind  22070  psdmul  22109  ply1scleq  22249  mat1  22391  chfacfisf  22798  chfacfisfcpmat  22799  uniopn  22841  ntrval  22980  clsval  22981  neival  23046  neiptopreu  23077  lpval  23083  restdis  23122  lmbrf  23204  cnpnei  23208  1stcrest  23397  hauspwdom  23445  lfinpfin  23468  txcnpi  23552  ptrescn  23583  xkococnlem  23603  qtopeu  23660  kqreglem1  23685  ptuncnv  23751  filss  23797  fsubbas  23811  fbasrn  23828  cfinfil  23837  ufinffr  23873  elfm3  23894  rnelfmlem  23896  rnelfm  23897  flimclslem  23928  flfval  23934  isfcf  23978  cnextfvval  24009  cnextf  24010  cnextcn  24011  ustelimasn  24167  trust  24173  restutop  24181  ustuqtop2  24186  utop2nei  24194  ucncn  24228  trcfilu  24237  cnextucn  24246  met1stc  24465  metustexhalf  24500  cfilucfil  24503  psmetutop  24511  nmoix  24673  nmoeq0  24680  idnghm  24687  blcvx  24742  xrsxmet  24754  iccntr  24766  icccmp  24770  iihalf1  24881  iihalf2  24884  xrhmeo  24900  cnheibor  24910  ipcau2  25190  lmmbrf  25218  iscauf  25236  cmetcaulem  25244  bcthlem4  25283  cmetcusp  25310  rrxcph  25348  minveclem4  25388  evthicc2  25417  cniccbdd  25418  ovollb2  25446  ovolunlem1a  25453  ovolunlem1  25454  voliun  25511  icombl  25521  ioombl  25522  iccvolcl  25524  ioovolcl  25527  mbfss  25603  mbfposb  25610  itg2const2  25698  itg2splitlem  25705  itg2gt0  25717  iblss2  25763  itgioo  25773  dvaddf  25901  dvmulf  25902  dvcobr  25905  dvcobrOLD  25906  dvcof  25908  rolle  25950  dvlip  25954  c1lip1  25958  dvivthlem1  25969  lhop1lem  25974  dvfsumlem1  25988  ftc1lem4  26002  ftc1lem5  26003  ply1divmo  26097  coe1termlem  26219  plydiveu  26262  taylplem1  26326  pserulm  26387  abelth  26407  abscxp2  26658  abscxpbnd  26719  logbgt0b  26759  ang180lem2  26776  ang180lem3  26777  isosctrlem1  26784  angpieqvd  26797  atandmtan  26886  birthdaylem3  26919  wilthlem2  27035  wilthimp  27038  isppw  27080  isppw2  27081  dvdsflsumcom  27154  chteq0  27176  perfectlem2  27197  dchrval  27201  dchrinvcl  27220  dchrptlem1  27231  bposlem3  27253  lgslem4  27267  lgsmod  27290  lgsdilem  27291  lgsdir2lem2  27293  lgsdir2  27297  lgsne0  27302  lgsmulsqcoprm  27310  lgseisenlem1  27342  2lgsoddprm  27383  2sqlem4  27388  chpo1ubb  27448  dchrisumn0  27488  pntrsumbnd2  27534  ostthlem1  27594  ostth3  27605  nosupbnd2lem1  27683  noinfbnd2lem1  27698  nocvxmin  27751  eqcuts2  27782  ltslpss  27904  madefi  27909  abslts  28245  eucliddivs  28372  peano5uzs  28400  z12bdaylem1  28466  elreno2  28491  idmot  28609  tgelrnln  28702  lmimid  28866  lmiisolem  28868  hypcgrlem1  28871  brcgr  28973  colinearalglem4  28982  colinearalg  28983  axlowdimlem14  29028  axcontlem4  29040  cplgrop  29510  lfgriswlk  29760  pthdlem1  29839  crctcshwlkn0  29894  elwspths2on  30035  elwspths2onw  30036  clwlkclwwlklem2fv2  30071  frgrncvvdeqlem9  30382  nvss  30668  sspn  30811  nmoub3i  30848  nmblolbii  30874  blocnilem  30879  minvecolem4  30955  htthlem  30992  norm1  31324  norm1exi  31325  pjeq  31474  axpjpj  31495  normcan  31651  pjoi0  31792  nmopub2tALT  31984  nmfnleub2  32001  eighmorth  32039  nmbdoplbi  32099  nmcoplbi  32103  nmophmi  32106  nmbdfnlbi  32124  nmcfnlbi  32127  riesz3i  32137  cnlnadjlem7  32148  branmfn  32180  nmopleid  32214  hstle  32305  superpos  32429  cvexchlem  32443  foresf1o  32579  elabreximd  32585  prssad  32604  prssbd  32605  unidifsnne  32611  tpssad  32614  fresunsn  32703  f1o3d  32704  fmptco1f1o  32711  funcnvmpt  32745  fgreu  32750  suppovss  32760  elsuppfnd  32761  fsupprnfi  32771  resf1o  32809  fpwrelmap  32812  argcj  32828  xrofsup  32847  eliccelico  32857  elicoelioo  32858  iocinif  32861  difioo  32862  hashpss  32889  hashne0  32890  elq2  32892  oexpled  32928  indf1ofs  32948  eliccioo  33012  cshf1o  33044  mgcmnt1d  33079  mgcmnt2d  33080  pwrssmgc  33082  mndlactf1o  33112  mndractf1o  33113  gsummpt2co  33131  gsumhashmul  33150  gsummulsubdishift1  33151  symgcom  33165  symgcom2  33166  odpmco  33168  pmtrcnel  33171  pmtridf1o  33176  cycpmco2lem6  33213  cycpmco2lem7  33214  cycpmco2  33215  cyc3co2  33222  cycpmconjv  33224  tocyccntz  33226  cyc3evpm  33232  cycpmconjslem2  33237  cycpmconjs  33238  fxpsubm  33254  fxpsubg  33255  fxpsubrg  33256  fxpsdrg  33257  archirngz  33271  unitnz  33321  elrgspnlem1  33324  elrgspnlem2  33325  elrgspnlem4  33327  elrgspnsubrun  33331  rloccring  33352  rlocf1  33355  domnpropd  33359  rrgsubm  33366  isdrng4  33377  sdrgdvcl  33381  sdrginvcl  33382  fracfld  33390  lindssn  33459  linds2eq  33462  dvdsrspss  33468  nsgqusf1olem1  33494  nsgqusf1olem3  33496  unitpidl1  33505  elrspunidl  33509  rhmimaidl  33513  drngidlhash  33515  prmidl2  33522  prmidl0  33531  qsidomlem1  33533  ssdifidlprm  33539  mxidlirredi  33552  mxidlirred  33553  ssmxidl  33555  drng0mxidl  33557  opprmxidlabs  33568  qsdrngilem  33575  qsdrngi  33576  qsdrng  33578  rsprprmprmidl  33603  rsprprmprmidlb  33604  rprmasso2  33607  rprmirredlem  33611  rprmirredb  33613  1arithidomlem2  33617  1arithufdlem4  33628  1arithufd  33629  ressply1evls1  33646  ply1asclunit  33655  ply1dg1rt  33661  ply1mulrtss  33663  ply1dg3rt0irred  33665  ply1degltlss  33677  ply1gsumz  33680  evlextv  33707  esplyfv1  33727  esplyind  33731  vietadeg1  33734  lsssra  33744  exsslsb  33753  lbslsat  33773  lindsunlem  33781  lindsun  33782  dimkerim  33784  fedgmullem1  33786  fedgmullem2  33787  fedgmul  33788  dimlssid  33789  lvecendof1f1o  33790  assalactf1o  33792  sdrgfldext  33807  fldsdrgfldext  33818  fldgenfldext  33825  evls1fldgencl  33827  fldextrspunlsp  33831  fldextrspunlem1  33832  fldextrspunfld  33833  irngss  33844  0ringirng  33846  irngnzply1  33848  extdgfialglem1  33849  irngnminplynz  33869  minplyelirng  33872  irredminply  33873  algextdeglem2  33875  algextdeglem4  33877  constrconj  33902  constrextdg2lem  33905  constrext2chnlem  33907  iconstr  33923  constrsdrg  33932  cos9thpiminplylem1  33939  cos9thpiminplylem2  33940  cos9thpiminplylem3  33941  cos9thpiminplylem5  33943  madjusmdetlem2  33985  qtophaus  33993  locfinreflem  33997  zarclssn  34030  zarmxt1  34037  zarcmplem  34038  rhmpreimacn  34042  unitdivcld  34058  tpr2rico  34069  ordtrestNEW  34078  lmxrge0  34109  elzrhunit  34134  qqhf  34143  gsumesum  34216  esumfsup  34227  esumcvg  34243  issgon  34280  sigainb  34293  insiga  34294  isrnmeas  34357  measvunilem  34369  volmeas  34388  ddeval1  34391  ddeval0  34392  imambfm  34419  omssubadd  34457  carsgclctunlem3  34477  eulerpartlemf  34527  eulerpartlemgvv  34533  probun  34576  dstfrvunirn  34632  plymulx  34705  signslema  34719  signstfvn  34726  signsvtn0  34727  signstfvneq0  34729  signstres  34732  signstfveq0a  34733  breprexplemc  34789  logdivsqrle  34807  hgt750lemg  34811  tgoldbachgtda  34818  tgoldbachgt  34820  lpadmax  34839  lpadleft  34840  lpadright  34841  bnj529  34897  bnj548  35053  bnj570  35061  bnj852  35077  bnj929  35092  bnj1097  35137  bnj1118  35140  bnj1145  35149  funen1cnv  35244  fissorduni  35246  spthcycl  35323  acycgr0v  35342  derangen  35366  subfacp1lem2b  35375  subfacp1lem4  35377  subfacp1lem5  35378  derangfmla  35384  ptpconn  35427  mppspstlem  35765  wsuclem  36017  colinearex  36254  btwnconn1lem11  36291  btwnconn1lem12  36292  fwddifnp1  36359  nn0prpwlem  36516  regsfromregtr  36668  bj-snmoore  37318  bj-imdiridlem  37390  relowlpssretop  37569  fin2so  37808  matunitlindflem2  37818  ptrecube  37821  poimirlem8  37829  poimirlem13  37834  poimirlem15  37836  poimirlem24  37845  poimirlem25  37846  poimirlem26  37847  heicant  37856  mblfinlem2  37859  voliunnfl  37865  mbfresfi  37867  itg2addnclem  37872  itg2addnclem3  37874  itg2gt0cn  37876  ftc1cnnclem  37892  ftc1anclem5  37898  cover2  37916  indexdom  37935  sdclem1  37944  fdc  37946  equivbnd2  37993  heiborlem8  38019  heibor  38022  isdrngo2  38159  iscringd  38199  smprngopr  38253  prnc  38268  eqbrtr  38434  eqeltr  38436  islfld  39332  lkrshpor  39377  lfl1dim  39391  lfl1dim2N  39392  cmtcomlemN  39518  2lplnmN  39829  pmapjat1  40123  trlnid  40449  tendoex  41245  dia1dimid  41333  dibval2  41414  dihmeetlem2N  41569  dochlkr  41655  mapdcv  41930  hdmaplkr  42183  hdmapip0  42185  hlhillcs  42228  aks6d1c6lem4  42437  dvdsexpnn  42598  readvrec  42627  frlmvscadiccat  42771  psrmnd  42808  nacsfix  42964  3rexfrabdioph  43049  4rexfrabdioph  43050  6rexfrabdioph  43051  7rexfrabdioph  43052  eldioph4b  43063  pellexlem2  43082  pellexlem5  43085  jm2.26lem3  43253  numinfctb  43355  ordne0gt0  43513  omge1  43549  omlim2  43551  omord2lim  43552  omord2i  43553  tfsconcatfv  43593  tfsconcatb0  43596  oaun3lem1  43626  ntrclsfv1  44306  ntrneifv1  44330  ntrneifv2  44331  cvgdvgrat  44564  radcnvrat  44565  dvconstbi  44585  bccbc  44596  elpwgded  44815  elpwgdedVD  45167  sspwimpcf  45170  sspwimpcfVD  45171  sspwimpALT2  45178  ax6e2ndeqALT  45181  eliuniin  45353  eliuniin2  45374  qinioo  45791  dfxlim2v  46101  xlimliminflimsup  46116  cncfiooicclem1  46147  ibliooicc  46225  stoweidlem27  46281  stoweidlem28  46282  fourierdlem89  46449  fourierdlem91  46451  fourierdlem92  46452  smflimmpt  47064  odz2prm2pw  47819  perfectALTVlem2  47978  blen1b  48844  naryfvalelfv  48888  itscnhlc0yqe  49015  itsclquadb  49032  lubeldm2  49211  glbeldm2  49212  ipolub  49243  ipoglb  49246  fucofulem1  49565  functhinclem1  49699  thincciso  49708  prsthinc  49719  functermclem  49762  prstchom2ALT  49819  onetansqsecsq  50016  cotsqcscsq  50017  aacllem  50056