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  2760  pm13.181  3023  opabss  5207  axprlem4OLD  5429  axprlem5OLD  5430  euotd  5518  brcogw  5879  somin1  6153  xpdifid  6188  funfni  6674  fnssres  6691  fn0  6699  fnimadisj  6700  fnimaeq0  6701  foimacnv  6865  fvelimab  6981  dffv2  7004  fvopab3ig  7012  dff3  7120  dffo4  7123  fpr2g  7231  ralima  7257  f1eqcocnv  7321  isomin  7357  f1ocnv2d  7686  fnexALT  7975  xp1st  8046  xp2nd  8047  frrlem3  8313  fpr2  8329  wfr3g  8347  wfrlem3OLD  8350  wfrlem4OLD  8352  wfr2  8376  iinon  8380  tfr3  8439  oawordri  8588  oaass  8599  omeulem1  8620  oeoa  8635  oeoe  8637  oeeulem  8639  ecelqsg  8812  elqsn0  8826  pwdom  9169  enfii  9226  phpeqd  9252  ominf  9294  findcard3  9318  marypha1lem  9473  wofib  9585  cantnff  9714  cantnfp1  9721  cantnf  9733  cnfcomlem  9739  ttrcltr  9756  frr3g  9796  r1sscl  9825  rankval3b  9866  infxpidm2  10057  numdom  10078  onssnum  10080  acni  10085  acni2  10086  dfac5  10169  djulepw  10233  infunsdom1  10252  infunsdom  10253  cofsmo  10309  cfsmolem  10310  fin1ai  10333  fin2i  10335  isf34lem1  10412  fin67  10435  itunisuc  10459  axdc3lem4  10493  zornn0g  10545  ttukeylem6  10554  brdom3  10568  tsken  10794  tskcard  10821  r1tskina  10822  intgru  10854  prlem934  11073  ltexprlem7  11082  supaddc  12235  mul2lt0rlt0  13137  xrmaxeq  13221  xrmineq  13222  xmulneg1  13311  ixxun  13403  difelfzle  13681  ssfzoulel  13799  elfznelfzo  13811  ico01fl0  13859  btwnzge0  13868  ltdifltdiv  13874  ioopnfsup  13904  icopnfsup  13905  modifeq2int  13974  suppssfz  14035  expmordi  14207  zzlesq  14245  faclbnd4lem4  14335  hasheni  14387  hashgt0  14427  hashge1  14428  hashprb  14436  lennncl  14572  wrdsymb0  14587  ccatsymb  14620  ccatlid  14624  ccatass  14626  ccatswrd  14706  swrdccat2  14707  ccatpfx  14739  swrdccatfn  14762  swrdccat  14773  revccat  14804  2cshw  14851  cnpart  15279  resqreu  15291  recval  15361  abs1m  15374  abslem2  15378  fzomaxdiflem  15381  sqreulem  15398  sqreu  15399  limsupgre  15517  rlimdiv  15682  fsumparts  15842  climcnds  15887  expcnv  15900  ntrivcvg  15933  mod2eq1n2dvds  16384  ndvdssub  16446  sadcaddlem  16494  rplpwr  16595  dvdssqlem  16603  algcvgblem  16614  eucalgcvga  16623  isprm2lem  16718  powm2modprm  16841  coprimeprodsq  16846  pythagtriplem11  16863  pythagtriplem13  16865  pcadd2  16928  4sqlem11  16993  vdwlem6  17024  vdwlem8  17026  vdwlem10  17028  ramval  17046  ramcl2  17054  ramlb  17057  ram0  17060  mreintcl  17638  mrcval  17653  mrccl  17654  mrcuni  17664  mrcun  17665  acsfiel  17697  rescabs  17877  rescabsOLD  17878  funcres  17941  setcmon  18132  setcepi  18133  fullestrcsetc  18196  funcsetcestrclem8  18207  fullsetcestrc  18211  yonffthlem  18327  pleval2i  18381  pospo  18390  poslubdg  18459  acsdrsel  18588  acsdrscl  18591  acsficl  18592  psss  18625  grpidd  18684  ismndd  18769  gsumsgrpccat  18853  gsumwmhm  18858  mulgaddcom  19116  subgmulg  19158  resghm  19250  conjnsg  19272  ghmqusker  19305  f1otrspeq  19465  pmtrval  19469  pmtrrn  19475  pmtrfinv  19479  pmtrprfval  19505  psgnunilem1  19511  psgnunilem5  19512  psgnunilem4  19515  psgneldm2i  19523  lsmelvalix  19659  pj1ghm  19721  efgredlemc  19763  frgp0  19778  qusabl  19883  cycsubgcyg  19919  gsumval3  19925  gsumcllem  19926  ablfac1c  20091  pgpfac1lem5  20099  isrngd  20170  isringd  20288  01eq0ring  20530  lspsneq0b  21011  lmodindp1  21012  lmhmf1o  21045  lmhmpreima  21047  reslmhm  21051  pwssplit3  21060  lspsncmp  21118  lspsneq  21124  znf1o  21570  dsmmlss  21764  frlmlbs  21817  frlmup1  21818  psrgrp  21976  mpfind  22131  psdmul  22170  ply1scleq  22309  mat1  22453  chfacfisf  22860  chfacfisfcpmat  22861  uniopn  22903  ntrval  23044  clsval  23045  neival  23110  neiptopreu  23141  lpval  23147  restdis  23186  lmbrf  23268  cnpnei  23272  1stcrest  23461  hauspwdom  23509  lfinpfin  23532  txcnpi  23616  ptrescn  23647  xkococnlem  23667  qtopeu  23724  kqreglem1  23749  ptuncnv  23815  filss  23861  fsubbas  23875  fbasrn  23892  cfinfil  23901  ufinffr  23937  elfm3  23958  rnelfmlem  23960  rnelfm  23961  flimclslem  23992  flfval  23998  isfcf  24042  cnextfvval  24073  cnextf  24074  cnextcn  24075  ustelimasn  24231  trust  24238  restutop  24246  ustuqtop2  24251  utop2nei  24259  ucncn  24294  trcfilu  24303  cnextucn  24312  met1stc  24534  metustexhalf  24569  cfilucfil  24572  psmetutop  24580  nmoix  24750  nmoeq0  24757  idnghm  24764  blcvx  24819  xrsxmet  24831  iccntr  24843  icccmp  24847  iihalf1  24958  iihalf2  24961  xrhmeo  24977  cnheibor  24987  ipcau2  25268  lmmbrf  25296  iscauf  25314  cmetcaulem  25322  bcthlem4  25361  cmetcusp  25388  rrxcph  25426  minveclem4  25466  evthicc2  25495  cniccbdd  25496  ovollb2  25524  ovolunlem1a  25531  ovolunlem1  25532  voliun  25589  icombl  25599  ioombl  25600  iccvolcl  25602  ioovolcl  25605  mbfss  25681  mbfposb  25688  itg2const2  25776  itg2splitlem  25783  itg2gt0  25795  iblss2  25841  itgioo  25851  dvaddf  25979  dvmulf  25980  dvcobr  25983  dvcobrOLD  25984  dvcof  25986  rolle  26028  dvlip  26032  c1lip1  26036  dvivthlem1  26047  lhop1lem  26052  dvfsumlem1  26066  ftc1lem4  26080  ftc1lem5  26081  ply1divmo  26175  coe1termlem  26297  plydiveu  26340  taylplem1  26404  pserulm  26465  abelth  26485  abscxp2  26735  abscxpbnd  26796  logbgt0b  26836  ang180lem2  26853  ang180lem3  26854  isosctrlem1  26861  angpieqvd  26874  atandmtan  26963  birthdaylem3  26996  wilthlem2  27112  wilthimp  27115  isppw  27157  isppw2  27158  dvdsflsumcom  27231  chteq0  27253  perfectlem2  27274  dchrval  27278  dchrinvcl  27297  dchrptlem1  27308  bposlem3  27330  lgslem4  27344  lgsmod  27367  lgsdilem  27368  lgsdir2lem2  27370  lgsdir2  27374  lgsne0  27379  lgsmulsqcoprm  27387  lgseisenlem1  27419  2lgsoddprm  27460  2sqlem4  27465  chpo1ubb  27525  dchrisumn0  27565  pntrsumbnd2  27611  ostthlem1  27671  ostth3  27682  nosupbnd2lem1  27760  noinfbnd2lem1  27775  nocvxmin  27823  eqscut2  27851  sltlpss  27945  madefi  27950  absslt  28273  peano5uzs  28390  idmot  28545  tgelrnln  28638  lmimid  28802  lmiisolem  28804  hypcgrlem1  28807  brcgr  28915  colinearalglem4  28924  colinearalg  28925  axlowdimlem14  28970  axcontlem4  28982  cplgrop  29454  lfgriswlk  29706  pthdlem1  29786  crctcshwlkn0  29841  elwspths2on  29980  clwlkclwwlklem2fv2  30015  frgrncvvdeqlem9  30326  nvss  30612  sspn  30755  nmoub3i  30792  nmblolbii  30818  blocnilem  30823  minvecolem4  30899  htthlem  30936  norm1  31268  norm1exi  31269  pjeq  31418  axpjpj  31439  normcan  31595  pjoi0  31736  nmopub2tALT  31928  nmfnleub2  31945  eighmorth  31983  nmbdoplbi  32043  nmcoplbi  32047  nmophmi  32050  nmbdfnlbi  32068  nmcfnlbi  32071  riesz3i  32081  cnlnadjlem7  32092  branmfn  32124  nmopleid  32158  hstle  32249  superpos  32373  cvexchlem  32387  foresf1o  32523  elabreximd  32529  unidifsnne  32554  f1o3d  32637  fmptco1f1o  32643  funcnvmpt  32677  fgreu  32682  suppovss  32690  elsuppfnd  32691  fsupprnfi  32701  resf1o  32741  fpwrelmap  32744  xrofsup  32771  eliccelico  32779  elicoelioo  32780  iocinif  32783  difioo  32784  hashpss  32813  indf1ofs  32851  eliccioo  32913  cshf1o  32947  mgcmnt1d  32987  mgcmnt2d  32988  pwrssmgc  32990  chnind  33001  chnub  33002  chnccats1  33005  mndlactf1o  33035  mndractf1o  33036  gsummpt2co  33051  gsumhashmul  33064  submomnd  33087  symgcom  33103  symgcom2  33104  odpmco  33106  pmtrcnel  33109  pmtridf1o  33114  cycpmco2lem6  33151  cycpmco2lem7  33152  cycpmco2  33153  cyc3co2  33160  cycpmconjv  33162  tocyccntz  33164  cyc3evpm  33170  cycpmconjslem2  33175  cycpmconjs  33176  archirngz  33196  unitnz  33243  elrgspnlem1  33246  elrgspnlem2  33247  elrgspnlem4  33249  elrgspnsubrun  33253  rloccring  33274  rlocf1  33277  domnpropd  33280  rrgsubm  33287  isdrng4  33298  sdrgdvcl  33301  sdrginvcl  33302  fracfld  33310  ornglmullt  33337  orngrmullt  33338  lindssn  33406  linds2eq  33409  dvdsrspss  33415  nsgqusf1olem1  33441  nsgqusf1olem3  33443  unitpidl1  33452  elrspunidl  33456  rhmimaidl  33460  drngidlhash  33462  prmidl2  33469  prmidl0  33478  qsidomlem1  33480  ssdifidlprm  33486  mxidlirredi  33499  mxidlirred  33500  ssmxidl  33502  drng0mxidl  33504  opprmxidlabs  33515  qsdrngilem  33522  qsdrngi  33523  qsdrng  33525  rsprprmprmidl  33550  rsprprmprmidlb  33551  rprmasso2  33554  rprmirredlem  33558  rprmirredb  33560  1arithidomlem2  33564  1arithufdlem4  33575  1arithufd  33576  ply1asclunit  33599  ply1dg1rt  33604  ply1mulrtss  33606  ply1dg3rt0irred  33607  ply1degltlss  33617  ply1gsumz  33619  lsssra  33639  exsslsb  33647  lbslsat  33667  lindsunlem  33675  lindsun  33676  dimkerim  33678  fedgmullem1  33680  fedgmullem2  33681  fedgmul  33682  dimlssid  33683  lvecendof1f1o  33684  assalactf1o  33686  fldsdrgfldext  33712  fldgenfldext  33718  evls1fldgencl  33720  fldextrspunlsp  33724  fldextrspunlem1  33725  fldextrspunfld  33726  irngss  33737  0ringirng  33739  irngnzply1  33741  irngnminplynz  33755  irredminply  33757  algextdeglem2  33759  algextdeglem4  33761  constrconj  33786  constrextdg2lem  33789  madjusmdetlem2  33827  qtophaus  33835  locfinreflem  33839  zarclssn  33872  zarmxt1  33879  zarcmplem  33880  rhmpreimacn  33884  unitdivcld  33900  tpr2rico  33911  ordtrestNEW  33920  lmxrge0  33951  elzrhunit  33978  qqhf  33987  gsumesum  34060  esumfsup  34071  esumcvg  34087  issgon  34124  sigainb  34137  insiga  34138  isrnmeas  34201  measvunilem  34213  volmeas  34232  ddeval1  34235  ddeval0  34236  imambfm  34264  omssubadd  34302  carsgclctunlem3  34322  eulerpartlemf  34372  eulerpartlemgvv  34378  probun  34421  dstfrvunirn  34477  plymulx  34563  signslema  34577  signstfvn  34584  signsvtn0  34585  signstfvneq0  34587  signstres  34590  signstfveq0a  34591  breprexplemc  34647  logdivsqrle  34665  hgt750lemg  34669  tgoldbachgtda  34676  tgoldbachgt  34678  lpadmax  34697  lpadleft  34698  lpadright  34699  bnj529  34755  bnj548  34911  bnj570  34919  bnj852  34935  bnj929  34950  bnj1097  34995  bnj1118  34998  bnj1145  35007  funen1cnv  35102  spthcycl  35134  acycgr0v  35153  derangen  35177  subfacp1lem2b  35186  subfacp1lem4  35188  subfacp1lem5  35189  derangfmla  35195  ptpconn  35238  mppspstlem  35576  wsuclem  35826  colinearex  36061  btwnconn1lem11  36098  btwnconn1lem12  36099  fwddifnp1  36166  nn0prpwlem  36323  bj-snmoore  37114  bj-imdiridlem  37186  relowlpssretop  37365  fin2so  37614  matunitlindflem2  37624  ptrecube  37627  poimirlem8  37635  poimirlem13  37640  poimirlem15  37642  poimirlem24  37651  poimirlem25  37652  poimirlem26  37653  heicant  37662  mblfinlem2  37665  voliunnfl  37671  mbfresfi  37673  itg2addnclem  37678  itg2addnclem3  37680  itg2gt0cn  37682  ftc1cnnclem  37698  ftc1anclem5  37704  cover2  37722  indexdom  37741  sdclem1  37750  fdc  37752  equivbnd2  37799  heiborlem8  37825  heibor  37828  isdrngo2  37965  iscringd  38005  smprngopr  38059  prnc  38074  eqbrtr  38233  eqeltr  38235  islfld  39063  lkrshpor  39108  lfl1dim  39122  lfl1dim2N  39123  cmtcomlemN  39249  2lplnmN  39561  pmapjat1  39855  trlnid  40181  tendoex  40977  dia1dimid  41065  dibval2  41146  dihmeetlem2N  41301  dochlkr  41387  mapdcv  41662  hdmaplkr  41915  hdmapip0  41917  hlhillcs  41964  aks6d1c6lem4  42174  dvdsexpnn  42368  readvrec  42392  frlmvscadiccat  42516  psrmnd  42555  nacsfix  42723  3rexfrabdioph  42808  4rexfrabdioph  42809  6rexfrabdioph  42810  7rexfrabdioph  42811  eldioph4b  42822  pellexlem2  42841  pellexlem5  42844  jm2.26lem3  43013  numinfctb  43115  ordne0gt0  43274  omge1  43310  omlim2  43312  omord2lim  43313  omord2i  43314  tfsconcatfv  43354  tfsconcatb0  43357  oaun3lem1  43387  ntrclsfv1  44068  ntrneifv1  44092  ntrneifv2  44093  cvgdvgrat  44332  radcnvrat  44333  dvconstbi  44353  bccbc  44364  elpwgded  44584  elpwgdedVD  44937  sspwimpcf  44940  sspwimpcfVD  44941  sspwimpALT2  44948  ax6e2ndeqALT  44951  eliuniin  45104  eliuniin2  45125  qinioo  45548  dfxlim2v  45862  xlimliminflimsup  45877  cncfiooicclem1  45908  ibliooicc  45986  stoweidlem27  46042  stoweidlem28  46043  fourierdlem89  46210  fourierdlem91  46212  fourierdlem92  46213  smflimmpt  46825  odz2prm2pw  47550  perfectALTVlem2  47709  blen1b  48509  naryfvalelfv  48553  itscnhlc0yqe  48680  itsclquadb  48697  lubeldm2  48853  glbeldm2  48854  ipolub  48877  ipoglb  48880  fucofulem1  49005  functhinclem1  49093  thincciso  49102  prsthinc  49111  functermclem  49139  prstchom2ALT  49168  onetansqsecsq  49280  cotsqcscsq  49281  aacllem  49320