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  805  exbiri  811  biadanid  823  oplem1  1056  eqtr  2757  pm13.181  3020  opabss  5211  axprlem4OLD  5434  axprlem5OLD  5435  euotd  5522  brcogw  5881  somin1  6155  xpdifid  6189  funfni  6674  fnssres  6691  fn0  6699  fnimadisj  6700  fnimaeq0  6701  foimacnv  6865  fvelimab  6980  dffv2  7003  fvopab3ig  7011  dff3  7119  dffo4  7122  fpr2g  7230  ralima  7256  f1eqcocnv  7320  isomin  7356  f1ocnv2d  7685  fnexALT  7973  xp1st  8044  xp2nd  8045  frrlem3  8311  fpr2  8327  wfr3g  8345  wfrlem3OLD  8348  wfrlem4OLD  8350  wfr2  8374  iinon  8378  tfr3  8437  oawordri  8586  oaass  8597  omeulem1  8618  oeoa  8633  oeoe  8635  oeeulem  8637  ecelqsg  8810  elqsn0  8824  pwdom  9167  enfii  9223  phpeqd  9249  ominf  9291  findcard3  9315  marypha1lem  9470  wofib  9582  cantnff  9711  cantnfp1  9718  cantnf  9730  cnfcomlem  9736  ttrcltr  9753  frr3g  9793  r1sscl  9822  rankval3b  9863  infxpidm2  10054  numdom  10075  onssnum  10077  acni  10082  acni2  10083  dfac5  10166  djulepw  10230  infunsdom1  10249  infunsdom  10250  cofsmo  10306  cfsmolem  10307  fin1ai  10330  fin2i  10332  isf34lem1  10409  fin67  10432  itunisuc  10456  axdc3lem4  10490  zornn0g  10542  ttukeylem6  10551  brdom3  10565  tsken  10791  tskcard  10818  r1tskina  10819  intgru  10851  prlem934  11070  ltexprlem7  11079  supaddc  12232  mul2lt0rlt0  13134  xrmaxeq  13217  xrmineq  13218  xmulneg1  13307  ixxun  13399  difelfzle  13677  ssfzoulel  13795  elfznelfzo  13807  ico01fl0  13855  btwnzge0  13864  ltdifltdiv  13870  ioopnfsup  13900  icopnfsup  13901  modifeq2int  13970  suppssfz  14031  expmordi  14203  zzlesq  14241  faclbnd4lem4  14331  hasheni  14383  hashgt0  14423  hashge1  14424  hashprb  14432  lennncl  14568  wrdsymb0  14583  ccatsymb  14616  ccatlid  14620  ccatass  14622  ccatswrd  14702  swrdccat2  14703  ccatpfx  14735  swrdccatfn  14758  swrdccat  14769  revccat  14800  2cshw  14847  cnpart  15275  resqreu  15287  recval  15357  abs1m  15370  abslem2  15374  fzomaxdiflem  15377  sqreulem  15394  sqreu  15395  limsupgre  15513  rlimdiv  15678  fsumparts  15838  climcnds  15883  expcnv  15896  ntrivcvg  15929  mod2eq1n2dvds  16380  ndvdssub  16442  sadcaddlem  16490  rplpwr  16591  dvdssqlem  16599  algcvgblem  16610  eucalgcvga  16619  isprm2lem  16714  powm2modprm  16836  coprimeprodsq  16841  pythagtriplem11  16858  pythagtriplem13  16860  pcadd2  16923  4sqlem11  16988  vdwlem6  17019  vdwlem8  17021  vdwlem10  17023  ramval  17041  ramcl2  17049  ramlb  17052  ram0  17055  mreintcl  17639  mrcval  17654  mrccl  17655  mrcuni  17665  mrcun  17666  acsfiel  17698  rescabs  17882  rescabsOLD  17883  funcres  17946  setcmon  18140  setcepi  18141  fullestrcsetc  18206  funcsetcestrclem8  18217  fullsetcestrc  18221  yonffthlem  18338  pleval2i  18393  pospo  18402  poslubdg  18471  acsdrsel  18600  acsdrscl  18603  acsficl  18604  psss  18637  grpidd  18696  ismndd  18781  gsumsgrpccat  18865  gsumwmhm  18870  mulgaddcom  19128  subgmulg  19170  resghm  19262  conjnsg  19284  ghmqusker  19317  f1otrspeq  19479  pmtrval  19483  pmtrrn  19489  pmtrfinv  19493  pmtrprfval  19519  psgnunilem1  19525  psgnunilem5  19526  psgnunilem4  19529  psgneldm2i  19537  lsmelvalix  19673  pj1ghm  19735  efgredlemc  19777  frgp0  19792  qusabl  19897  cycsubgcyg  19933  gsumval3  19939  gsumcllem  19940  ablfac1c  20105  pgpfac1lem5  20113  isrngd  20190  isringd  20304  01eq0ring  20546  lspsneq0b  21028  lmodindp1  21029  lmhmf1o  21062  lmhmpreima  21064  reslmhm  21068  pwssplit3  21077  lspsncmp  21135  lspsneq  21141  znf1o  21587  dsmmlss  21781  frlmlbs  21834  frlmup1  21835  psrgrp  21993  mpfind  22148  psdmul  22187  ply1scleq  22324  mat1  22468  chfacfisf  22875  chfacfisfcpmat  22876  uniopn  22918  ntrval  23059  clsval  23060  neival  23125  neiptopreu  23156  lpval  23162  restdis  23201  lmbrf  23283  cnpnei  23287  1stcrest  23476  hauspwdom  23524  lfinpfin  23547  txcnpi  23631  ptrescn  23662  xkococnlem  23682  qtopeu  23739  kqreglem1  23764  ptuncnv  23830  filss  23876  fsubbas  23890  fbasrn  23907  cfinfil  23916  ufinffr  23952  elfm3  23973  rnelfmlem  23975  rnelfm  23976  flimclslem  24007  flfval  24013  isfcf  24057  cnextfvval  24088  cnextf  24089  cnextcn  24090  ustelimasn  24246  trust  24253  restutop  24261  ustuqtop2  24266  utop2nei  24274  ucncn  24309  trcfilu  24318  cnextucn  24327  met1stc  24549  metustexhalf  24584  cfilucfil  24587  psmetutop  24595  nmoix  24765  nmoeq0  24772  idnghm  24779  blcvx  24833  xrsxmet  24844  iccntr  24856  icccmp  24860  iihalf1  24971  iihalf2  24974  xrhmeo  24990  cnheibor  25000  ipcau2  25281  lmmbrf  25309  iscauf  25327  cmetcaulem  25335  bcthlem4  25374  cmetcusp  25401  rrxcph  25439  minveclem4  25479  evthicc2  25508  cniccbdd  25509  ovollb2  25537  ovolunlem1a  25544  ovolunlem1  25545  voliun  25602  icombl  25612  ioombl  25613  iccvolcl  25615  ioovolcl  25618  mbfss  25694  mbfposb  25701  itg2const2  25790  itg2splitlem  25797  itg2gt0  25809  iblss2  25855  itgioo  25865  dvaddf  25993  dvmulf  25994  dvcobr  25997  dvcobrOLD  25998  dvcof  26000  rolle  26042  dvlip  26046  c1lip1  26050  dvivthlem1  26061  lhop1lem  26066  dvfsumlem1  26080  ftc1lem4  26094  ftc1lem5  26095  ply1divmo  26189  coe1termlem  26311  plydiveu  26354  taylplem1  26418  pserulm  26479  abelth  26499  abscxp2  26749  abscxpbnd  26810  logbgt0b  26850  ang180lem2  26867  ang180lem3  26868  isosctrlem1  26875  angpieqvd  26888  atandmtan  26977  birthdaylem3  27010  wilthlem2  27126  wilthimp  27129  isppw  27171  isppw2  27172  dvdsflsumcom  27245  chteq0  27267  perfectlem2  27288  dchrval  27292  dchrinvcl  27311  dchrptlem1  27322  bposlem3  27344  lgslem4  27358  lgsmod  27381  lgsdilem  27382  lgsdir2lem2  27384  lgsdir2  27388  lgsne0  27393  lgsmulsqcoprm  27401  lgseisenlem1  27433  2lgsoddprm  27474  2sqlem4  27479  chpo1ubb  27539  dchrisumn0  27579  pntrsumbnd2  27625  ostthlem1  27685  ostth3  27696  nosupbnd2lem1  27774  noinfbnd2lem1  27789  nocvxmin  27837  eqscut2  27865  sltlpss  27959  madefi  27964  absslt  28287  peano5uzs  28404  idmot  28559  tgelrnln  28652  lmimid  28816  lmiisolem  28818  hypcgrlem1  28821  brcgr  28929  colinearalglem4  28938  colinearalg  28939  axlowdimlem14  28984  axcontlem4  28996  cplgrop  29468  lfgriswlk  29720  pthdlem1  29798  crctcshwlkn0  29850  elwspths2on  29989  clwlkclwwlklem2fv2  30024  frgrncvvdeqlem9  30335  nvss  30621  sspn  30764  nmoub3i  30801  nmblolbii  30827  blocnilem  30832  minvecolem4  30908  htthlem  30945  norm1  31277  norm1exi  31278  pjeq  31427  axpjpj  31448  normcan  31604  pjoi0  31745  nmopub2tALT  31937  nmfnleub2  31954  eighmorth  31992  nmbdoplbi  32052  nmcoplbi  32056  nmophmi  32059  nmbdfnlbi  32077  nmcfnlbi  32080  riesz3i  32090  cnlnadjlem7  32101  branmfn  32133  nmopleid  32167  hstle  32258  superpos  32382  cvexchlem  32396  bibiad  32485  foresf1o  32531  elabreximd  32537  unidifsnne  32561  f1o3d  32643  fmptco1f1o  32649  funcnvmpt  32683  fgreu  32688  suppovss  32695  elsuppfnd  32696  fsupprnfi  32706  resf1o  32747  fpwrelmap  32750  xrofsup  32777  eliccelico  32785  elicoelioo  32786  iocinif  32789  difioo  32790  eliccioo  32897  cshf1o  32931  mgcmnt1d  32971  mgcmnt2d  32972  pwrssmgc  32974  chnind  32984  chnub  32985  mndlactf1o  33017  mndractf1o  33018  gsummpt2co  33033  gsumhashmul  33046  submomnd  33069  symgcom  33085  symgcom2  33086  odpmco  33088  pmtrcnel  33091  pmtridf1o  33096  cycpmco2lem6  33133  cycpmco2lem7  33134  cycpmco2  33135  cyc3co2  33142  cycpmconjv  33144  tocyccntz  33146  cyc3evpm  33152  cycpmconjslem2  33157  cycpmconjs  33158  archirngz  33178  unitnz  33228  elrgspnlem1  33231  elrgspnlem2  33232  elrgspnlem4  33234  rloccring  33256  rlocf1  33259  rrgsubm  33267  isdrng4  33278  sdrgdvcl  33280  sdrginvcl  33281  fracfld  33289  ornglmullt  33316  orngrmullt  33317  lindssn  33385  linds2eq  33388  dvdsrspss  33394  nsgqusf1olem1  33420  nsgqusf1olem3  33422  unitpidl1  33431  elrspunidl  33435  rhmimaidl  33439  drngidlhash  33441  prmidl2  33448  prmidl0  33457  qsidomlem1  33459  ssdifidlprm  33465  mxidlirredi  33478  mxidlirred  33479  ssmxidl  33481  drng0mxidl  33483  opprmxidlabs  33494  qsdrngilem  33501  qsdrngi  33502  qsdrng  33504  rsprprmprmidl  33529  rsprprmprmidlb  33530  rprmasso2  33533  rprmirredlem  33537  rprmirredb  33539  1arithidomlem2  33543  1arithufdlem4  33554  1arithufd  33555  ply1asclunit  33578  ply1dg1rt  33583  ply1mulrtss  33585  ply1dg3rt0irred  33586  ply1degltlss  33596  ply1gsumz  33598  lsssra  33617  lbslsat  33643  lindsunlem  33651  lindsun  33652  dimkerim  33654  fedgmullem1  33656  fedgmullem2  33657  fedgmul  33658  dimlssid  33659  lvecendof1f1o  33660  assalactf1o  33662  fldgenfldext  33692  evls1fldgencl  33694  irngss  33701  0ringirng  33703  irngnzply1  33705  irngnminplynz  33719  irredminply  33721  algextdeglem2  33723  algextdeglem4  33725  constrconj  33749  madjusmdetlem2  33788  qtophaus  33796  locfinreflem  33800  zarclssn  33833  zarmxt1  33840  zarcmplem  33841  rhmpreimacn  33845  unitdivcld  33861  tpr2rico  33872  ordtrestNEW  33881  lmxrge0  33912  elzrhunit  33939  qqhf  33948  indf1ofs  34006  gsumesum  34039  esumfsup  34050  esumcvg  34066  issgon  34103  sigainb  34116  insiga  34117  isrnmeas  34180  measvunilem  34192  volmeas  34211  ddeval1  34214  ddeval0  34215  imambfm  34243  omssubadd  34281  carsgclctunlem3  34301  eulerpartlemf  34351  eulerpartlemgvv  34357  probun  34400  dstfrvunirn  34455  plymulx  34541  signslema  34555  signstfvn  34562  signsvtn0  34563  signstfvneq0  34565  signstres  34568  signstfveq0a  34569  breprexplemc  34625  logdivsqrle  34643  hgt750lemg  34647  tgoldbachgtda  34654  tgoldbachgt  34656  lpadmax  34675  lpadleft  34676  lpadright  34677  bnj529  34733  bnj548  34889  bnj570  34897  bnj852  34913  bnj929  34928  bnj1097  34973  bnj1118  34976  bnj1145  34985  funen1cnv  35080  spthcycl  35113  acycgr0v  35132  derangen  35156  subfacp1lem2b  35165  subfacp1lem4  35167  subfacp1lem5  35168  derangfmla  35174  ptpconn  35217  mppspstlem  35555  wsuclem  35806  colinearex  36041  btwnconn1lem11  36078  btwnconn1lem12  36079  fwddifnp1  36146  nn0prpwlem  36304  bj-snmoore  37095  bj-imdiridlem  37167  relowlpssretop  37346  fin2so  37593  matunitlindflem2  37603  ptrecube  37606  poimirlem8  37614  poimirlem13  37619  poimirlem15  37621  poimirlem24  37630  poimirlem25  37631  poimirlem26  37632  heicant  37641  mblfinlem2  37644  voliunnfl  37650  mbfresfi  37652  itg2addnclem  37657  itg2addnclem3  37659  itg2gt0cn  37661  ftc1cnnclem  37677  ftc1anclem5  37683  cover2  37701  indexdom  37720  sdclem1  37729  fdc  37731  equivbnd2  37778  heiborlem8  37804  heibor  37807  isdrngo2  37944  iscringd  37984  smprngopr  38038  prnc  38053  eqbrtr  38212  eqeltr  38214  islfld  39043  lkrshpor  39088  lfl1dim  39102  lfl1dim2N  39103  cmtcomlemN  39229  2lplnmN  39541  pmapjat1  39835  trlnid  40161  tendoex  40957  dia1dimid  41045  dibval2  41126  dihmeetlem2N  41281  dochlkr  41367  mapdcv  41642  hdmaplkr  41895  hdmapip0  41897  hlhillcs  41944  aks6d1c6lem4  42154  dvdsexpnn  42346  readvrec  42370  frlmvscadiccat  42492  psrmnd  42531  nacsfix  42699  3rexfrabdioph  42784  4rexfrabdioph  42785  6rexfrabdioph  42786  7rexfrabdioph  42787  eldioph4b  42798  pellexlem2  42817  pellexlem5  42820  jm2.26lem3  42989  numinfctb  43091  ordne0gt0  43250  omge1  43286  omlim2  43288  omord2lim  43289  omord2i  43290  tfsconcatfv  43330  tfsconcatb0  43333  oaun3lem1  43363  ntrclsfv1  44044  ntrneifv1  44068  ntrneifv2  44069  cvgdvgrat  44308  radcnvrat  44309  dvconstbi  44329  bccbc  44340  elpwgded  44561  elpwgdedVD  44914  sspwimpcf  44917  sspwimpcfVD  44918  sspwimpALT2  44925  ax6e2ndeqALT  44928  eliuniin  45038  eliuniin2  45059  qinioo  45487  dfxlim2v  45802  xlimliminflimsup  45817  cncfiooicclem1  45848  ibliooicc  45926  stoweidlem27  45982  stoweidlem28  45983  fourierdlem89  46150  fourierdlem91  46152  fourierdlem92  46153  smflimmpt  46765  odz2prm2pw  47487  perfectALTVlem2  47646  blen1b  48437  naryfvalelfv  48481  itscnhlc0yqe  48608  itsclquadb  48625  lubeldm2  48752  glbeldm2  48753  ipolub  48776  ipoglb  48779  functhinclem1  48840  thincciso  48848  prsthinc  48854  prstchom2ALT  48879  onetansqsecsq  48991  cotsqcscsq  48992  aacllem  49031