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  2782  pm13.181  3039  opabss  5173  axprlem4OLD  5399  axprlem5OLD  5400  euotd  5494  brcogw  5852  somin1  6131  xpdifid  6164  xpdifcnvepel  6165  funfni  6642  fnssres  6659  fn0  6667  fnimadisj  6668  fnimaeq0  6669  foimacnv  6839  fvelimab  6954  dffv2  6977  fvopab3ig  6986  funcnvmpt  6992  dff3  7097  dffo4  7100  fpr2g  7214  ralima  7240  f1eqcocnv  7306  isomin  7342  f1ocnv2d  7671  fnexALT  7952  xp1st  8022  xp2nd  8023  frrlem3  8291  fpr2  8307  wfr3g  8322  wfr2  8330  iinon  8333  tfr3  8392  oawordri  8541  oaass  8552  omeulem1  8573  oeoa  8589  oeoe  8591  oeeulem  8593  elqsn0  8788  funen1cnv  9039  pwdom  9131  enfii  9184  phpeqd  9210  ominf  9238  findcard3  9257  marypha1lem  9407  wofib  9521  cantnff  9657  cantnfp1  9664  cantnf  9676  cnfcomlem  9682  ttrcltr  9699  frr3g  9742  r1sscl  9771  rankval3b  9812  infxpidm2  10024  numdom  10045  onssnum  10047  acni  10052  acni2  10053  dfac5  10135  djulepw  10199  infunsdom1  10218  infunsdom  10219  cofsmo  10275  cfsmolem  10276  fin1ai  10299  fin2i  10301  isf34lem1  10378  fin67  10401  itunisuc  10425  axdc3lem4  10459  zornn0g  10511  ttukeylem6  10520  brdom3  10535  tsken  10767  tskcard  10794  r1tskina  10795  intgru  10827  prlem934  11046  ltexprlem7  11055  supaddc  12210  mul2lt0rlt0  13150  xrmaxeq  13235  xrmineq  13236  xmulneg1  13325  ixxun  13418  difelfzle  13700  ssfzoulel  13820  elfznelfzo  13833  ico01fl0  13884  btwnzge0  13893  ltdifltdiv  13899  ioopnfsup  13929  icopnfsup  13930  modifeq2int  14001  suppssfz  14062  expmordi  14235  zzlesq  14274  faclbnd4lem4  14364  hasheni  14416  hashgt0  14456  hashge1  14457  hashprb  14465  hashpss  14478  lennncl  14603  wrdsymb0  14618  ccatsymb  14652  ccatlid  14656  ccatass  14658  ccatswrd  14742  swrdccat2  14743  ccatpfx  14774  swrdccatfn  14797  swrdccat  14808  revccat  14839  2cshw  14888  cnpart  15331  resqreu  15343  recval  15414  abs1m  15427  abslem2  15431  fzomaxdiflem  15434  sqreulem  15451  sqreu  15452  limsupgre  15572  rlimdiv  15737  fsumparts  15897  climcnds  15944  expcnv  15957  ntrivcvg  15990  mod2eq1n2dvds  16443  ndvdssub  16505  sadcaddlem  16553  rplpwr  16654  dvdssqlem  16662  algcvgblem  16673  eucalgcvga  16682  isprm2lem  16777  powm2modprm  16901  coprimeprodsq  16906  pythagtriplem11  16923  pythagtriplem13  16925  pcadd2  16988  4sqlem11  17053  vdwlem6  17084  vdwlem8  17086  vdwlem10  17088  ramval  17106  ramcl2  17114  ramlb  17117  ram0  17120  mreintcl  17685  mrcval  17704  mrccl  17705  mrcuni  17715  mrcun  17716  acsfiel  17748  rescabs  17928  funcres  17991  setcmon  18182  setcepi  18183  fullestrcsetc  18245  funcsetcestrclem8  18256  fullsetcestrc  18260  yonffthlem  18376  pleval2i  18428  pospo  18437  poslubdg  18506  acsdrsel  18637  acsdrscl  18640  acsficl  18641  psss  18674  chnind  18715  chnub  18716  chnccats1  18719  chnccat  18720  grpidd  18771  ismndd  18865  gsumsgrpccat  18955  gsumwmhm  18960  mulgaddcom  19227  subgmulg  19270  resghm  19365  conjnsg  19387  ghmqusker  19420  f1otrspeq  19580  pmtrval  19584  pmtrrn  19590  pmtrfinv  19594  pmtrprfval  19620  psgnunilem1  19626  psgnunilem5  19627  psgnunilem4  19630  psgneldm2i  19638  lsmelvalix  19774  pj1ghm  19836  efgredlemc  19878  frgp0  19893  qusabl  19998  cycsubgcyg  20034  gsumval3  20040  gsumcllem  20041  ablfac1c  20206  pgpfac1lem5  20214  submomnd  20265  isrngd  20314  isringd  20439  01eq0ring  20697  isdrng4  20908  ornglmullt  21041  orngrmullt  21042  lspsneq0b  21203  lmodindp1  21204  lmhmf1o  21236  lmhmpreima  21238  reslmhm  21242  pwssplit3  21251  lspsncmp  21309  lspsneq  21315  prmidl2  21535  prmidl0  21547  qsidomlem1  21549  ssdifidlprm  21555  prmidlsubm  21556  znf1o  21770  dsmmlss  21963  frlmlbs  22016  frlmup1  22017  psrgrp  22177  mpfind  22337  psdmul  22400  ply1scleq  22536  mat1  22675  matunitlindflem2  22908  chfacfisf  23085  chfacfisfcpmat  23086  uniopn  23128  ntrval  23267  clsval  23268  neival  23333  neiptopreu  23364  lpval  23370  restdis  23409  lmbrf  23491  cnpnei  23495  1stcrest  23684  hauspwdom  23733  lfinpfin  23756  txcnpi  23840  ptrescn  23871  xkococnlem  23891  qtopeu  23948  kqreglem1  23973  ptuncnv  24039  filss  24085  fsubbas  24099  fbasrn  24116  cfinfil  24125  ufinffr  24161  elfm3  24182  rnelfmlem  24184  rnelfm  24185  flimclslem  24216  flfval  24222  isfcf  24266  cnextfvval  24297  cnextf  24298  cnextcn  24299  ustelimasn  24455  trust  24461  restutop  24469  ustuqtop2  24474  utop2nei  24482  ucncn  24516  trcfilu  24525  cnextucn  24534  met1stc  24753  metustexhalf  24788  cfilucfil  24791  psmetutop  24799  nmoix  24961  nmoeq0  24968  idnghm  24975  blcvx  25030  xrsxmet  25042  iccntr  25054  icccmp  25058  iihalf1  25165  iihalf2  25167  xrhmeo  25180  cnheibor  25189  ipcau2  25468  lmmbrf  25496  iscauf  25514  cmetcaulem  25522  bcthlem4  25561  cmetcusp  25588  rrxcph  25626  minveclem4  25666  evthicc2  25694  cniccbdd  25695  ovollb2  25723  ovolunlem1a  25730  ovolunlem1  25731  voliun  25788  icombl  25798  ioombl  25799  iccvolcl  25801  ioovolcl  25804  mbfss  25880  mbfposb  25887  itg2const2  25975  itg2splitlem  25982  itg2gt0  25994  iblss2  26040  itgioo  26050  dvaddf  26176  dvmulf  26177  dvcobr  26180  dvcof  26182  rolle  26224  dvlip  26227  c1lip1  26231  dvivthlem1  26242  lhop1lem  26247  dvfsumlem1  26260  ftc1lem4  26273  ftc1lem5  26274  ply1divmo  26368  coe1termlem  26491  plymulidp  26519  plydiveu  26535  taylplem1  26606  pserulm  26665  abelth  26684  abscxp2  26938  abscxpbnd  26998  logbgt0b  27038  ang180lem2  27055  ang180lem3  27056  isosctrlem1  27063  angpieqvd  27076  atandmtan  27165  birthdaylem3  27198  wilthlem2  27313  wilthimp  27316  isppw  27358  isppw2  27359  dvdsflsumcom  27432  chteq0  27453  perfectlem2  27474  dchrval  27478  dchrinvcl  27497  dchrptlem1  27508  bposlem3  27530  lgslem4  27544  lgsmod  27567  lgsdilem  27568  lgsdir2lem2  27570  lgsdir2  27574  lgsne0  27579  lgsmulsqcoprm  27587  lgseisenlem1  27619  2lgsoddprm  27660  2sqlem4  27665  chpo1ubb  27725  dchrisumn0  27765  pntrsumbnd2  27811  ostthlem1  27871  ostth3  27882  nosupbnd2lem1  27959  noinfbnd2lem1  27974  nocvxmin  28028  eqcuts2  28059  ltslpss  28181  madefi  28186  abslts  28522  eucliddivs  28649  peano5uzs  28677  z12bdaylem1  28743  elreno2  28768  idmot  28887  tgelrnln  28985  lnincplng  29149  plngmiropp  29159  lmimid  29186  lmiisolem  29188  hypcgrlem1  29192  brcgr  29365  colinearalglem4  29374  colinearalg  29375  axlowdimlem14  29420  axcontlem4  29432  cplgrop  29905  lfgriswlk  30158  pthdlem1  30239  spthcycl  30279  crctcshwlkn0  30297  elwspths2on  30438  elwspths2onw  30439  clwlkclwwlklem2fv2  30474  frgrncvvdeqlem9  30795  nvss  31082  sspn  31225  nmoub3i  31262  nmblolbii  31288  blocnilem  31293  minvecolem4  31369  htthlem  31406  norm1  31738  norm1exi  31739  pjeq  31888  axpjpj  31909  normcan  32065  pjoi0  32206  nmopub2tALT  32398  nmfnleub2  32415  eighmorth  32453  nmbdoplbi  32513  nmcoplbi  32517  nmophmi  32520  nmbdfnlbi  32538  nmcfnlbi  32541  riesz3i  32551  cnlnadjlem7  32562  branmfn  32594  nmopleid  32628  hstle  32719  superpos  32843  cvexchlem  32857  foresf1o  32987  elabreximd  32993  prssad  33012  prssbd  33013  unidifsnne  33019  tpssad  33022  fresunsn  33106  f1o3d  33107  fmptco1f1o  33114  fgreu  33152  suppovss  33161  elsuppfnd  33162  fsupprnfi  33172  resf1o  33209  fpwrelmap  33212  argcj  33227  xrofsup  33246  eliccelico  33256  elicoelioo  33257  iocinif  33260  difioo  33261  hashne0  33288  elq2  33290  oexpled  33314  indf1ofs  33320  eliccioo  33384  cshf1o  33410  mgcmnt1d  33445  mgcmnt2d  33446  pwrssmgc  33448  mndlactf1o  33478  mndractf1o  33479  gsummpt2co  33496  gsumhashmul  33515  gsummulsubdishift1  33516  symgcom  33531  symgcom2  33532  odpmco  33534  pmtrcnel  33537  pmtridf1o  33542  cycpmco2lem6  33579  cycpmco2lem7  33580  cycpmco2  33581  cyc3co2  33588  cycpmconjv  33590  tocyccntz  33592  cyc3evpm  33598  cycpmconjslem2  33603  cycpmconjs  33604  fxpsubm  33620  fxpsubg  33621  fxpsubrg  33622  fxpsdrg  33623  archirngz  33637  unitnz  33686  elrgspnlem1  33690  elrgspnlem2  33691  elrgspnlem4  33693  elrgspnsubrun  33697  rloccring  33719  rlocf1  33722  rlocisunit  33724  domnpropd  33728  rrgsubm  33732  sdrgdvcl  33748  sdrginvcl  33749  fracfld  33757  lindssn  33819  linds2eq  33822  dvdsrspss  33828  nsgqusf1olem1  33850  nsgqusf1olem3  33852  unitpidl1  33860  elrspunidl  33864  rhmimaidl  33868  drngidlhash  33869  mxidlirredi  33882  mxidlirred  33883  ssmxidl  33885  drng0mxidl  33886  opprmxidlabs  33897  qsdrngilem  33904  qsdrngi  33905  qsdrng  33907  drnglring  33910  dflring2  33911  dflringlem  33912  dflringlem3  33914  dflring4  33916  fldlring  33917  rsprprmprmidl  33940  rsprprmprmidlb  33941  rprmasso2  33944  rprmirredlem  33948  rprmirredb  33950  1arithidomlem2  33954  1arithufdlem4  33965  1arithufd  33966  ressply1evls1  33983  ply1asclunit  33992  ply1dg1rt  33998  ply1mulrtss  34000  ply1dg3rt0irred  34002  ply1degltlss  34014  ply1gsumz  34017  mplidomlem  34045  evlextv  34060  esplyfv1  34087  esplyind  34093  vietadeg1  34096  lsssra  34106  exsslsb  34115  lbslsat  34134  lindsunlem  34142  lindsun  34143  dimkerim  34145  fedgmullem1  34147  fedgmullem2  34148  fedgmul  34149  dimlssid  34150  lvecendof1f1o  34151  assalactf1o  34153  sdrgfldext  34168  fldsdrgfldext  34179  fldgenfldext  34186  evls1fldgencl  34188  fldextrspunlsp  34192  fldextrspunlem1  34193  fldextrspunfld  34194  irngss  34205  0ringirng  34207  irngnzply1  34209  extdgfialglem1  34210  irngnminplynz  34230  minplyelirng  34233  irredminply  34234  algextdeglem2  34236  algextdeglem4  34238  constrconj  34263  constrextdg2lem  34266  constrext2chnlem  34268  iconstr  34284  constrsdrg  34293  cos9thpiminplylem1  34300  cos9thpiminplylem2  34301  cos9thpiminplylem3  34302  cos9thpiminplylem5  34304  madjusmdetlem2  34346  qtophaus  34354  locfinreflem  34358  zarclssn  34391  zarmxt1  34398  zarcmplem  34399  rhmpreimacn  34403  unitdivcld  34419  tpr2rico  34430  ordtrestNEW  34439  lmxrge0  34470  elzrhunit  34495  qqhf  34504  gsumesum  34577  esumfsup  34588  esumcvg  34604  issgon  34641  sigainb  34655  insiga  34656  isrnmeas  34719  measvunilem  34731  volmeas  34750  ddeval1  34753  ddeval0  34754  imambfm  34781  omssubadd  34819  carsgclctunlem3  34839  eulerpartlemf  34889  eulerpartlemgvv  34895  probun  34938  dstfrvunirn  34994  signslema  35078  signstfvn  35085  signsvtn0  35086  signstfvneq0  35088  signstres  35091  signstfveq0a  35092  breprexplemc  35148  logdivsqrle  35166  hgt750lemg  35170  tgoldbachgtda  35177  tgoldbachgt  35179  lpadmax  35201  lpadleft  35202  lpadright  35203  bnj529  35259  bnj548  35414  bnj570  35422  bnj852  35438  bnj929  35453  bnj1097  35498  bnj1118  35501  bnj1145  35510  fissorduni  35602  vonf1oonfo  35720  acycgr0v  35735  derangen  35759  subfacp1lem2b  35768  subfacp1lem4  35770  subfacp1lem5  35771  derangfmla  35777  ptpconn  35820  mppspstlem  36158  wsuclem  36410  colinearex  36648  btwnconn1lem11  36685  btwnconn1lem12  36686  fwddifnp1  36753  nn0prpwlem  36949  ttctr  37120  dfttc2g  37133  regsfromregtco  37165  bj-snmoore  37871  bj-imdiridlem  37945  relowlpssretop  38126  fin2so  38369  ptrecube  38377  poimirlem8  38385  poimirlem13  38390  poimirlem15  38392  poimirlem24  38401  poimirlem25  38402  poimirlem26  38403  heicant  38412  mblfinlem2  38415  voliunnfl  38421  mbfresfi  38423  itg2addnclem  38428  itg2addnclem3  38430  itg2gt0cn  38432  ftc1cnnclem  38448  ftc1anclem5  38454  cover2  38473  indexdom  38492  sdclem1  38501  fdc  38503  equivbnd2  38550  heiborlem8  38576  heibor  38579  isdrngo2  38716  iscringd  38756  smprngopr  38810  prnc  38825  eqbrtr  38994  eqeltr  38996  islfld  39943  lkrshpor  39988  lfl1dim  40002  lfl1dim2N  40003  cmtcomlemN  40129  2lplnmN  40440  pmapjat1  40734  trlnid  41060  tendoex  41856  dia1dimid  41944  dibval2  42025  dihmeetlem2N  42180  dochlkr  42266  mapdcv  42541  hdmaplkr  42794  hdmapip0  42796  hlhillcs  42839  aks6d1c6lem4  43047  dvdsexpnn  43216  readvrec  43245  frlmvscadiccat  43402  psrmnd  43433  nacsfix  43565  3rexfrabdioph  43646  4rexfrabdioph  43647  6rexfrabdioph  43648  7rexfrabdioph  43649  eldioph4b  43660  pellexlem2  43679  pellexlem5  43682  jm2.26lem3  43850  numinfctb  43952  ordne0gt0  44110  omge1  44146  omlim2  44148  omord2lim  44149  omord2i  44150  tfsconcatfv  44190  tfsconcatb0  44193  oaun3lem1  44223  ntrclsfv1  44903  ntrneifv1  44927  ntrneifv2  44928  cvgdvgrat  45145  radcnvrat  45146  dvconstbi  45166  bccbc  45177  elpwgded  45395  elpwgdedVD  45747  sspwimpcf  45750  sspwimpcfVD  45751  sspwimpALT2  45758  ax6e2ndeqALT  45761  eliuniin  45939  eliuniin2  45960  qinioo  46373  dfxlim2v  46683  xlimliminflimsup  46698  cncfiooicclem1  46729  ibliooicc  46807  stoweidlem27  46863  stoweidlem28  46864  fourierdlem89  47031  fourierdlem91  47033  fourierdlem92  47034  smflimmpt  47646  tmachlem-agreesn  47783  odz2prm2pw  48474  perfectALTVlem2  48646  blen1b  49526  naryfvalelfv  49570  itscnhlc0yqe  49697  itsclquadb  49714  lubeldm2  49890  glbeldm2  49891  ipolub  49922  ipoglb  49925  fucofulem1  50244  functhinclem1  50378  thincciso  50387  prsthinc  50398  functermclem  50441  prstchom2ALT  50498  onetansqsecsq  50695  cotsqcscsq  50696  aacllem  50780