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

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 397

This theorem is referenced by:  bitr  802  exbiri  808  biadanid  820  oplem1  1054  eqtr  2762  pm13.181  3027  opabss  5139  axprlem4  5350  axprlem5  5351  euotd  5428  brcogw  5780  somin1  6043  xpdifid  6076  funfni  6548  fncoOLD  6559  fnssres  6564  fn0  6573  fnimadisj  6574  fnimaeq0  6575  foimacnv  6742  fvelimab  6850  dffv2  6872  fvopab3ig  6880  dff3  6985  dffo4  6988  fpr2g  7096  f1eqcocnv  7182  f1eqcocnvOLD  7183  isomin  7217  f1ocnv2d  7531  fnexALT  7802  xp1st  7872  xp2nd  7873  frrlem3  8113  fpr2  8129  wfr3g  8147  wfrlem3OLD  8150  wfrlem4OLD  8152  wfr2  8176  iinon  8180  tfr3  8239  oawordri  8390  oaass  8401  omeulem1  8422  oeoa  8437  oeoe  8439  oeeulem  8441  ecelqsg  8570  elqsn0  8584  pwdom  8925  enfii  8981  phpeqd  9007  marypha1lem  9201  wofib  9313  cantnff  9441  cantnfp1  9448  cantnf  9460  cnfcomlem  9466  ttrcltr  9483  frr3g  9523  r1sscl  9552  rankval3b  9593  infxpidm2  9782  numdom  9803  onssnum  9805  acni  9810  acni2  9811  dfac5  9893  djulepw  9957  infunsdom1  9978  infunsdom  9979  cofsmo  10034  cfsmolem  10035  fin1ai  10058  fin2i  10060  isf34lem1  10137  fin67  10160  itunisuc  10184  axdc3lem4  10218  zornn0g  10270  ttukeylem6  10279  brdom3  10293  tsken  10519  tskcard  10546  r1tskina  10547  intgru  10579  prlem934  10798  ltexprlem7  10807  supaddc  11951  mul2lt0rlt0  12841  xrmaxeq  12922  xrmineq  12923  xmulneg1  13012  ixxun  13104  difelfzle  13378  ssfzoulel  13490  elfznelfzo  13501  ico01fl0  13548  btwnzge0  13557  ltdifltdiv  13563  ioopnfsup  13593  icopnfsup  13594  modifeq2int  13662  suppssfz  13723  expmordi  13894  faclbnd4lem4  14019  hasheni  14071  hashgt0  14112  hashge1  14113  hashprb  14121  lennncl  14246  wrdsymb0  14261  ccatsymb  14296  ccatlid  14300  ccatass  14302  ccatswrd  14390  swrdccat2  14391  ccatpfx  14423  swrdccatfn  14446  swrdccat  14457  revccat  14488  2cshw  14535  cnpart  14960  resqreu  14973  recval  15043  abs1m  15056  abslem2  15060  fzomaxdiflem  15063  sqreulem  15080  sqreu  15081  limsupgre  15199  rlimdiv  15366  fsumparts  15527  climcnds  15572  expcnv  15585  ntrivcvg  15618  mod2eq1n2dvds  16065  ndvdssub  16127  sadcaddlem  16173  rplpwr  16276  dvdssqlem  16280  algcvgblem  16291  eucalgcvga  16300  isprm2lem  16395  powm2modprm  16513  coprimeprodsq  16518  pythagtriplem11  16535  pythagtriplem13  16537  pcadd2  16600  4sqlem11  16665  vdwlem6  16696  vdwlem8  16698  vdwlem10  16700  ramval  16718  ramcl2  16726  ramlb  16729  ram0  16732  mreintcl  17313  mrcval  17328  mrccl  17329  mrcuni  17339  mrcun  17340  acsfiel  17372  rescabs  17556  rescabsOLD  17557  funcres  17620  setcmon  17811  setcepi  17812  fullestrcsetc  17877  funcsetcestrclem8  17888  fullsetcestrc  17892  yonffthlem  18009  pleval2i  18063  pospo  18072  poslubdg  18141  acsdrsel  18270  acsdrscl  18273  acsficl  18274  psss  18307  grpidd  18364  ismndd  18416  gsumsgrpccat  18487  gsumccatOLD  18488  gsumwmhm  18493  mulgaddcom  18736  subgmulg  18778  resghm  18859  conjnsg  18879  f1otrspeq  19064  pmtrval  19068  pmtrrn  19074  pmtrfinv  19078  pmtrprfval  19104  psgnunilem1  19110  psgnunilem5  19111  psgnunilem4  19114  psgneldm2i  19122  lsmelvalix  19255  pj1ghm  19318  efgredlemc  19360  frgp0  19375  qusabl  19475  cycsubgcyg  19511  gsumval3  19517  gsumcllem  19518  ablfac1c  19683  pgpfac1lem5  19691  isringd  19833  lspsneq0b  20284  lmodindp1  20285  lmhmf1o  20317  lmhmpreima  20319  reslmhm  20323  pwssplit3  20332  lspsncmp  20387  lspsneq  20393  znf1o  20768  dsmmlss  20960  frlmlbs  21013  frlmup1  21014  mpfind  21326  mhplss  21354  mat1  21605  chfacfisf  22012  chfacfisfcpmat  22013  uniopn  22055  ntrval  22196  clsval  22197  neival  22262  neiptopreu  22293  lpval  22299  restdis  22338  lmbrf  22420  cnpnei  22424  1stcrest  22613  hauspwdom  22661  lfinpfin  22684  txcnpi  22768  ptrescn  22799  xkococnlem  22819  qtopeu  22876  kqreglem1  22901  ptuncnv  22967  filss  23013  fsubbas  23027  fbasrn  23044  cfinfil  23053  ufinffr  23089  elfm3  23110  rnelfmlem  23112  rnelfm  23113  flimclslem  23144  flfval  23150  isfcf  23194  cnextfvval  23225  cnextf  23226  cnextcn  23227  ustelimasn  23383  trust  23390  restutop  23398  ustuqtop2  23403  utop2nei  23411  ucncn  23446  trcfilu  23455  cnextucn  23464  met1stc  23686  metustexhalf  23721  cfilucfil  23724  psmetutop  23732  nmoix  23902  nmoeq0  23909  idnghm  23916  blcvx  23970  xrsxmet  23981  iccntr  23993  icccmp  23997  iihalf1  24103  iihalf2  24105  xrhmeo  24118  cnheibor  24127  ipcau2  24407  lmmbrf  24435  iscauf  24453  cmetcaulem  24461  bcthlem4  24500  cmetcusp  24527  rrxcph  24565  minveclem4  24605  evthicc2  24633  cniccbdd  24634  ovollb2  24662  ovolunlem1a  24669  ovolunlem1  24670  voliun  24727  icombl  24737  ioombl  24738  iccvolcl  24740  ioovolcl  24743  mbfss  24819  mbfposb  24826  itg2const2  24915  itg2splitlem  24922  itg2gt0  24934  iblss2  24979  itgioo  24989  dvaddf  25115  dvmulf  25116  dvcobr  25119  dvcof  25121  rolle  25163  dvlip  25166  c1lip1  25170  dvivthlem1  25181  lhop1lem  25186  dvfsumlem1  25199  ftc1lem4  25212  ftc1lem5  25213  ply1divmo  25309  coe1termlem  25428  plydiveu  25467  taylplem1  25531  pserulm  25590  abelth  25609  abscxp2  25857  abscxpbnd  25915  logbgt0b  25952  ang180lem2  25969  ang180lem3  25970  isosctrlem1  25977  angpieqvd  25990  atandmtan  26079  birthdaylem3  26112  wilthlem2  26227  wilthimp  26230  isppw  26272  isppw2  26273  dvdsflsumcom  26346  chteq0  26366  perfectlem2  26387  dchrval  26391  dchrinvcl  26410  dchrptlem1  26421  bposlem3  26443  lgslem4  26457  lgsmod  26480  lgsdilem  26481  lgsdir2lem2  26483  lgsdir2  26487  lgsne0  26492  lgsmulsqcoprm  26500  lgseisenlem1  26532  2lgsoddprm  26573  2sqlem4  26578  chpo1ubb  26638  dchrisumn0  26678  pntrsumbnd2  26724  ostthlem1  26784  ostth3  26795  idmot  26907  tgelrnln  27000  lmimid  27164  lmiisolem  27166  hypcgrlem1  27169  brcgr  27277  colinearalglem4  27286  colinearalg  27287  axlowdimlem14  27332  axcontlem4  27344  cplgrop  27813  lfgriswlk  28065  pthdlem1  28143  crctcshwlkn0  28195  elwspths2on  28334  clwlkclwwlklem2fv2  28369  frgrncvvdeqlem9  28680  nvss  28964  sspn  29107  nmoub3i  29144  nmblolbii  29170  blocnilem  29175  minvecolem4  29251  htthlem  29288  norm1  29620  norm1exi  29621  pjeq  29770  axpjpj  29791  normcan  29947  pjoi0  30088  nmopub2tALT  30280  nmfnleub2  30297  eighmorth  30335  nmbdoplbi  30395  nmcoplbi  30399  nmophmi  30402  nmbdfnlbi  30420  nmcfnlbi  30423  riesz3i  30433  cnlnadjlem7  30444  branmfn  30476  nmopleid  30510  hstle  30601  superpos  30725  cvexchlem  30739  foresf1o  30859  elabreximd  30864  unidifsnne  30893  f1o3d  30971  fmptco1f1o  30977  funcnvmpt  31013  fgreu  31018  suppovss  31026  fsupprnfi  31035  resf1o  31074  fpwrelmap  31077  xrofsup  31099  eliccelico  31107  elicoelioo  31108  iocinif  31111  difioo  31112  eliccioo  31214  cshf1o  31243  mgcmnt1d  31284  mgcmnt2d  31285  pwrssmgc  31287  gsummpt2co  31317  gsumhashmul  31325  submomnd  31345  symgcom  31361  symgcom2  31362  odpmco  31364  pmtrcnel  31367  pmtridf1o  31370  cycpmco2lem6  31407  cycpmco2lem7  31408  cycpmco2  31409  cyc3co2  31416  cycpmconjv  31418  tocyccntz  31420  cyc3evpm  31426  cycpmconjslem2  31431  cycpmconjs  31432  archirngz  31452  ornglmullt  31515  orngrmullt  31516  lindssn  31582  linds2eq  31584  nsgqusf1olem1  31607  nsgqusf1olem3  31609  elrspunidl  31615  rhmimaidl  31618  prmidl2  31625  prmidl0  31635  qsidomlem1  31637  ssmxidl  31651  ply1scleq  31677  lbslsat  31708  lindsunlem  31714  lindsun  31715  dimkerim  31717  fedgmullem1  31719  fedgmullem2  31720  fedgmul  31721  madjusmdetlem2  31787  qtophaus  31795  locfinreflem  31799  zarclssn  31832  zarmxt1  31839  zarcmplem  31840  rhmpreimacn  31844  unitdivcld  31860  tpr2rico  31871  ordtrestNEW  31880  lmxrge0  31911  elzrhunit  31938  qqhf  31945  indf1ofs  32003  gsumesum  32036  esumfsup  32047  esumcvg  32063  issgon  32100  sigainb  32113  insiga  32114  isrnmeas  32177  measvunilem  32189  volmeas  32208  ddeval1  32211  ddeval0  32212  imambfm  32238  omssubadd  32276  carsgclctunlem3  32296  eulerpartlemf  32346  eulerpartlemgvv  32352  probun  32395  dstfrvunirn  32450  plymulx  32536  signslema  32550  signstfvn  32557  signsvtn0  32558  signstfvneq0  32560  signstres  32563  signstfveq0a  32564  breprexplemc  32621  logdivsqrle  32639  hgt750lemg  32643  tgoldbachgtda  32650  tgoldbachgt  32652  lpadmax  32671  lpadleft  32672  lpadright  32673  bnj529  32730  bnj548  32886  bnj570  32894  bnj852  32910  bnj929  32925  bnj1097  32970  bnj1118  32973  bnj1145  32982  funen1cnv  33069  spthcycl  33100  acycgr0v  33119  derangen  33143  subfacp1lem2b  33152  subfacp1lem4  33154  subfacp1lem5  33155  derangfmla  33161  ptpconn  33204  mppspstlem  33542  wsuclem  33828  nosupbnd2lem1  33927  noinfbnd2lem1  33942  nocvxmin  33982  eqscut2  34009  sltlpss  34096  colinearex  34371  btwnconn1lem11  34408  btwnconn1lem12  34409  fwddifnp1  34476  nn0prpwlem  34520  bj-snmoore  35293  bj-imdiridlem  35365  relowlpssretop  35544  fin2so  35773  matunitlindflem2  35783  ptrecube  35786  poimirlem8  35794  poimirlem13  35799  poimirlem15  35801  poimirlem24  35810  poimirlem25  35811  poimirlem26  35812  heicant  35821  mblfinlem2  35824  voliunnfl  35830  mbfresfi  35832  itg2addnclem  35837  itg2addnclem3  35839  itg2gt0cn  35841  ftc1cnnclem  35857  ftc1anclem5  35863  cover2  35881  indexdom  35901  sdclem1  35910  fdc  35912  equivbnd2  35959  heiborlem8  35985  heibor  35988  isdrngo2  36125  iscringd  36165  smprngopr  36219  prnc  36234  eqeltr  36390  islfld  37083  lkrshpor  37128  lfl1dim  37142  lfl1dim2N  37143  cmtcomlemN  37269  2lplnmN  37580  pmapjat1  37874  trlnid  38200  tendoex  38996  dia1dimid  39084  dibval2  39165  dihmeetlem2N  39320  dochlkr  39406  mapdcv  39681  hdmaplkr  39934  hdmapip0  39936  hlhillcs  39983  frlmvscadiccat  40244  mhphf  40292  dvdsexpnn  40347  nacsfix  40541  3rexfrabdioph  40626  4rexfrabdioph  40627  6rexfrabdioph  40628  7rexfrabdioph  40629  eldioph4b  40640  pellexlem2  40659  pellexlem5  40662  jm2.26lem3  40830  numinfctb  40935  ntrclsfv1  41672  ntrneifv1  41696  ntrneifv2  41697  cvgdvgrat  41938  radcnvrat  41939  dvconstbi  41959  bccbc  41970  elpwgded  42191  elpwgdedVD  42544  sspwimpcf  42547  sspwimpcfVD  42548  sspwimpALT2  42555  ax6e2ndeqALT  42558  eliuniin  42656  eliuniin2  42676  qinioo  43080  dfxlim2v  43395  xlimliminflimsup  43410  cncfiooicclem1  43441  ibliooicc  43519  stoweidlem27  43575  stoweidlem28  43576  fourierdlem89  43743  fourierdlem91  43745  fourierdlem92  43746  smflimmpt  44354  odz2prm2pw  45026  perfectALTVlem2  45185  blen1b  45945  naryfvalelfv  45989  itscnhlc0yqe  46116  itsclquadb  46133  lubeldm2  46261  glbeldm2  46262  ipolub  46285  ipoglb  46288  functhinclem1  46333  thincciso  46341  prsthinc  46346  prstchom2ALT  46371  onetansqsecsq  46474  cotsqcscsq  46475  aacllem  46516