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  bibiad  839  oplem1  1056  eqtr  2750  pm13.181  3008  opabss  5174  axprlem4OLD  5387  axprlem5OLD  5388  euotd  5476  brcogw  5835  somin1  6109  xpdifid  6144  funfni  6627  fnssres  6644  fn0  6652  fnimadisj  6653  fnimaeq0  6654  foimacnv  6820  fvelimab  6936  dffv2  6959  fvopab3ig  6967  dff3  7075  dffo4  7078  fpr2g  7188  ralima  7214  f1eqcocnv  7279  isomin  7315  f1ocnv2d  7645  fnexALT  7932  xp1st  8003  xp2nd  8004  frrlem3  8270  fpr2  8286  wfr3g  8301  wfr2  8309  iinon  8312  tfr3  8370  oawordri  8517  oaass  8528  omeulem1  8549  oeoa  8564  oeoe  8566  oeeulem  8568  elqsn0  8760  pwdom  9099  enfii  9156  phpeqd  9182  ominf  9212  findcard3  9236  marypha1lem  9391  wofib  9505  cantnff  9634  cantnfp1  9641  cantnf  9653  cnfcomlem  9659  ttrcltr  9676  frr3g  9716  r1sscl  9745  rankval3b  9786  infxpidm2  9977  numdom  9998  onssnum  10000  acni  10005  acni2  10006  dfac5  10089  djulepw  10153  infunsdom1  10172  infunsdom  10173  cofsmo  10229  cfsmolem  10230  fin1ai  10253  fin2i  10255  isf34lem1  10332  fin67  10355  itunisuc  10379  axdc3lem4  10413  zornn0g  10465  ttukeylem6  10474  brdom3  10488  tsken  10714  tskcard  10741  r1tskina  10742  intgru  10774  prlem934  10993  ltexprlem7  11002  supaddc  12157  mul2lt0rlt0  13062  xrmaxeq  13146  xrmineq  13147  xmulneg1  13236  ixxun  13329  difelfzle  13609  ssfzoulel  13728  elfznelfzo  13740  ico01fl0  13788  btwnzge0  13797  ltdifltdiv  13803  ioopnfsup  13833  icopnfsup  13834  modifeq2int  13905  suppssfz  13966  expmordi  14139  zzlesq  14178  faclbnd4lem4  14268  hasheni  14320  hashgt0  14360  hashge1  14361  hashprb  14369  lennncl  14506  wrdsymb0  14521  ccatsymb  14554  ccatlid  14558  ccatass  14560  ccatswrd  14640  swrdccat2  14641  ccatpfx  14673  swrdccatfn  14696  swrdccat  14707  revccat  14738  2cshw  14785  cnpart  15213  resqreu  15225  recval  15296  abs1m  15309  abslem2  15313  fzomaxdiflem  15316  sqreulem  15333  sqreu  15334  limsupgre  15454  rlimdiv  15619  fsumparts  15779  climcnds  15824  expcnv  15837  ntrivcvg  15870  mod2eq1n2dvds  16324  ndvdssub  16386  sadcaddlem  16434  rplpwr  16535  dvdssqlem  16543  algcvgblem  16554  eucalgcvga  16563  isprm2lem  16658  powm2modprm  16781  coprimeprodsq  16786  pythagtriplem11  16803  pythagtriplem13  16805  pcadd2  16868  4sqlem11  16933  vdwlem6  16964  vdwlem8  16966  vdwlem10  16968  ramval  16986  ramcl2  16994  ramlb  16997  ram0  17000  mreintcl  17563  mrcval  17578  mrccl  17579  mrcuni  17589  mrcun  17590  acsfiel  17622  rescabs  17802  funcres  17865  setcmon  18056  setcepi  18057  fullestrcsetc  18119  funcsetcestrclem8  18130  fullsetcestrc  18134  yonffthlem  18250  pleval2i  18302  pospo  18311  poslubdg  18380  acsdrsel  18509  acsdrscl  18512  acsficl  18513  psss  18546  grpidd  18605  ismndd  18690  gsumsgrpccat  18774  gsumwmhm  18779  mulgaddcom  19037  subgmulg  19079  resghm  19171  conjnsg  19193  ghmqusker  19226  f1otrspeq  19384  pmtrval  19388  pmtrrn  19394  pmtrfinv  19398  pmtrprfval  19424  psgnunilem1  19430  psgnunilem5  19431  psgnunilem4  19434  psgneldm2i  19442  lsmelvalix  19578  pj1ghm  19640  efgredlemc  19682  frgp0  19697  qusabl  19802  cycsubgcyg  19838  gsumval3  19844  gsumcllem  19845  ablfac1c  20010  pgpfac1lem5  20018  isrngd  20089  isringd  20207  01eq0ring  20446  lspsneq0b  20926  lmodindp1  20927  lmhmf1o  20960  lmhmpreima  20962  reslmhm  20966  pwssplit3  20975  lspsncmp  21033  lspsneq  21039  znf1o  21468  dsmmlss  21660  frlmlbs  21713  frlmup1  21714  psrgrp  21872  mpfind  22021  psdmul  22060  ply1scleq  22199  mat1  22341  chfacfisf  22748  chfacfisfcpmat  22749  uniopn  22791  ntrval  22930  clsval  22931  neival  22996  neiptopreu  23027  lpval  23033  restdis  23072  lmbrf  23154  cnpnei  23158  1stcrest  23347  hauspwdom  23395  lfinpfin  23418  txcnpi  23502  ptrescn  23533  xkococnlem  23553  qtopeu  23610  kqreglem1  23635  ptuncnv  23701  filss  23747  fsubbas  23761  fbasrn  23778  cfinfil  23787  ufinffr  23823  elfm3  23844  rnelfmlem  23846  rnelfm  23847  flimclslem  23878  flfval  23884  isfcf  23928  cnextfvval  23959  cnextf  23960  cnextcn  23961  ustelimasn  24117  trust  24124  restutop  24132  ustuqtop2  24137  utop2nei  24145  ucncn  24179  trcfilu  24188  cnextucn  24197  met1stc  24416  metustexhalf  24451  cfilucfil  24454  psmetutop  24462  nmoix  24624  nmoeq0  24631  idnghm  24638  blcvx  24693  xrsxmet  24705  iccntr  24717  icccmp  24721  iihalf1  24832  iihalf2  24835  xrhmeo  24851  cnheibor  24861  ipcau2  25141  lmmbrf  25169  iscauf  25187  cmetcaulem  25195  bcthlem4  25234  cmetcusp  25261  rrxcph  25299  minveclem4  25339  evthicc2  25368  cniccbdd  25369  ovollb2  25397  ovolunlem1a  25404  ovolunlem1  25405  voliun  25462  icombl  25472  ioombl  25473  iccvolcl  25475  ioovolcl  25478  mbfss  25554  mbfposb  25561  itg2const2  25649  itg2splitlem  25656  itg2gt0  25668  iblss2  25714  itgioo  25724  dvaddf  25852  dvmulf  25853  dvcobr  25856  dvcobrOLD  25857  dvcof  25859  rolle  25901  dvlip  25905  c1lip1  25909  dvivthlem1  25920  lhop1lem  25925  dvfsumlem1  25939  ftc1lem4  25953  ftc1lem5  25954  ply1divmo  26048  coe1termlem  26170  plydiveu  26213  taylplem1  26277  pserulm  26338  abelth  26358  abscxp2  26609  abscxpbnd  26670  logbgt0b  26710  ang180lem2  26727  ang180lem3  26728  isosctrlem1  26735  angpieqvd  26748  atandmtan  26837  birthdaylem3  26870  wilthlem2  26986  wilthimp  26989  isppw  27031  isppw2  27032  dvdsflsumcom  27105  chteq0  27127  perfectlem2  27148  dchrval  27152  dchrinvcl  27171  dchrptlem1  27182  bposlem3  27204  lgslem4  27218  lgsmod  27241  lgsdilem  27242  lgsdir2lem2  27244  lgsdir2  27248  lgsne0  27253  lgsmulsqcoprm  27261  lgseisenlem1  27293  2lgsoddprm  27334  2sqlem4  27339  chpo1ubb  27399  dchrisumn0  27439  pntrsumbnd2  27485  ostthlem1  27545  ostth3  27556  nosupbnd2lem1  27634  noinfbnd2lem1  27649  nocvxmin  27697  eqscut2  27725  sltlpss  27826  madefi  27831  absslt  28158  eucliddivs  28272  peano5uzs  28299  idmot  28471  tgelrnln  28564  lmimid  28728  lmiisolem  28730  hypcgrlem1  28733  brcgr  28834  colinearalglem4  28843  colinearalg  28844  axlowdimlem14  28889  axcontlem4  28901  cplgrop  29371  lfgriswlk  29623  pthdlem1  29703  crctcshwlkn0  29758  elwspths2on  29897  clwlkclwwlklem2fv2  29932  frgrncvvdeqlem9  30243  nvss  30529  sspn  30672  nmoub3i  30709  nmblolbii  30735  blocnilem  30740  minvecolem4  30816  htthlem  30853  norm1  31185  norm1exi  31186  pjeq  31335  axpjpj  31356  normcan  31512  pjoi0  31653  nmopub2tALT  31845  nmfnleub2  31862  eighmorth  31900  nmbdoplbi  31960  nmcoplbi  31964  nmophmi  31967  nmbdfnlbi  31985  nmcfnlbi  31988  riesz3i  31998  cnlnadjlem7  32009  branmfn  32041  nmopleid  32075  hstle  32166  superpos  32290  cvexchlem  32304  foresf1o  32440  elabreximd  32446  prssad  32465  prssbd  32466  unidifsnne  32472  tpssad  32475  f1o3d  32558  fmptco1f1o  32564  funcnvmpt  32598  fgreu  32603  suppovss  32611  elsuppfnd  32612  fsupprnfi  32622  resf1o  32660  fpwrelmap  32663  argcj  32679  xrofsup  32697  eliccelico  32707  elicoelioo  32708  iocinif  32711  difioo  32712  hashpss  32741  hashne0  32742  elq2  32743  oexpled  32779  indf1ofs  32796  eliccioo  32858  cshf1o  32891  mgcmnt1d  32930  mgcmnt2d  32931  pwrssmgc  32933  chnind  32944  chnub  32945  chnccats1  32948  mndlactf1o  32978  mndractf1o  32979  gsummpt2co  32995  gsumhashmul  33008  submomnd  33031  symgcom  33047  symgcom2  33048  odpmco  33050  pmtrcnel  33053  pmtridf1o  33058  cycpmco2lem6  33095  cycpmco2lem7  33096  cycpmco2  33097  cyc3co2  33104  cycpmconjv  33106  tocyccntz  33108  cyc3evpm  33114  cycpmconjslem2  33119  cycpmconjs  33120  fxpsubm  33136  archirngz  33150  unitnz  33197  elrgspnlem1  33200  elrgspnlem2  33201  elrgspnlem4  33203  elrgspnsubrun  33207  rloccring  33228  rlocf1  33231  domnpropd  33234  rrgsubm  33241  isdrng4  33252  sdrgdvcl  33256  sdrginvcl  33257  fracfld  33265  ornglmullt  33292  orngrmullt  33293  lindssn  33356  linds2eq  33359  dvdsrspss  33365  nsgqusf1olem1  33391  nsgqusf1olem3  33393  unitpidl1  33402  elrspunidl  33406  rhmimaidl  33410  drngidlhash  33412  prmidl2  33419  prmidl0  33428  qsidomlem1  33430  ssdifidlprm  33436  mxidlirredi  33449  mxidlirred  33450  ssmxidl  33452  drng0mxidl  33454  opprmxidlabs  33465  qsdrngilem  33472  qsdrngi  33473  qsdrng  33475  rsprprmprmidl  33500  rsprprmprmidlb  33501  rprmasso2  33504  rprmirredlem  33508  rprmirredb  33510  1arithidomlem2  33514  1arithufdlem4  33525  1arithufd  33526  ressply1evls1  33541  ply1asclunit  33550  ply1dg1rt  33555  ply1mulrtss  33557  ply1dg3rt0irred  33558  ply1degltlss  33569  ply1gsumz  33571  lsssra  33591  exsslsb  33599  lbslsat  33619  lindsunlem  33627  lindsun  33628  dimkerim  33630  fedgmullem1  33632  fedgmullem2  33633  fedgmul  33634  dimlssid  33635  lvecendof1f1o  33636  assalactf1o  33638  sdrgfldext  33653  fldsdrgfldext  33664  fldgenfldext  33670  evls1fldgencl  33672  fldextrspunlsp  33676  fldextrspunlem1  33677  fldextrspunfld  33678  irngss  33689  0ringirng  33691  irngnzply1  33693  irngnminplynz  33709  minplyelirng  33712  irredminply  33713  algextdeglem2  33715  algextdeglem4  33717  constrconj  33742  constrextdg2lem  33745  constrext2chnlem  33747  iconstr  33763  constrsdrg  33772  cos9thpiminplylem1  33779  cos9thpiminplylem2  33780  cos9thpiminplylem3  33781  cos9thpiminplylem5  33783  madjusmdetlem2  33825  qtophaus  33833  locfinreflem  33837  zarclssn  33870  zarmxt1  33877  zarcmplem  33878  rhmpreimacn  33882  unitdivcld  33898  tpr2rico  33909  ordtrestNEW  33918  lmxrge0  33949  elzrhunit  33974  qqhf  33983  gsumesum  34056  esumfsup  34067  esumcvg  34083  issgon  34120  sigainb  34133  insiga  34134  isrnmeas  34197  measvunilem  34209  volmeas  34228  ddeval1  34231  ddeval0  34232  imambfm  34260  omssubadd  34298  carsgclctunlem3  34318  eulerpartlemf  34368  eulerpartlemgvv  34374  probun  34417  dstfrvunirn  34473  plymulx  34546  signslema  34560  signstfvn  34567  signsvtn0  34568  signstfvneq0  34570  signstres  34573  signstfveq0a  34574  breprexplemc  34630  logdivsqrle  34648  hgt750lemg  34652  tgoldbachgtda  34659  tgoldbachgt  34661  lpadmax  34680  lpadleft  34681  lpadright  34682  bnj529  34738  bnj548  34894  bnj570  34902  bnj852  34918  bnj929  34933  bnj1097  34978  bnj1118  34981  bnj1145  34990  funen1cnv  35085  spthcycl  35123  acycgr0v  35142  derangen  35166  subfacp1lem2b  35175  subfacp1lem4  35177  subfacp1lem5  35178  derangfmla  35184  ptpconn  35227  mppspstlem  35565  wsuclem  35820  colinearex  36055  btwnconn1lem11  36092  btwnconn1lem12  36093  fwddifnp1  36160  nn0prpwlem  36317  bj-snmoore  37108  bj-imdiridlem  37180  relowlpssretop  37359  fin2so  37608  matunitlindflem2  37618  ptrecube  37621  poimirlem8  37629  poimirlem13  37634  poimirlem15  37636  poimirlem24  37645  poimirlem25  37646  poimirlem26  37647  heicant  37656  mblfinlem2  37659  voliunnfl  37665  mbfresfi  37667  itg2addnclem  37672  itg2addnclem3  37674  itg2gt0cn  37676  ftc1cnnclem  37692  ftc1anclem5  37698  cover2  37716  indexdom  37735  sdclem1  37744  fdc  37746  equivbnd2  37793  heiborlem8  37819  heibor  37822  isdrngo2  37959  iscringd  37999  smprngopr  38053  prnc  38068  eqbrtr  38227  eqeltr  38229  islfld  39062  lkrshpor  39107  lfl1dim  39121  lfl1dim2N  39122  cmtcomlemN  39248  2lplnmN  39560  pmapjat1  39854  trlnid  40180  tendoex  40976  dia1dimid  41064  dibval2  41145  dihmeetlem2N  41300  dochlkr  41386  mapdcv  41661  hdmaplkr  41914  hdmapip0  41916  hlhillcs  41959  aks6d1c6lem4  42168  dvdsexpnn  42328  readvrec  42357  frlmvscadiccat  42501  psrmnd  42540  nacsfix  42707  3rexfrabdioph  42792  4rexfrabdioph  42793  6rexfrabdioph  42794  7rexfrabdioph  42795  eldioph4b  42806  pellexlem2  42825  pellexlem5  42828  jm2.26lem3  42997  numinfctb  43099  ordne0gt0  43257  omge1  43293  omlim2  43295  omord2lim  43296  omord2i  43297  tfsconcatfv  43337  tfsconcatb0  43340  oaun3lem1  43370  ntrclsfv1  44051  ntrneifv1  44075  ntrneifv2  44076  cvgdvgrat  44309  radcnvrat  44310  dvconstbi  44330  bccbc  44341  elpwgded  44561  elpwgdedVD  44913  sspwimpcf  44916  sspwimpcfVD  44917  sspwimpALT2  44924  ax6e2ndeqALT  44927  eliuniin  45100  eliuniin2  45121  qinioo  45540  dfxlim2v  45852  xlimliminflimsup  45867  cncfiooicclem1  45898  ibliooicc  45976  stoweidlem27  46032  stoweidlem28  46033  fourierdlem89  46200  fourierdlem91  46202  fourierdlem92  46203  smflimmpt  46815  odz2prm2pw  47568  perfectALTVlem2  47727  blen1b  48581  naryfvalelfv  48625  itscnhlc0yqe  48752  itsclquadb  48769  lubeldm2  48948  glbeldm2  48949  ipolub  48980  ipoglb  48983  fucofulem1  49303  functhinclem1  49437  thincciso  49446  prsthinc  49457  functermclem  49500  prstchom2ALT  49557  onetansqsecsq  49754  cotsqcscsq  49755  aacllem  49794