Theorem biimpar 483

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  bitr  817  exbiri  823  biadanid  835  bibiad  853  oplem1  1072  eqtr  2781  pm13.181  3038  opabss  5169  euotd  5486  brcogw  5846  somin1  6127  xpdifid  6159  xpdifcnvepel  6160  funfni  6645  fnssres  6662  fn0  6670  fnimadisj  6671  fnimaeq0  6672  foimacnv  6842  fvelimab  6957  dffv2  6980  fvopab3ig  6989  funcnvmpt  6995  dff3  7100  dffo4  7103  fpr2g  7217  ralima  7243  f1eqcocnv  7309  isomin  7345  f1ocnv2d  7674  fnexALT  7963  xp1st  8033  xp2nd  8034  frrlem3  8306  fpr2  8322  wfr3g  8337  wfr2  8345  iinon  8348  tfr3  8407  oawordri  8558  oaass  8569  omeulem1  8590  oeoa  8606  oeoe  8608  oeeulem  8610  elqsn0  8805  funen1cnv  9056  pwdom  9148  enfii  9201  phpeqd  9227  ominf  9255  findcard3  9274  fissorduni  9282  marypha1lem  9425  wofib  9539  cantnff  9675  cantnfp1  9682  cantnf  9694  cnfcomlem  9700  ttrcltr  9717  frr3g  9760  r1sscl  9792  rankval3b  9836  infxpidm2  10096  numdom  10117  onssnum  10119  acni  10124  acni2  10125  dfac5  10207  djulepw  10271  infunsdom1  10290  infunsdom  10291  cofsmo  10347  cfsmolem  10348  fin1ai  10371  fin2i  10373  isf34lem1  10450  fin67  10473  itunisuc  10497  axdc3lem4  10531  zornn0g  10583  ttukeylem6  10592  brdom3  10607  tsken  10839  tskcard  10866  r1tskina  10867  intgru  10899  prlem934  11118  ltexprlem7  11127  supaddc  12284  mul2lt0rlt0  13224  xrmaxeq  13309  xrmineq  13310  xmulneg1  13399  ixxun  13492  difelfzle  13775  ssfzoulel  13895  elfznelfzo  13908  ico01fl0  13959  btwnzge0  13968  ltdifltdiv  13974  ioopnfsup  14004  icopnfsup  14005  modifeq2int  14076  suppssfz  14137  expmordi  14310  zzlesq  14350  faclbnd4lem4  14440  hasheni  14492  hashgt0  14532  hashge1  14533  hashprb  14541  hashpss  14554  lennncl  14679  wrdsymb0  14694  ccatsymb  14728  ccatlid  14732  ccatass  14734  ccatswrd  14818  swrdccat2  14819  ccatpfx  14850  swrdccatfn  14873  swrdccat  14884  revccat  14915  2cshw  14964  cnpart  15407  resqreu  15419  recval  15490  abs1m  15503  abslem2  15507  fzomaxdiflem  15510  sqreulem  15527  sqreu  15528  limsupgre  15648  rlimdiv  15813  fsumparts  15973  climcnds  16020  expcnv  16033  ntrivcvg  16066  mod2eq1n2dvds  16517  ndvdssub  16579  sadcaddlem  16627  rplpwr  16732  dvdsexpnn  16740  algcvgblem  16752  eucalgcvga  16761  isprm2lem  16856  powm2modprm  16981  coprimeprodsq  16986  pythagtriplem11  17003  pythagtriplem13  17005  pcadd2  17068  4sqlem11  17133  vdwlem6  17164  vdwlem8  17166  vdwlem10  17168  ramval  17186  ramcl2  17194  ramlb  17197  ram0  17200  mreintcl  17765  mrcval  17784  mrccl  17785  mrcuni  17795  mrcun  17796  acsfiel  17828  rescabs  18008  funcres  18071  setcmon  18262  setcepi  18263  fullestrcsetc  18325  funcsetcestrclem8  18336  fullsetcestrc  18340  yonffthlem  18456  pleval2i  18508  pospo  18517  poslubdg  18586  acsdrsel  18717  acsdrscl  18720  acsficl  18721  psss  18754  chnind  18795  chnub  18796  chnccats1  18799  chnccat  18800  grpidd  18852  ismndd  18946  gsumsgrpccat  19036  gsumwmhm  19041  mulgaddcom  19308  subgmulg  19351  resghm  19446  conjnsg  19468  ghmqusker  19501  f1otrspeq  19661  pmtrval  19665  pmtrrn  19671  pmtrfinv  19675  pmtrprfval  19701  psgnunilem1  19707  psgnunilem5  19708  psgnunilem4  19711  psgneldm2i  19719  lsmelvalix  19855  pj1ghm  19917  efgredlemc  19959  frgp0  19974  qusabl  20079  cycsubgcyg  20115  gsumval3  20121  gsumcllem  20122  ablfac1c  20287  pgpfac1lem5  20295  submomnd  20346  isrngd  20395  isringd  20522  01eq0ring  20781  isdrng4  20992  ornglmullt  21126  orngrmullt  21127  lspsneq0b  21288  lmodindp1  21289  lmhmf1o  21321  lmhmpreima  21323  reslmhm  21327  pwssplit3  21336  lspsncmp  21394  lspsneq  21400  prmidl2  21622  prmidl0  21634  qsidomlem1  21636  ssdifidlprm  21642  prmidlsubm  21643  znf1o  21857  dsmmlss  22050  frlmlbs  22103  frlmup1  22104  psrgrp  22264  mpfind  22424  psdmul  22487  ply1scleq  22623  mat1  22762  matunitlindflem2  22995  chfacfisf  23172  chfacfisfcpmat  23173  uniopn  23215  ntrval  23354  clsval  23355  neival  23420  neiptopreu  23451  lpval  23457  restdis  23496  lmbrf  23578  cnpnei  23582  1stcrest  23771  hauspwdom  23820  lfinpfin  23843  txcnpi  23927  ptrescn  23958  xkococnlem  23978  qtopeu  24035  kqreglem1  24060  ptuncnv  24126  filss  24172  fsubbas  24186  fbasrn  24203  cfinfil  24212  ufinffr  24248  elfm3  24269  rnelfmlem  24271  rnelfm  24272  flimclslem  24303  flfval  24309  isfcf  24353  cnextfvval  24384  cnextf  24385  cnextcn  24386  ustelimasn  24542  trust  24548  restutop  24556  ustuqtop2  24561  utop2nei  24569  ucncn  24603  trcfilu  24612  cnextucn  24621  met1stc  24840  metustexhalf  24875  cfilucfil  24878  psmetutop  24886  nmoix  25048  nmoeq0  25055  idnghm  25062  blcvx  25117  xrsxmet  25129  iccntr  25141  icccmp  25145  iihalf1  25252  iihalf2  25254  xrhmeo  25267  cnheibor  25276  ipcau2  25555  lmmbrf  25583  iscauf  25601  cmetcaulem  25609  bcthlem4  25648  cmetcusp  25675  rrxcph  25713  minveclem4  25753  evthicc2  25781  cniccbdd  25782  ovollb2  25810  ovolunlem1a  25817  ovolunlem1  25818  voliun  25875  icombl  25885  ioombl  25886  iccvolcl  25888  ioovolcl  25891  mbfss  25967  mbfposb  25974  itg2const2  26062  itg2splitlem  26069  itg2gt0  26081  iblss2  26126  itgioo  26136  dvaddf  26262  dvmulf  26263  dvcobr  26266  dvcof  26268  rolle  26310  dvlip  26313  c1lip1  26317  dvivthlem1  26328  lhop1lem  26333  dvfsumlem1  26346  ftc1lem4  26359  ftc1lem5  26360  ply1divmo  26454  coe1termlem  26577  plymulidp  26603  plydiveu  26619  taylplem1  26690  pserulm  26749  abelth  26768  abscxp2  27021  abscxpbnd  27081  logbgt0b  27121  ang180lem2  27138  ang180lem3  27139  isosctrlem1  27146  angpieqvd  27159  atandmtan  27248  birthdaylem3  27281  wilthlem2  27396  wilthimp  27399  isppw  27441  isppw2  27442  dvdsflsumcom  27515  chteq0  27536  perfectlem2  27557  dchrval  27561  dchrinvcl  27580  dchrptlem1  27591  bposlem3  27613  lgslem4  27627  lgsmod  27650  lgsdilem  27651  lgsdir2lem2  27653  lgsdir2  27657  lgsne0  27662  lgsmulsqcoprm  27670  lgseisenlem1  27702  2lgsoddprm  27743  2sqlem4  27748  chpo1ubb  27808  dchrisumn0  27848  pntrsumbnd2  27894  ostthlem1  27954  ostth3  27965  nosupbnd2lem1  28072  noinfbnd2lem1  28087  nocvxmin  28141  eqcuts2  28172  ltslpss  28294  madefi  28299  abslts  28635  eucliddivs  28762  peano5uzs  28790  z12bdaylem1  28856  elreno2  28881  idmot  29000  tgelrnln  29098  lnincplng  29262  plngmiropp  29272  lmimid  29299  lmiisolem  29301  hypcgrlem1  29305  brcgr  29478  colinearalglem4  29487  colinearalg  29488  axlowdimlem14  29533  axcontlem4  29545  cplgrop  30018  lfgriswlk  30271  pthdlem1  30352  spthcycl  30392  crctcshwlkn0  30410  elwspths2on  30551  elwspths2onw  30552  clwlkclwwlklem2fv2  30587  frgrncvvdeqlem9  30908  nvss  31195  sspn  31338  nmoub3i  31375  nmblolbii  31401  blocnilem  31406  minvecolem4  31482  htthlem  31519  norm1  31851  norm1exi  31852  pjeq  32001  axpjpj  32022  normcan  32178  pjoi0  32319  nmopub2tALT  32511  nmfnleub2  32528  eighmorth  32566  nmbdoplbi  32626  nmcoplbi  32630  nmophmi  32633  nmbdfnlbi  32651  nmcfnlbi  32654  riesz3i  32664  cnlnadjlem7  32675  branmfn  32707  nmopleid  32741  hstle  32832  superpos  32956  cvexchlem  32970  foresf1o  33100  elabreximd  33106  prssad  33125  prssbd  33126  unidifsnne  33132  tpssad  33135  fresunsn  33219  f1o3d  33220  fmptco1f1o  33227  fgreu  33265  suppovss  33274  elsuppfnd  33275  fsupprnfi  33285  resf1o  33322  fpwrelmap  33325  argcj  33340  xrofsup  33359  eliccelico  33369  elicoelioo  33370  iocinif  33373  difioo  33374  hashne0  33401  elq2  33403  oexpled  33427  indf1ofs  33433  eliccioo  33497  cshf1o  33523  mgcmnt1d  33558  mgcmnt2d  33559  pwrssmgc  33561  mndlactf1o  33591  mndractf1o  33592  gsummpt2co  33609  gsumhashmul  33628  gsummulsubdishift1  33629  symgcom  33644  symgcom2  33645  odpmco  33647  pmtrcnel  33650  pmtridf1o  33655  cycpmco2lem6  33692  cycpmco2lem7  33693  cycpmco2  33694  cyc3co2  33701  cycpmconjv  33703  tocyccntz  33705  cyc3evpm  33711  cycpmconjslem2  33716  cycpmconjs  33717  fxpsubm  33733  fxpsubg  33734  fxpsubrg  33735  fxpsdrg  33736  archirngz  33750  unitnz  33799  elrgspnlem1  33803  elrgspnlem2  33804  elrgspnlem4  33806  elrgspnsubrun  33810  rloccring  33832  rlocf1  33835  rlocisunit  33837  domnpropd  33841  rrgsubm  33845  sdrgdvcl  33861  sdrginvcl  33862  fracfld  33870  lindssn  33933  linds2eq  33936  dvdsrspss  33942  nsgqusf1olem1  33964  nsgqusf1olem3  33966  unitpidl1  33974  elrspunidl  33978  rhmimaidl  33982  drngidlhash  33983  mxidlirredi  33996  mxidlirred  33997  ssmxidl  33999  drng0mxidl  34000  opprmxidlabs  34011  qsdrngilem  34018  qsdrngi  34019  qsdrng  34021  drnglring  34024  dflring2  34025  dflringlem  34026  dflringlem3  34028  dflring4  34030  fldlring  34031  rsprprmprmidl  34054  rsprprmprmidlb  34055  rprmasso2  34058  rprmirredlem  34062  rprmirredb  34064  1arithidomlem2  34068  1arithufdlem4  34079  1arithufd  34080  ressply1evls1  34097  ply1asclunit  34106  ply1dg1rt  34112  ply1mulrtss  34114  ply1dg3rt0irred  34116  ply1degltlss  34128  ply1gsumz  34131  mplidomlem  34159  evlextv  34174  esplyfv1  34201  esplyind  34207  vietadeg1  34210  lsssra  34220  exsslsb  34229  lbslsat  34248  lindsunlem  34256  lindsun  34257  dimkerim  34259  fedgmullem1  34261  fedgmullem2  34262  fedgmul  34263  dimlssid  34264  lvecendof1f1o  34265  assalactf1o  34267  sdrgfldext  34282  fldsdrgfldext  34293  fldgenfldext  34300  evls1fldgencl  34302  fldextrspunlsp  34306  fldextrspunlem1  34307  fldextrspunfld  34308  irngss  34319  0ringirng  34321  irngnzply1  34323  extdgfialglem1  34324  irngnminplynz  34344  minplyelirng  34347  irredminply  34348  algextdeglem2  34350  algextdeglem4  34352  constrconj  34377  constrextdg2lem  34380  constrext2chnlem  34382  iconstr  34398  constrsdrg  34407  cos9thpiminplylem1  34414  cos9thpiminplylem2  34415  cos9thpiminplylem3  34416  cos9thpiminplylem5  34418  madjusmdetlem2  34460  qtophaus  34468  locfinreflem  34472  zarclssn  34505  zarmxt1  34512  zarcmplem  34513  rhmpreimacn  34517  unitdivcld  34533  tpr2rico  34544  ordtrestNEW  34553  lmxrge0  34584  elzrhunit  34609  qqhf  34618  gsumesum  34691  esumfsup  34702  esumcvg  34718  issgon  34755  sigainb  34769  insiga  34770  isrnmeas  34833  measvunilem  34845  volmeas  34864  ddeval1  34867  ddeval0  34868  imambfm  34894  omssubadd  34932  carsgclctunlem3  34952  eulerpartlemf  35002  eulerpartlemgvv  35008  probun  35051  dstfrvunirn  35107  signslema  35191  signstfvn  35198  signsvtn0  35199  signstfvneq0  35201  signstres  35204  signstfveq0a  35205  breprexplemc  35261  logdivsqrle  35279  hgt750lemg  35283  tgoldbachgtda  35290  tgoldbachgt  35292  lpadmax  35314  lpadleft  35315  lpadright  35316  bnj529  35372  bnj548  35527  bnj570  35535  bnj852  35551  bnj929  35566  bnj1097  35611  bnj1118  35614  bnj1145  35623  acwer1prclem  35759  vonf1oonfo  35898  acycgr0v  35913  derangen  35937  subfacp1lem2b  35946  subfacp1lem4  35948  subfacp1lem5  35949  derangfmla  35955  ptpconn  35998  mppspstlem  36336  wsuclem  36587  colinearex  36825  btwnconn1lem11  36862  btwnconn1lem12  36863  fwddifnp1  36930  nn0prpwlem  37110  ttctr  37281  dfttc2g  37294  regsfromregtco  37326  bj-snmoore  38034  bj-imdiridlem  38106  relowlpssretop  38287  fin2so  38530  ptrecube  38538  poimirlem8  38546  poimirlem13  38551  poimirlem15  38553  poimirlem24  38562  poimirlem25  38563  poimirlem26  38564  heicant  38573  mblfinlem2  38576  voliunnfl  38582  mbfresfi  38584  itg2addnclem  38589  itg2addnclem3  38591  itg2gt0cn  38593  ftc1cnnclem  38609  ftc1anclem5  38615  cover2  38649  indexdom  38668  sdclem1  38677  fdc  38679  equivbnd2  38726  heiborlem8  38752  heibor  38755  isdrngo2  38892  iscringd  38932  smprngopr  38986  prnc  39001  eqbrtr  39170  eqeltr  39172  islfld  40119  lkrshpor  40164  lfl1dim  40178  lfl1dim2N  40179  cmtcomlemN  40305  2lplnmN  40616  pmapjat1  40910  trlnid  41236  tendoex  42032  dia1dimid  42120  dibval2  42201  dihmeetlem2N  42356  dochlkr  42442  mapdcv  42717  hdmaplkr  42970  hdmapip0  42972  hlhillcs  43015  aks6d1c6lem4  43223  readvrec  43413  frlmvscadiccat  43573  psrmnd  43607  nacsfix  43722  3rexfrabdioph  43803  4rexfrabdioph  43804  6rexfrabdioph  43805  7rexfrabdioph  43806  eldioph4b  43817  pellexlem2  43836  pellexlem5  43839  jm2.26lem3  44007  numinfctb  44104  ordne0gt0  44262  omge1  44298  omlim2  44300  omord2lim  44301  omord2i  44302  tfsconcatfv  44342  tfsconcatb0  44345  oaun3lem1  44375  ntrclsfv1  45054  ntrneifv1  45078  ntrneifv2  45079  cvgdvgrat  45296  radcnvrat  45297  dvconstbi  45317  bccbc  45328  elpwgded  45546  elpwgdedVD  45898  sspwimpcf  45901  sspwimpcfVD  45902  sspwimpALT2  45909  ax6e2ndeqALT  45912  eliuniin  46113  eliuniin2  46134  qinioo  46546  dfxlim2v  46856  xlimliminflimsup  46871  cncfiooicclem1  46902  ibliooicc  46980  stoweidlem27  47036  stoweidlem28  47037  fourierdlem89  47204  fourierdlem91  47206  fourierdlem92  47207  smflimmpt  47819  tmachlem-agreesn  47956  odz2prm2pw  48647  perfectALTVlem2  48819  blen1b  49699  naryfvalelfv  49743  itscnhlc0yqe  49870  itsclquadb  49887  lubeldm2  50063  glbeldm2  50064  ipolub  50095  ipoglb  50098  fucofulem1  50417  functhinclem1  50551  thincciso  50560  prsthinc  50571  functermclem  50614  prstchom2ALT  50671  onetansqsecsq  50853  cotsqcscsq  50854  aacllem  50938