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  bibiad  840  oplem1  1057  eqtr  2756  pm13.181  3014  opabss  5149  axprlem4OLD  5372  axprlem5OLD  5373  euotd  5467  brcogw  5823  somin1  6096  xpdifid  6132  funfni  6604  fnssres  6621  fn0  6629  fnimadisj  6630  fnimaeq0  6631  foimacnv  6797  fvelimab  6912  dffv2  6935  fvopab3ig  6943  funcnvmpt  6949  dff3  7052  dffo4  7055  fpr2g  7166  ralima  7192  f1eqcocnv  7256  isomin  7292  f1ocnv2d  7620  fnexALT  7904  xp1st  7974  xp2nd  7975  frrlem3  8238  fpr2  8254  wfr3g  8269  wfr2  8277  iinon  8280  tfr3  8338  oawordri  8485  oaass  8496  omeulem1  8517  oeoa  8533  oeoe  8535  oeeulem  8537  elqsn0  8731  pwdom  9067  enfii  9120  phpeqd  9146  ominf  9174  findcard3  9193  marypha1lem  9346  wofib  9460  cantnff  9595  cantnfp1  9602  cantnf  9614  cnfcomlem  9620  ttrcltr  9637  frr3g  9680  r1sscl  9709  rankval3b  9750  infxpidm2  9939  numdom  9960  onssnum  9962  acni  9967  acni2  9968  dfac5  10051  djulepw  10115  infunsdom1  10134  infunsdom  10135  cofsmo  10191  cfsmolem  10192  fin1ai  10215  fin2i  10217  isf34lem1  10294  fin67  10317  itunisuc  10341  axdc3lem4  10375  zornn0g  10427  ttukeylem6  10436  brdom3  10450  tsken  10677  tskcard  10704  r1tskina  10705  intgru  10737  prlem934  10956  ltexprlem7  10965  supaddc  12123  mul2lt0rlt0  13046  xrmaxeq  13131  xrmineq  13132  xmulneg1  13221  ixxun  13314  difelfzle  13595  ssfzoulel  13715  elfznelfzo  13728  ico01fl0  13778  btwnzge0  13787  ltdifltdiv  13793  ioopnfsup  13823  icopnfsup  13824  modifeq2int  13895  suppssfz  13956  expmordi  14129  zzlesq  14168  faclbnd4lem4  14258  hasheni  14310  hashgt0  14350  hashge1  14351  hashprb  14359  lennncl  14496  wrdsymb0  14511  ccatsymb  14545  ccatlid  14549  ccatass  14551  ccatswrd  14631  swrdccat2  14632  ccatpfx  14663  swrdccatfn  14686  swrdccat  14697  revccat  14728  2cshw  14775  cnpart  15202  resqreu  15214  recval  15285  abs1m  15298  abslem2  15302  fzomaxdiflem  15305  sqreulem  15322  sqreu  15323  limsupgre  15443  rlimdiv  15608  fsumparts  15769  climcnds  15816  expcnv  15829  ntrivcvg  15862  mod2eq1n2dvds  16316  ndvdssub  16378  sadcaddlem  16426  rplpwr  16527  dvdssqlem  16535  algcvgblem  16546  eucalgcvga  16555  isprm2lem  16650  powm2modprm  16774  coprimeprodsq  16779  pythagtriplem11  16796  pythagtriplem13  16798  pcadd2  16861  4sqlem11  16926  vdwlem6  16957  vdwlem8  16959  vdwlem10  16961  ramval  16979  ramcl2  16987  ramlb  16990  ram0  16993  mreintcl  17557  mrcval  17576  mrccl  17577  mrcuni  17587  mrcun  17588  acsfiel  17620  rescabs  17800  funcres  17863  setcmon  18054  setcepi  18055  fullestrcsetc  18117  funcsetcestrclem8  18128  fullsetcestrc  18132  yonffthlem  18248  pleval2i  18300  pospo  18309  poslubdg  18378  acsdrsel  18509  acsdrscl  18512  acsficl  18513  psss  18546  chnind  18587  chnub  18588  chnccats1  18591  chnccat  18592  grpidd  18639  ismndd  18724  gsumsgrpccat  18808  gsumwmhm  18813  mulgaddcom  19074  subgmulg  19116  resghm  19207  conjnsg  19229  ghmqusker  19262  f1otrspeq  19422  pmtrval  19426  pmtrrn  19432  pmtrfinv  19436  pmtrprfval  19462  psgnunilem1  19468  psgnunilem5  19469  psgnunilem4  19472  psgneldm2i  19480  lsmelvalix  19616  pj1ghm  19678  efgredlemc  19720  frgp0  19735  qusabl  19840  cycsubgcyg  19876  gsumval3  19882  gsumcllem  19883  ablfac1c  20048  pgpfac1lem5  20056  submomnd  20107  isrngd  20154  isringd  20272  01eq0ring  20507  ornglmullt  20846  orngrmullt  20847  lspsneq0b  21008  lmodindp1  21009  lmhmf1o  21041  lmhmpreima  21043  reslmhm  21047  pwssplit3  21056  lspsncmp  21114  lspsneq  21120  znf1o  21531  dsmmlss  21724  frlmlbs  21777  frlmup1  21778  psrgrp  21935  mpfind  22093  psdmul  22132  ply1scleq  22270  mat1  22412  chfacfisf  22819  chfacfisfcpmat  22820  uniopn  22862  ntrval  23001  clsval  23002  neival  23067  neiptopreu  23098  lpval  23104  restdis  23143  lmbrf  23225  cnpnei  23229  1stcrest  23418  hauspwdom  23466  lfinpfin  23489  txcnpi  23573  ptrescn  23604  xkococnlem  23624  qtopeu  23681  kqreglem1  23706  ptuncnv  23772  filss  23818  fsubbas  23832  fbasrn  23849  cfinfil  23858  ufinffr  23894  elfm3  23915  rnelfmlem  23917  rnelfm  23918  flimclslem  23949  flfval  23955  isfcf  23999  cnextfvval  24030  cnextf  24031  cnextcn  24032  ustelimasn  24188  trust  24194  restutop  24202  ustuqtop2  24207  utop2nei  24215  ucncn  24249  trcfilu  24258  cnextucn  24267  met1stc  24486  metustexhalf  24521  cfilucfil  24524  psmetutop  24532  nmoix  24694  nmoeq0  24701  idnghm  24708  blcvx  24763  xrsxmet  24775  iccntr  24787  icccmp  24791  iihalf1  24898  iihalf2  24900  xrhmeo  24913  cnheibor  24922  ipcau2  25201  lmmbrf  25229  iscauf  25247  cmetcaulem  25255  bcthlem4  25294  cmetcusp  25321  rrxcph  25359  minveclem4  25399  evthicc2  25427  cniccbdd  25428  ovollb2  25456  ovolunlem1a  25463  ovolunlem1  25464  voliun  25521  icombl  25531  ioombl  25532  iccvolcl  25534  ioovolcl  25537  mbfss  25613  mbfposb  25620  itg2const2  25708  itg2splitlem  25715  itg2gt0  25727  iblss2  25773  itgioo  25783  dvaddf  25909  dvmulf  25910  dvcobr  25913  dvcof  25915  rolle  25957  dvlip  25960  c1lip1  25964  dvivthlem1  25975  lhop1lem  25980  dvfsumlem1  25993  ftc1lem4  26006  ftc1lem5  26007  ply1divmo  26101  coe1termlem  26223  plydiveu  26264  taylplem1  26328  pserulm  26387  abelth  26406  abscxp2  26657  abscxpbnd  26717  logbgt0b  26757  ang180lem2  26774  ang180lem3  26775  isosctrlem1  26782  angpieqvd  26795  atandmtan  26884  birthdaylem3  26917  wilthlem2  27032  wilthimp  27035  isppw  27077  isppw2  27078  dvdsflsumcom  27151  chteq0  27172  perfectlem2  27193  dchrval  27197  dchrinvcl  27216  dchrptlem1  27227  bposlem3  27249  lgslem4  27263  lgsmod  27286  lgsdilem  27287  lgsdir2lem2  27289  lgsdir2  27293  lgsne0  27298  lgsmulsqcoprm  27306  lgseisenlem1  27338  2lgsoddprm  27379  2sqlem4  27384  chpo1ubb  27444  dchrisumn0  27484  pntrsumbnd2  27530  ostthlem1  27590  ostth3  27601  nosupbnd2lem1  27679  noinfbnd2lem1  27694  nocvxmin  27747  eqcuts2  27778  ltslpss  27900  madefi  27905  abslts  28241  eucliddivs  28368  peano5uzs  28396  z12bdaylem1  28462  elreno2  28487  idmot  28605  tgelrnln  28698  lmimid  28862  lmiisolem  28864  hypcgrlem1  28867  brcgr  28969  colinearalglem4  28978  colinearalg  28979  axlowdimlem14  29024  axcontlem4  29036  cplgrop  29506  lfgriswlk  29755  pthdlem1  29834  crctcshwlkn0  29889  elwspths2on  30030  elwspths2onw  30031  clwlkclwwlklem2fv2  30066  frgrncvvdeqlem9  30377  nvss  30664  sspn  30807  nmoub3i  30844  nmblolbii  30870  blocnilem  30875  minvecolem4  30951  htthlem  30988  norm1  31320  norm1exi  31321  pjeq  31470  axpjpj  31491  normcan  31647  pjoi0  31788  nmopub2tALT  31980  nmfnleub2  31997  eighmorth  32035  nmbdoplbi  32095  nmcoplbi  32099  nmophmi  32102  nmbdfnlbi  32120  nmcfnlbi  32123  riesz3i  32133  cnlnadjlem7  32144  branmfn  32176  nmopleid  32210  hstle  32301  superpos  32425  cvexchlem  32439  foresf1o  32574  elabreximd  32580  prssad  32599  prssbd  32600  unidifsnne  32606  tpssad  32609  fresunsn  32698  f1o3d  32699  fmptco1f1o  32706  fgreu  32744  suppovss  32754  elsuppfnd  32755  fsupprnfi  32765  resf1o  32803  fpwrelmap  32806  argcj  32821  xrofsup  32840  eliccelico  32850  elicoelioo  32851  iocinif  32854  difioo  32855  hashpss  32882  hashne0  32883  elq2  32885  oexpled  32920  indf1ofs  32926  eliccioo  32990  cshf1o  33022  mgcmnt1d  33057  mgcmnt2d  33058  pwrssmgc  33060  mndlactf1o  33090  mndractf1o  33091  gsummpt2co  33109  gsumhashmul  33128  gsummulsubdishift1  33129  symgcom  33144  symgcom2  33145  odpmco  33147  pmtrcnel  33150  pmtridf1o  33155  cycpmco2lem6  33192  cycpmco2lem7  33193  cycpmco2  33194  cyc3co2  33201  cycpmconjv  33203  tocyccntz  33205  cyc3evpm  33211  cycpmconjslem2  33216  cycpmconjs  33217  fxpsubm  33233  fxpsubg  33234  fxpsubrg  33235  fxpsdrg  33236  archirngz  33250  unitnz  33300  elrgspnlem1  33303  elrgspnlem2  33304  elrgspnlem4  33306  elrgspnsubrun  33310  rloccring  33331  rlocf1  33334  domnpropd  33338  rrgsubm  33345  isdrng4  33356  sdrgdvcl  33360  sdrginvcl  33361  fracfld  33369  lindssn  33438  linds2eq  33441  dvdsrspss  33447  nsgqusf1olem1  33473  nsgqusf1olem3  33475  unitpidl1  33484  elrspunidl  33488  rhmimaidl  33492  drngidlhash  33494  prmidl2  33501  prmidl0  33510  qsidomlem1  33512  ssdifidlprm  33518  mxidlirredi  33531  mxidlirred  33532  ssmxidl  33534  drng0mxidl  33536  opprmxidlabs  33547  qsdrngilem  33554  qsdrngi  33555  qsdrng  33557  rsprprmprmidl  33582  rsprprmprmidlb  33583  rprmasso2  33586  rprmirredlem  33590  rprmirredb  33592  1arithidomlem2  33596  1arithufdlem4  33607  1arithufd  33608  ressply1evls1  33625  ply1asclunit  33634  ply1dg1rt  33640  ply1mulrtss  33642  ply1dg3rt0irred  33644  ply1degltlss  33656  ply1gsumz  33659  evlextv  33686  esplyfv1  33713  esplyind  33719  vietadeg1  33722  lsssra  33732  exsslsb  33741  lbslsat  33760  lindsunlem  33768  lindsun  33769  dimkerim  33771  fedgmullem1  33773  fedgmullem2  33774  fedgmul  33775  dimlssid  33776  lvecendof1f1o  33777  assalactf1o  33779  sdrgfldext  33794  fldsdrgfldext  33805  fldgenfldext  33812  evls1fldgencl  33814  fldextrspunlsp  33818  fldextrspunlem1  33819  fldextrspunfld  33820  irngss  33831  0ringirng  33833  irngnzply1  33835  extdgfialglem1  33836  irngnminplynz  33856  minplyelirng  33859  irredminply  33860  algextdeglem2  33862  algextdeglem4  33864  constrconj  33889  constrextdg2lem  33892  constrext2chnlem  33894  iconstr  33910  constrsdrg  33919  cos9thpiminplylem1  33926  cos9thpiminplylem2  33927  cos9thpiminplylem3  33928  cos9thpiminplylem5  33930  madjusmdetlem2  33972  qtophaus  33980  locfinreflem  33984  zarclssn  34017  zarmxt1  34024  zarcmplem  34025  rhmpreimacn  34029  unitdivcld  34045  tpr2rico  34056  ordtrestNEW  34065  lmxrge0  34096  elzrhunit  34121  qqhf  34130  gsumesum  34203  esumfsup  34214  esumcvg  34230  issgon  34267  sigainb  34280  insiga  34281  isrnmeas  34344  measvunilem  34356  volmeas  34375  ddeval1  34378  ddeval0  34379  imambfm  34406  omssubadd  34444  carsgclctunlem3  34464  eulerpartlemf  34514  eulerpartlemgvv  34520  probun  34563  dstfrvunirn  34619  plymulx  34692  signslema  34706  signstfvn  34713  signsvtn0  34714  signstfvneq0  34716  signstres  34719  signstfveq0a  34720  breprexplemc  34776  logdivsqrle  34794  hgt750lemg  34798  tgoldbachgtda  34805  tgoldbachgt  34807  lpadmax  34826  lpadleft  34827  lpadright  34828  bnj529  34884  bnj548  35039  bnj570  35047  bnj852  35063  bnj929  35078  bnj1097  35123  bnj1118  35126  bnj1145  35135  funen1cnv  35231  fissorduni  35233  spthcycl  35311  acycgr0v  35330  derangen  35354  subfacp1lem2b  35363  subfacp1lem4  35365  subfacp1lem5  35366  derangfmla  35372  ptpconn  35415  mppspstlem  35753  wsuclem  36005  colinearex  36242  btwnconn1lem11  36279  btwnconn1lem12  36280  fwddifnp1  36347  nn0prpwlem  36504  ttctr  36675  dfttc2g  36688  regsfromregtco  36720  bj-snmoore  37425  bj-imdiridlem  37499  relowlpssretop  37680  fin2so  37928  matunitlindflem2  37938  ptrecube  37941  poimirlem8  37949  poimirlem13  37954  poimirlem15  37956  poimirlem24  37965  poimirlem25  37966  poimirlem26  37967  heicant  37976  mblfinlem2  37979  voliunnfl  37985  mbfresfi  37987  itg2addnclem  37992  itg2addnclem3  37994  itg2gt0cn  37996  ftc1cnnclem  38012  ftc1anclem5  38018  cover2  38036  indexdom  38055  sdclem1  38064  fdc  38066  equivbnd2  38113  heiborlem8  38139  heibor  38142  isdrngo2  38279  iscringd  38319  smprngopr  38373  prnc  38388  eqbrtr  38559  eqeltr  38561  islfld  39508  lkrshpor  39553  lfl1dim  39567  lfl1dim2N  39568  cmtcomlemN  39694  2lplnmN  40005  pmapjat1  40299  trlnid  40625  tendoex  41421  dia1dimid  41509  dibval2  41590  dihmeetlem2N  41745  dochlkr  41831  mapdcv  42106  hdmaplkr  42359  hdmapip0  42361  hlhillcs  42404  aks6d1c6lem4  42612  dvdsexpnn  42765  readvrec  42794  frlmvscadiccat  42951  psrmnd  42988  nacsfix  43144  3rexfrabdioph  43225  4rexfrabdioph  43226  6rexfrabdioph  43227  7rexfrabdioph  43228  eldioph4b  43239  pellexlem2  43258  pellexlem5  43261  jm2.26lem3  43429  numinfctb  43531  ordne0gt0  43689  omge1  43725  omlim2  43727  omord2lim  43728  omord2i  43729  tfsconcatfv  43769  tfsconcatb0  43772  oaun3lem1  43802  ntrclsfv1  44482  ntrneifv1  44506  ntrneifv2  44507  cvgdvgrat  44740  radcnvrat  44741  dvconstbi  44761  bccbc  44772  elpwgded  44991  elpwgdedVD  45343  sspwimpcf  45346  sspwimpcfVD  45347  sspwimpALT2  45354  ax6e2ndeqALT  45357  eliuniin  45529  eliuniin2  45550  qinioo  45965  dfxlim2v  46275  xlimliminflimsup  46290  cncfiooicclem1  46321  ibliooicc  46399  stoweidlem27  46455  stoweidlem28  46456  fourierdlem89  46623  fourierdlem91  46625  fourierdlem92  46626  smflimmpt  47238  odz2prm2pw  48026  perfectALTVlem2  48198  blen1b  49064  naryfvalelfv  49108  itscnhlc0yqe  49235  itsclquadb  49252  lubeldm2  49431  glbeldm2  49432  ipolub  49463  ipoglb  49466  fucofulem1  49785  functhinclem1  49919  thincciso  49928  prsthinc  49939  functermclem  49982  prstchom2ALT  50039  onetansqsecsq  50236  cotsqcscsq  50237  aacllem  50276