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  oplem1  1057  eqtr  2763  pm13.181  3029  opabss  5230  axprlem4  5444  axprlem5  5445  euotd  5532  brcogw  5893  somin1  6165  xpdifid  6199  funfni  6685  fncoOLD  6698  fnssres  6703  fn0  6711  fnimadisj  6712  fnimaeq0  6713  foimacnv  6879  fvelimab  6994  dffv2  7017  fvopab3ig  7025  dff3  7134  dffo4  7137  fpr2g  7248  ralima  7274  f1eqcocnv  7337  isomin  7373  f1ocnv2d  7703  fnexALT  7991  xp1st  8062  xp2nd  8063  frrlem3  8329  fpr2  8345  wfr3g  8363  wfrlem3OLD  8366  wfrlem4OLD  8368  wfr2  8392  iinon  8396  tfr3  8455  oawordri  8606  oaass  8617  omeulem1  8638  oeoa  8653  oeoe  8655  oeeulem  8657  ecelqsg  8830  elqsn0  8844  pwdom  9195  enfii  9252  phpeqd  9278  ominf  9321  findcard3  9346  marypha1lem  9502  wofib  9614  cantnff  9743  cantnfp1  9750  cantnf  9762  cnfcomlem  9768  ttrcltr  9785  frr3g  9825  r1sscl  9854  rankval3b  9895  infxpidm2  10086  numdom  10107  onssnum  10109  acni  10114  acni2  10115  dfac5  10198  djulepw  10262  infunsdom1  10281  infunsdom  10282  cofsmo  10338  cfsmolem  10339  fin1ai  10362  fin2i  10364  isf34lem1  10441  fin67  10464  itunisuc  10488  axdc3lem4  10522  zornn0g  10574  ttukeylem6  10583  brdom3  10597  tsken  10823  tskcard  10850  r1tskina  10851  intgru  10883  prlem934  11102  ltexprlem7  11111  supaddc  12262  mul2lt0rlt0  13159  xrmaxeq  13241  xrmineq  13242  xmulneg1  13331  ixxun  13423  difelfzle  13698  ssfzoulel  13810  elfznelfzo  13822  ico01fl0  13870  btwnzge0  13879  ltdifltdiv  13885  ioopnfsup  13915  icopnfsup  13916  modifeq2int  13984  suppssfz  14045  expmordi  14217  zzlesq  14255  faclbnd4lem4  14345  hasheni  14397  hashgt0  14437  hashge1  14438  hashprb  14446  lennncl  14582  wrdsymb0  14597  ccatsymb  14630  ccatlid  14634  ccatass  14636  ccatswrd  14716  swrdccat2  14717  ccatpfx  14749  swrdccatfn  14772  swrdccat  14783  revccat  14814  2cshw  14861  cnpart  15289  resqreu  15301  recval  15371  abs1m  15384  abslem2  15388  fzomaxdiflem  15391  sqreulem  15408  sqreu  15409  limsupgre  15527  rlimdiv  15694  fsumparts  15854  climcnds  15899  expcnv  15912  ntrivcvg  15945  mod2eq1n2dvds  16395  ndvdssub  16457  sadcaddlem  16503  rplpwr  16605  dvdssqlem  16613  algcvgblem  16624  eucalgcvga  16633  isprm2lem  16728  powm2modprm  16850  coprimeprodsq  16855  pythagtriplem11  16872  pythagtriplem13  16874  pcadd2  16937  4sqlem11  17002  vdwlem6  17033  vdwlem8  17035  vdwlem10  17037  ramval  17055  ramcl2  17063  ramlb  17066  ram0  17069  mreintcl  17653  mrcval  17668  mrccl  17669  mrcuni  17679  mrcun  17680  acsfiel  17712  rescabs  17896  rescabsOLD  17897  funcres  17960  setcmon  18154  setcepi  18155  fullestrcsetc  18220  funcsetcestrclem8  18231  fullsetcestrc  18235  yonffthlem  18352  pleval2i  18406  pospo  18415  poslubdg  18484  acsdrsel  18613  acsdrscl  18616  acsficl  18617  psss  18650  grpidd  18709  ismndd  18794  gsumsgrpccat  18875  gsumwmhm  18880  mulgaddcom  19138  subgmulg  19180  resghm  19272  conjnsg  19294  ghmqusker  19327  f1otrspeq  19489  pmtrval  19493  pmtrrn  19499  pmtrfinv  19503  pmtrprfval  19529  psgnunilem1  19535  psgnunilem5  19536  psgnunilem4  19539  psgneldm2i  19547  lsmelvalix  19683  pj1ghm  19745  efgredlemc  19787  frgp0  19802  qusabl  19907  cycsubgcyg  19943  gsumval3  19949  gsumcllem  19950  ablfac1c  20115  pgpfac1lem5  20123  isrngd  20200  isringd  20314  01eq0ring  20556  lspsneq0b  21034  lmodindp1  21035  lmhmf1o  21068  lmhmpreima  21070  reslmhm  21074  pwssplit3  21083  lspsncmp  21141  lspsneq  21147  znf1o  21593  dsmmlss  21787  frlmlbs  21840  frlmup1  21841  psrgrp  21999  mpfind  22154  psdmul  22193  ply1scleq  22330  mat1  22474  chfacfisf  22881  chfacfisfcpmat  22882  uniopn  22924  ntrval  23065  clsval  23066  neival  23131  neiptopreu  23162  lpval  23168  restdis  23207  lmbrf  23289  cnpnei  23293  1stcrest  23482  hauspwdom  23530  lfinpfin  23553  txcnpi  23637  ptrescn  23668  xkococnlem  23688  qtopeu  23745  kqreglem1  23770  ptuncnv  23836  filss  23882  fsubbas  23896  fbasrn  23913  cfinfil  23922  ufinffr  23958  elfm3  23979  rnelfmlem  23981  rnelfm  23982  flimclslem  24013  flfval  24019  isfcf  24063  cnextfvval  24094  cnextf  24095  cnextcn  24096  ustelimasn  24252  trust  24259  restutop  24267  ustuqtop2  24272  utop2nei  24280  ucncn  24315  trcfilu  24324  cnextucn  24333  met1stc  24555  metustexhalf  24590  cfilucfil  24593  psmetutop  24601  nmoix  24771  nmoeq0  24778  idnghm  24785  blcvx  24839  xrsxmet  24850  iccntr  24862  icccmp  24866  iihalf1  24977  iihalf2  24980  xrhmeo  24996  cnheibor  25006  ipcau2  25287  lmmbrf  25315  iscauf  25333  cmetcaulem  25341  bcthlem4  25380  cmetcusp  25407  rrxcph  25445  minveclem4  25485  evthicc2  25514  cniccbdd  25515  ovollb2  25543  ovolunlem1a  25550  ovolunlem1  25551  voliun  25608  icombl  25618  ioombl  25619  iccvolcl  25621  ioovolcl  25624  mbfss  25700  mbfposb  25707  itg2const2  25796  itg2splitlem  25803  itg2gt0  25815  iblss2  25861  itgioo  25871  dvaddf  25999  dvmulf  26000  dvcobr  26003  dvcobrOLD  26004  dvcof  26006  rolle  26048  dvlip  26052  c1lip1  26056  dvivthlem1  26067  lhop1lem  26072  dvfsumlem1  26086  ftc1lem4  26100  ftc1lem5  26101  ply1divmo  26195  coe1termlem  26317  plydiveu  26358  taylplem1  26422  pserulm  26483  abelth  26503  abscxp2  26753  abscxpbnd  26814  logbgt0b  26854  ang180lem2  26871  ang180lem3  26872  isosctrlem1  26879  angpieqvd  26892  atandmtan  26981  birthdaylem3  27014  wilthlem2  27130  wilthimp  27133  isppw  27175  isppw2  27176  dvdsflsumcom  27249  chteq0  27271  perfectlem2  27292  dchrval  27296  dchrinvcl  27315  dchrptlem1  27326  bposlem3  27348  lgslem4  27362  lgsmod  27385  lgsdilem  27386  lgsdir2lem2  27388  lgsdir2  27392  lgsne0  27397  lgsmulsqcoprm  27405  lgseisenlem1  27437  2lgsoddprm  27478  2sqlem4  27483  chpo1ubb  27543  dchrisumn0  27583  pntrsumbnd2  27629  ostthlem1  27689  ostth3  27700  nosupbnd2lem1  27778  noinfbnd2lem1  27793  nocvxmin  27841  eqscut2  27869  sltlpss  27963  madefi  27968  absslt  28291  peano5uzs  28408  idmot  28563  tgelrnln  28656  lmimid  28820  lmiisolem  28822  hypcgrlem1  28825  brcgr  28933  colinearalglem4  28942  colinearalg  28943  axlowdimlem14  28988  axcontlem4  29000  cplgrop  29472  lfgriswlk  29724  pthdlem1  29802  crctcshwlkn0  29854  elwspths2on  29993  clwlkclwwlklem2fv2  30028  frgrncvvdeqlem9  30339  nvss  30625  sspn  30768  nmoub3i  30805  nmblolbii  30831  blocnilem  30836  minvecolem4  30912  htthlem  30949  norm1  31281  norm1exi  31282  pjeq  31431  axpjpj  31452  normcan  31608  pjoi0  31749  nmopub2tALT  31941  nmfnleub2  31958  eighmorth  31996  nmbdoplbi  32056  nmcoplbi  32060  nmophmi  32063  nmbdfnlbi  32081  nmcfnlbi  32084  riesz3i  32094  cnlnadjlem7  32105  branmfn  32137  nmopleid  32171  hstle  32262  superpos  32386  cvexchlem  32400  bibiad  32486  foresf1o  32532  elabreximd  32538  unidifsnne  32564  f1o3d  32646  fmptco1f1o  32652  funcnvmpt  32685  fgreu  32690  suppovss  32697  fsupprnfi  32704  resf1o  32744  fpwrelmap  32747  xrofsup  32774  eliccelico  32782  elicoelioo  32783  iocinif  32786  difioo  32787  eliccioo  32895  cshf1o  32929  mgcmnt1d  32970  mgcmnt2d  32971  pwrssmgc  32973  chnind  32983  chnub  32984  mndlactf1o  33016  mndractf1o  33017  gsummpt2co  33031  gsumhashmul  33040  submomnd  33060  symgcom  33076  symgcom2  33077  odpmco  33079  pmtrcnel  33082  pmtridf1o  33087  cycpmco2lem6  33124  cycpmco2lem7  33125  cycpmco2  33126  cyc3co2  33133  cycpmconjv  33135  tocyccntz  33137  cyc3evpm  33143  cycpmconjslem2  33148  cycpmconjs  33149  archirngz  33169  unitnz  33219  rloccring  33242  rlocf1  33245  rrgsubm  33253  isdrng4  33264  sdrgdvcl  33266  sdrginvcl  33267  fracfld  33275  ornglmullt  33302  orngrmullt  33303  lindssn  33371  linds2eq  33374  dvdsrspss  33380  nsgqusf1olem1  33406  nsgqusf1olem3  33408  unitpidl1  33417  elrspunidl  33421  rhmimaidl  33425  drngidlhash  33427  prmidl2  33434  prmidl0  33443  qsidomlem1  33445  ssdifidlprm  33451  mxidlirredi  33464  mxidlirred  33465  ssmxidl  33467  drng0mxidl  33469  opprmxidlabs  33480  qsdrngilem  33487  qsdrngi  33488  qsdrng  33490  rsprprmprmidl  33515  rsprprmprmidlb  33516  rprmasso2  33519  rprmirredlem  33523  rprmirredb  33525  1arithidomlem2  33529  1arithufdlem4  33540  1arithufd  33541  ply1asclunit  33564  ply1dg1rt  33569  ply1mulrtss  33571  ply1dg3rt0irred  33572  ply1degltlss  33582  ply1gsumz  33584  lsssra  33603  lbslsat  33629  lindsunlem  33637  lindsun  33638  dimkerim  33640  fedgmullem1  33642  fedgmullem2  33643  fedgmul  33644  dimlssid  33645  lvecendof1f1o  33646  assalactf1o  33648  fldgenfldext  33678  evls1fldgencl  33680  irngss  33687  0ringirng  33689  irngnzply1  33691  irngnminplynz  33705  irredminply  33707  algextdeglem2  33709  algextdeglem4  33711  constrconj  33735  madjusmdetlem2  33774  qtophaus  33782  locfinreflem  33786  zarclssn  33819  zarmxt1  33826  zarcmplem  33827  rhmpreimacn  33831  unitdivcld  33847  tpr2rico  33858  ordtrestNEW  33867  lmxrge0  33898  elzrhunit  33925  qqhf  33932  indf1ofs  33990  gsumesum  34023  esumfsup  34034  esumcvg  34050  issgon  34087  sigainb  34100  insiga  34101  isrnmeas  34164  measvunilem  34176  volmeas  34195  ddeval1  34198  ddeval0  34199  imambfm  34227  omssubadd  34265  carsgclctunlem3  34285  eulerpartlemf  34335  eulerpartlemgvv  34341  probun  34384  dstfrvunirn  34439  plymulx  34525  signslema  34539  signstfvn  34546  signsvtn0  34547  signstfvneq0  34549  signstres  34552  signstfveq0a  34553  breprexplemc  34609  logdivsqrle  34627  hgt750lemg  34631  tgoldbachgtda  34638  tgoldbachgt  34640  lpadmax  34659  lpadleft  34660  lpadright  34661  bnj529  34717  bnj548  34873  bnj570  34881  bnj852  34897  bnj929  34912  bnj1097  34957  bnj1118  34960  bnj1145  34969  funen1cnv  35064  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  36288  bj-snmoore  37079  bj-imdiridlem  37151  relowlpssretop  37330  fin2so  37567  matunitlindflem2  37577  ptrecube  37580  poimirlem8  37588  poimirlem13  37593  poimirlem15  37595  poimirlem24  37604  poimirlem25  37605  poimirlem26  37606  heicant  37615  mblfinlem2  37618  voliunnfl  37624  mbfresfi  37626  itg2addnclem  37631  itg2addnclem3  37633  itg2gt0cn  37635  ftc1cnnclem  37651  ftc1anclem5  37657  cover2  37675  indexdom  37694  sdclem1  37703  fdc  37705  equivbnd2  37752  heiborlem8  37778  heibor  37781  isdrngo2  37918  iscringd  37958  smprngopr  38012  prnc  38027  eqbrtr  38187  eqeltr  38189  islfld  39018  lkrshpor  39063  lfl1dim  39077  lfl1dim2N  39078  cmtcomlemN  39204  2lplnmN  39516  pmapjat1  39810  trlnid  40136  tendoex  40932  dia1dimid  41020  dibval2  41101  dihmeetlem2N  41256  dochlkr  41342  mapdcv  41617  hdmaplkr  41870  hdmapip0  41872  hlhillcs  41919  aks6d1c6lem4  42130  dvdsexpnn  42320  frlmvscadiccat  42461  psrmnd  42500  nacsfix  42668  3rexfrabdioph  42753  4rexfrabdioph  42754  6rexfrabdioph  42755  7rexfrabdioph  42756  eldioph4b  42767  pellexlem2  42786  pellexlem5  42789  jm2.26lem3  42958  numinfctb  43060  ordne0gt0  43223  omge1  43259  omlim2  43261  omord2lim  43262  omord2i  43263  tfsconcatfv  43303  tfsconcatb0  43306  oaun3lem1  43336  ntrclsfv1  44017  ntrneifv1  44041  ntrneifv2  44042  cvgdvgrat  44282  radcnvrat  44283  dvconstbi  44303  bccbc  44314  elpwgded  44535  elpwgdedVD  44888  sspwimpcf  44891  sspwimpcfVD  44892  sspwimpALT2  44899  ax6e2ndeqALT  44902  eliuniin  45001  eliuniin2  45022  qinioo  45453  dfxlim2v  45768  xlimliminflimsup  45783  cncfiooicclem1  45814  ibliooicc  45892  stoweidlem27  45948  stoweidlem28  45949  fourierdlem89  46116  fourierdlem91  46118  fourierdlem92  46119  smflimmpt  46731  odz2prm2pw  47437  perfectALTVlem2  47596  blen1b  48322  naryfvalelfv  48366  itscnhlc0yqe  48493  itsclquadb  48510  lubeldm2  48636  glbeldm2  48637  ipolub  48660  ipoglb  48663  functhinclem1  48708  thincciso  48716  prsthinc  48721  prstchom2ALT  48746  onetansqsecsq  48853  cotsqcscsq  48854  aacllem  48895