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  2780  pm13.181  3037  opabss  5169  axprlem4OLD  5395  axprlem5OLD  5396  euotd  5490  brcogw  5848  somin1  6127  xpdifid  6160  xpdifcnvepel  6161  funfni  6639  fnssres  6656  fn0  6664  fnimadisj  6665  fnimaeq0  6666  foimacnv  6836  fvelimab  6951  dffv2  6974  fvopab3ig  6983  funcnvmpt  6989  dff3  7094  dffo4  7097  fpr2g  7211  ralima  7237  f1eqcocnv  7303  isomin  7339  f1ocnv2d  7668  fnexALT  7949  xp1st  8019  xp2nd  8020  frrlem3  8288  fpr2  8304  wfr3g  8319  wfr2  8327  iinon  8330  tfr3  8389  oawordri  8540  oaass  8551  omeulem1  8572  oeoa  8588  oeoe  8590  oeeulem  8592  elqsn0  8787  funen1cnv  9038  pwdom  9130  enfii  9183  phpeqd  9209  ominf  9237  findcard3  9256  marypha1lem  9406  wofib  9520  cantnff  9656  cantnfp1  9663  cantnf  9675  cnfcomlem  9681  ttrcltr  9698  frr3g  9741  r1sscl  9770  rankval3b  9811  infxpidm2  10023  numdom  10044  onssnum  10046  acni  10051  acni2  10052  dfac5  10134  djulepw  10198  infunsdom1  10217  infunsdom  10218  cofsmo  10274  cfsmolem  10275  fin1ai  10298  fin2i  10300  isf34lem1  10377  fin67  10400  itunisuc  10424  axdc3lem4  10458  zornn0g  10510  ttukeylem6  10519  brdom3  10534  tsken  10766  tskcard  10793  r1tskina  10794  intgru  10826  prlem934  11045  ltexprlem7  11054  supaddc  12209  mul2lt0rlt0  13149  xrmaxeq  13234  xrmineq  13235  xmulneg1  13324  ixxun  13417  difelfzle  13699  ssfzoulel  13819  elfznelfzo  13832  ico01fl0  13883  btwnzge0  13892  ltdifltdiv  13898  ioopnfsup  13928  icopnfsup  13929  modifeq2int  14000  suppssfz  14061  expmordi  14234  zzlesq  14273  faclbnd4lem4  14363  hasheni  14415  hashgt0  14455  hashge1  14456  hashprb  14464  hashpss  14477  lennncl  14602  wrdsymb0  14617  ccatsymb  14651  ccatlid  14655  ccatass  14657  ccatswrd  14741  swrdccat2  14742  ccatpfx  14773  swrdccatfn  14796  swrdccat  14807  revccat  14838  2cshw  14887  cnpart  15330  resqreu  15342  recval  15413  abs1m  15426  abslem2  15430  fzomaxdiflem  15433  sqreulem  15450  sqreu  15451  limsupgre  15571  rlimdiv  15736  fsumparts  15896  climcnds  15943  expcnv  15956  ntrivcvg  15989  mod2eq1n2dvds  16440  ndvdssub  16502  sadcaddlem  16550  rplpwr  16651  dvdssqlem  16659  algcvgblem  16670  eucalgcvga  16679  isprm2lem  16774  powm2modprm  16898  coprimeprodsq  16903  pythagtriplem11  16920  pythagtriplem13  16922  pcadd2  16985  4sqlem11  17050  vdwlem6  17081  vdwlem8  17083  vdwlem10  17085  ramval  17103  ramcl2  17111  ramlb  17114  ram0  17117  mreintcl  17682  mrcval  17701  mrccl  17702  mrcuni  17712  mrcun  17713  acsfiel  17745  rescabs  17925  funcres  17988  setcmon  18179  setcepi  18180  fullestrcsetc  18242  funcsetcestrclem8  18253  fullsetcestrc  18257  yonffthlem  18373  pleval2i  18425  pospo  18434  poslubdg  18503  acsdrsel  18634  acsdrscl  18637  acsficl  18638  psss  18671  chnind  18712  chnub  18713  chnccats1  18716  chnccat  18717  grpidd  18768  ismndd  18862  gsumsgrpccat  18952  gsumwmhm  18957  mulgaddcom  19224  subgmulg  19267  resghm  19362  conjnsg  19384  ghmqusker  19417  f1otrspeq  19577  pmtrval  19581  pmtrrn  19587  pmtrfinv  19591  pmtrprfval  19617  psgnunilem1  19623  psgnunilem5  19624  psgnunilem4  19627  psgneldm2i  19635  lsmelvalix  19771  pj1ghm  19833  efgredlemc  19875  frgp0  19890  qusabl  19995  cycsubgcyg  20031  gsumval3  20037  gsumcllem  20038  ablfac1c  20203  pgpfac1lem5  20211  submomnd  20262  isrngd  20311  isringd  20436  01eq0ring  20694  isdrng4  20905  ornglmullt  21038  orngrmullt  21039  lspsneq0b  21200  lmodindp1  21201  lmhmf1o  21233  lmhmpreima  21235  reslmhm  21239  pwssplit3  21248  lspsncmp  21306  lspsneq  21312  prmidl2  21532  prmidl0  21544  qsidomlem1  21546  ssdifidlprm  21552  prmidlsubm  21553  znf1o  21767  dsmmlss  21960  frlmlbs  22013  frlmup1  22014  psrgrp  22174  mpfind  22334  psdmul  22397  ply1scleq  22533  mat1  22672  matunitlindflem2  22905  chfacfisf  23082  chfacfisfcpmat  23083  uniopn  23125  ntrval  23264  clsval  23265  neival  23330  neiptopreu  23361  lpval  23367  restdis  23406  lmbrf  23488  cnpnei  23492  1stcrest  23681  hauspwdom  23730  lfinpfin  23753  txcnpi  23837  ptrescn  23868  xkococnlem  23888  qtopeu  23945  kqreglem1  23970  ptuncnv  24036  filss  24082  fsubbas  24096  fbasrn  24113  cfinfil  24122  ufinffr  24158  elfm3  24179  rnelfmlem  24181  rnelfm  24182  flimclslem  24213  flfval  24219  isfcf  24263  cnextfvval  24294  cnextf  24295  cnextcn  24296  ustelimasn  24452  trust  24458  restutop  24466  ustuqtop2  24471  utop2nei  24479  ucncn  24513  trcfilu  24522  cnextucn  24531  met1stc  24750  metustexhalf  24785  cfilucfil  24788  psmetutop  24796  nmoix  24958  nmoeq0  24965  idnghm  24972  blcvx  25027  xrsxmet  25039  iccntr  25051  icccmp  25055  iihalf1  25162  iihalf2  25164  xrhmeo  25177  cnheibor  25186  ipcau2  25465  lmmbrf  25493  iscauf  25511  cmetcaulem  25519  bcthlem4  25558  cmetcusp  25585  rrxcph  25623  minveclem4  25663  evthicc2  25691  cniccbdd  25692  ovollb2  25720  ovolunlem1a  25727  ovolunlem1  25728  voliun  25785  icombl  25795  ioombl  25796  iccvolcl  25798  ioovolcl  25801  mbfss  25877  mbfposb  25884  itg2const2  25972  itg2splitlem  25979  itg2gt0  25991  iblss2  26036  itgioo  26046  dvaddf  26172  dvmulf  26173  dvcobr  26176  dvcof  26178  rolle  26220  dvlip  26223  c1lip1  26227  dvivthlem1  26238  lhop1lem  26243  dvfsumlem1  26256  ftc1lem4  26269  ftc1lem5  26270  ply1divmo  26364  coe1termlem  26487  plymulidp  26515  plydiveu  26531  taylplem1  26602  pserulm  26661  abelth  26680  abscxp2  26933  abscxpbnd  26993  logbgt0b  27033  ang180lem2  27050  ang180lem3  27051  isosctrlem1  27058  angpieqvd  27071  atandmtan  27160  birthdaylem3  27193  wilthlem2  27308  wilthimp  27311  isppw  27353  isppw2  27354  dvdsflsumcom  27427  chteq0  27448  perfectlem2  27469  dchrval  27473  dchrinvcl  27492  dchrptlem1  27503  bposlem3  27525  lgslem4  27539  lgsmod  27562  lgsdilem  27563  lgsdir2lem2  27565  lgsdir2  27569  lgsne0  27574  lgsmulsqcoprm  27582  lgseisenlem1  27614  2lgsoddprm  27655  2sqlem4  27660  chpo1ubb  27720  dchrisumn0  27760  pntrsumbnd2  27806  ostthlem1  27866  ostth3  27877  nosupbnd2lem1  27954  noinfbnd2lem1  27969  nocvxmin  28023  eqcuts2  28054  ltslpss  28176  madefi  28181  abslts  28517  eucliddivs  28644  peano5uzs  28672  z12bdaylem1  28738  elreno2  28763  idmot  28882  tgelrnln  28980  lnincplng  29144  plngmiropp  29154  lmimid  29181  lmiisolem  29183  hypcgrlem1  29187  brcgr  29360  colinearalglem4  29369  colinearalg  29370  axlowdimlem14  29415  axcontlem4  29427  cplgrop  29900  lfgriswlk  30153  pthdlem1  30234  spthcycl  30274  crctcshwlkn0  30292  elwspths2on  30433  elwspths2onw  30434  clwlkclwwlklem2fv2  30469  frgrncvvdeqlem9  30790  nvss  31077  sspn  31220  nmoub3i  31257  nmblolbii  31283  blocnilem  31288  minvecolem4  31364  htthlem  31401  norm1  31733  norm1exi  31734  pjeq  31883  axpjpj  31904  normcan  32060  pjoi0  32201  nmopub2tALT  32393  nmfnleub2  32410  eighmorth  32448  nmbdoplbi  32508  nmcoplbi  32512  nmophmi  32515  nmbdfnlbi  32533  nmcfnlbi  32536  riesz3i  32546  cnlnadjlem7  32557  branmfn  32589  nmopleid  32623  hstle  32714  superpos  32838  cvexchlem  32852  foresf1o  32982  elabreximd  32988  prssad  33007  prssbd  33008  unidifsnne  33014  tpssad  33017  fresunsn  33101  f1o3d  33102  fmptco1f1o  33109  fgreu  33147  suppovss  33156  elsuppfnd  33157  fsupprnfi  33167  resf1o  33204  fpwrelmap  33207  argcj  33222  xrofsup  33241  eliccelico  33251  elicoelioo  33252  iocinif  33255  difioo  33256  hashne0  33283  elq2  33285  oexpled  33309  indf1ofs  33315  eliccioo  33379  cshf1o  33405  mgcmnt1d  33440  mgcmnt2d  33441  pwrssmgc  33443  mndlactf1o  33473  mndractf1o  33474  gsummpt2co  33491  gsumhashmul  33510  gsummulsubdishift1  33511  symgcom  33526  symgcom2  33527  odpmco  33529  pmtrcnel  33532  pmtridf1o  33537  cycpmco2lem6  33574  cycpmco2lem7  33575  cycpmco2  33576  cyc3co2  33583  cycpmconjv  33585  tocyccntz  33587  cyc3evpm  33593  cycpmconjslem2  33598  cycpmconjs  33599  fxpsubm  33615  fxpsubg  33616  fxpsubrg  33617  fxpsdrg  33618  archirngz  33632  unitnz  33681  elrgspnlem1  33685  elrgspnlem2  33686  elrgspnlem4  33688  elrgspnsubrun  33692  rloccring  33714  rlocf1  33717  rlocisunit  33719  domnpropd  33723  rrgsubm  33727  sdrgdvcl  33743  sdrginvcl  33744  fracfld  33752  lindssn  33814  linds2eq  33817  dvdsrspss  33823  nsgqusf1olem1  33845  nsgqusf1olem3  33847  unitpidl1  33855  elrspunidl  33859  rhmimaidl  33863  drngidlhash  33864  mxidlirredi  33877  mxidlirred  33878  ssmxidl  33880  drng0mxidl  33881  opprmxidlabs  33892  qsdrngilem  33899  qsdrngi  33900  qsdrng  33902  drnglring  33905  dflring2  33906  dflringlem  33907  dflringlem3  33909  dflring4  33911  fldlring  33912  rsprprmprmidl  33935  rsprprmprmidlb  33936  rprmasso2  33939  rprmirredlem  33943  rprmirredb  33945  1arithidomlem2  33949  1arithufdlem4  33960  1arithufd  33961  ressply1evls1  33978  ply1asclunit  33987  ply1dg1rt  33993  ply1mulrtss  33995  ply1dg3rt0irred  33997  ply1degltlss  34009  ply1gsumz  34012  mplidomlem  34040  evlextv  34055  esplyfv1  34082  esplyind  34088  vietadeg1  34091  lsssra  34101  exsslsb  34110  lbslsat  34129  lindsunlem  34137  lindsun  34138  dimkerim  34140  fedgmullem1  34142  fedgmullem2  34143  fedgmul  34144  dimlssid  34145  lvecendof1f1o  34146  assalactf1o  34148  sdrgfldext  34163  fldsdrgfldext  34174  fldgenfldext  34181  evls1fldgencl  34183  fldextrspunlsp  34187  fldextrspunlem1  34188  fldextrspunfld  34189  irngss  34200  0ringirng  34202  irngnzply1  34204  extdgfialglem1  34205  irngnminplynz  34225  minplyelirng  34228  irredminply  34229  algextdeglem2  34231  algextdeglem4  34233  constrconj  34258  constrextdg2lem  34261  constrext2chnlem  34263  iconstr  34279  constrsdrg  34288  cos9thpiminplylem1  34295  cos9thpiminplylem2  34296  cos9thpiminplylem3  34297  cos9thpiminplylem5  34299  madjusmdetlem2  34341  qtophaus  34349  locfinreflem  34353  zarclssn  34386  zarmxt1  34393  zarcmplem  34394  rhmpreimacn  34398  unitdivcld  34414  tpr2rico  34425  ordtrestNEW  34434  lmxrge0  34465  elzrhunit  34490  qqhf  34499  gsumesum  34572  esumfsup  34583  esumcvg  34599  issgon  34636  sigainb  34650  insiga  34651  isrnmeas  34714  measvunilem  34726  volmeas  34745  ddeval1  34748  ddeval0  34749  imambfm  34776  omssubadd  34814  carsgclctunlem3  34834  eulerpartlemf  34884  eulerpartlemgvv  34890  probun  34933  dstfrvunirn  34989  signslema  35073  signstfvn  35080  signsvtn0  35081  signstfvneq0  35083  signstres  35086  signstfveq0a  35087  breprexplemc  35143  logdivsqrle  35161  hgt750lemg  35165  tgoldbachgtda  35172  tgoldbachgt  35174  lpadmax  35196  lpadleft  35197  lpadright  35198  bnj529  35254  bnj548  35409  bnj570  35417  bnj852  35433  bnj929  35448  bnj1097  35493  bnj1118  35496  bnj1145  35505  fissorduni  35597  vonf1oonfo  35715  acycgr0v  35730  derangen  35754  subfacp1lem2b  35763  subfacp1lem4  35765  subfacp1lem5  35766  derangfmla  35772  ptpconn  35815  mppspstlem  36153  wsuclem  36405  colinearex  36643  btwnconn1lem11  36680  btwnconn1lem12  36681  fwddifnp1  36748  nn0prpwlem  36944  ttctr  37115  dfttc2g  37128  regsfromregtco  37160  bj-snmoore  37866  bj-imdiridlem  37940  relowlpssretop  38121  fin2so  38364  ptrecube  38372  poimirlem8  38380  poimirlem13  38385  poimirlem15  38387  poimirlem24  38396  poimirlem25  38397  poimirlem26  38398  heicant  38407  mblfinlem2  38410  voliunnfl  38416  mbfresfi  38418  itg2addnclem  38423  itg2addnclem3  38425  itg2gt0cn  38427  ftc1cnnclem  38443  ftc1anclem5  38449  cover2  38468  indexdom  38487  sdclem1  38496  fdc  38498  equivbnd2  38545  heiborlem8  38571  heibor  38574  isdrngo2  38711  iscringd  38751  smprngopr  38805  prnc  38820  eqbrtr  38989  eqeltr  38991  islfld  39938  lkrshpor  39983  lfl1dim  39997  lfl1dim2N  39998  cmtcomlemN  40124  2lplnmN  40435  pmapjat1  40729  trlnid  41055  tendoex  41851  dia1dimid  41939  dibval2  42020  dihmeetlem2N  42175  dochlkr  42261  mapdcv  42536  hdmaplkr  42789  hdmapip0  42791  hlhillcs  42834  aks6d1c6lem4  43042  dvdsexpnn  43211  readvrec  43240  frlmvscadiccat  43397  psrmnd  43428  nacsfix  43560  3rexfrabdioph  43641  4rexfrabdioph  43642  6rexfrabdioph  43643  7rexfrabdioph  43644  eldioph4b  43655  pellexlem2  43674  pellexlem5  43677  jm2.26lem3  43845  numinfctb  43947  ordne0gt0  44105  omge1  44141  omlim2  44143  omord2lim  44144  omord2i  44145  tfsconcatfv  44185  tfsconcatb0  44188  oaun3lem1  44218  ntrclsfv1  44898  ntrneifv1  44922  ntrneifv2  44923  cvgdvgrat  45140  radcnvrat  45141  dvconstbi  45161  bccbc  45172  elpwgded  45390  elpwgdedVD  45742  sspwimpcf  45745  sspwimpcfVD  45746  sspwimpALT2  45753  ax6e2ndeqALT  45756  eliuniin  45934  eliuniin2  45955  qinioo  46368  dfxlim2v  46678  xlimliminflimsup  46693  cncfiooicclem1  46724  ibliooicc  46802  stoweidlem27  46858  stoweidlem28  46859  fourierdlem89  47026  fourierdlem91  47028  fourierdlem92  47029  smflimmpt  47641  tmachlem-agreesn  47778  odz2prm2pw  48469  perfectALTVlem2  48641  blen1b  49521  naryfvalelfv  49565  itscnhlc0yqe  49692  itsclquadb  49709  lubeldm2  49885  glbeldm2  49886  ipolub  49917  ipoglb  49920  fucofulem1  50239  functhinclem1  50373  thincciso  50382  prsthinc  50393  functermclem  50436  prstchom2ALT  50493  onetansqsecsq  50690  cotsqcscsq  50691  aacllem  50775