Theorem biimpar 482

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 411	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  bitr  816  exbiri  822  biadanid  834  bibiad  852  oplem1  1072  eqtr  2783  pm13.181  3040  opabss  5175  axprlem4OLD  5401  axprlem5OLD  5402  euotd  5496  brcogw  5854  somin1  6133  xpdifid  6165  xpdifcnvepel  6166  funfni  6641  fnssres  6658  fn0  6666  fnimadisj  6667  fnimaeq0  6668  foimacnv  6838  fvelimab  6953  dffv2  6976  fvopab3ig  6985  funcnvmpt  6991  dff3  7095  dffo4  7098  fpr2g  7209  ralima  7235  f1eqcocnv  7299  isomin  7335  f1ocnv2d  7663  fnexALT  7944  xp1st  8014  xp2nd  8015  frrlem3  8281  fpr2  8297  wfr3g  8312  wfr2  8320  iinon  8323  tfr3  8382  oawordri  8531  oaass  8542  omeulem1  8563  oeoa  8579  oeoe  8581  oeeulem  8583  elqsn0  8778  pwdom  9113  enfii  9166  phpeqd  9192  ominf  9220  findcard3  9239  marypha1lem  9389  wofib  9503  cantnff  9639  cantnfp1  9646  cantnf  9658  cnfcomlem  9664  ttrcltr  9681  frr3g  9724  r1sscl  9753  rankval3b  9794  infxpidm2  9997  numdom  10018  onssnum  10020  acni  10025  acni2  10026  dfac5  10108  djulepw  10172  infunsdom1  10191  infunsdom  10192  cofsmo  10248  cfsmolem  10249  fin1ai  10272  fin2i  10274  isf34lem1  10351  fin67  10374  itunisuc  10398  axdc3lem4  10432  zornn0g  10484  ttukeylem6  10493  brdom3  10507  tsken  10734  tskcard  10761  r1tskina  10762  intgru  10794  prlem934  11013  ltexprlem7  11022  supaddc  12177  mul2lt0rlt0  13115  xrmaxeq  13200  xrmineq  13201  xmulneg1  13290  ixxun  13383  difelfzle  13665  ssfzoulel  13785  elfznelfzo  13798  ico01fl0  13848  btwnzge0  13857  ltdifltdiv  13863  ioopnfsup  13893  icopnfsup  13894  modifeq2int  13965  suppssfz  14026  expmordi  14199  zzlesq  14238  faclbnd4lem4  14328  hasheni  14380  hashgt0  14420  hashge1  14421  hashprb  14429  hashpss  14442  lennncl  14567  wrdsymb0  14582  ccatsymb  14616  ccatlid  14620  ccatass  14622  ccatswrd  14702  swrdccat2  14703  ccatpfx  14734  swrdccatfn  14757  swrdccat  14768  revccat  14799  2cshw  14846  cnpart  15287  resqreu  15299  recval  15370  abs1m  15383  abslem2  15387  fzomaxdiflem  15390  sqreulem  15407  sqreu  15408  limsupgre  15528  rlimdiv  15693  fsumparts  15854  climcnds  15901  expcnv  15914  ntrivcvg  15947  mod2eq1n2dvds  16400  ndvdssub  16462  sadcaddlem  16510  rplpwr  16611  dvdssqlem  16619  algcvgblem  16630  eucalgcvga  16639  isprm2lem  16734  powm2modprm  16858  coprimeprodsq  16863  pythagtriplem11  16880  pythagtriplem13  16882  pcadd2  16945  4sqlem11  17010  vdwlem6  17041  vdwlem8  17043  vdwlem10  17045  ramval  17063  ramcl2  17071  ramlb  17074  ram0  17077  mreintcl  17642  mrcval  17661  mrccl  17662  mrcuni  17672  mrcun  17673  acsfiel  17705  rescabs  17885  funcres  17948  setcmon  18139  setcepi  18140  fullestrcsetc  18202  funcsetcestrclem8  18213  fullsetcestrc  18217  yonffthlem  18333  pleval2i  18385  pospo  18394  poslubdg  18463  acsdrsel  18594  acsdrscl  18597  acsficl  18598  psss  18631  chnind  18672  chnub  18673  chnccats1  18676  chnccat  18677  grpidd  18724  ismndd  18809  gsumsgrpccat  18894  gsumwmhm  18899  mulgaddcom  19159  subgmulg  19202  resghm  19297  conjnsg  19319  ghmqusker  19352  f1otrspeq  19512  pmtrval  19516  pmtrrn  19522  pmtrfinv  19526  pmtrprfval  19552  psgnunilem1  19558  psgnunilem5  19559  psgnunilem4  19562  psgneldm2i  19570  lsmelvalix  19706  pj1ghm  19768  efgredlemc  19810  frgp0  19825  qusabl  19930  cycsubgcyg  19966  gsumval3  19972  gsumcllem  19973  ablfac1c  20138  pgpfac1lem5  20146  submomnd  20197  isrngd  20246  isringd  20370  01eq0ring  20628  isdrng4  20839  ornglmullt  20972  orngrmullt  20973  lspsneq0b  21134  lmodindp1  21135  lmhmf1o  21167  lmhmpreima  21169  reslmhm  21173  pwssplit3  21182  lspsncmp  21240  lspsneq  21246  prmidl2  21466  prmidl0  21478  qsidomlem1  21480  ssdifidlprm  21486  prmidlsubm  21487  znf1o  21701  dsmmlss  21894  frlmlbs  21947  frlmup1  21948  psrgrp  22106  mpfind  22266  psdmul  22329  ply1scleq  22465  mat1  22604  chfacfisf  23011  chfacfisfcpmat  23012  uniopn  23054  ntrval  23193  clsval  23194  neival  23259  neiptopreu  23290  lpval  23296  restdis  23335  lmbrf  23417  cnpnei  23421  1stcrest  23610  hauspwdom  23658  lfinpfin  23681  txcnpi  23765  ptrescn  23796  xkococnlem  23816  qtopeu  23873  kqreglem1  23898  ptuncnv  23964  filss  24010  fsubbas  24024  fbasrn  24041  cfinfil  24050  ufinffr  24086  elfm3  24107  rnelfmlem  24109  rnelfm  24110  flimclslem  24141  flfval  24147  isfcf  24191  cnextfvval  24222  cnextf  24223  cnextcn  24224  ustelimasn  24380  trust  24386  restutop  24394  ustuqtop2  24399  utop2nei  24407  ucncn  24441  trcfilu  24450  cnextucn  24459  met1stc  24678  metustexhalf  24713  cfilucfil  24716  psmetutop  24724  nmoix  24886  nmoeq0  24893  idnghm  24900  blcvx  24955  xrsxmet  24967  iccntr  24979  icccmp  24983  iihalf1  25090  iihalf2  25092  xrhmeo  25105  cnheibor  25114  ipcau2  25393  lmmbrf  25421  iscauf  25439  cmetcaulem  25447  bcthlem4  25486  cmetcusp  25513  rrxcph  25551  minveclem4  25591  evthicc2  25619  cniccbdd  25620  ovollb2  25648  ovolunlem1a  25655  ovolunlem1  25656  voliun  25713  icombl  25723  ioombl  25724  iccvolcl  25726  ioovolcl  25729  mbfss  25805  mbfposb  25812  itg2const2  25900  itg2splitlem  25907  itg2gt0  25919  iblss2  25965  itgioo  25975  dvaddf  26101  dvmulf  26102  dvcobr  26105  dvcof  26107  rolle  26149  dvlip  26152  c1lip1  26156  dvivthlem1  26167  lhop1lem  26172  dvfsumlem1  26185  ftc1lem4  26198  ftc1lem5  26199  ply1divmo  26293  coe1termlem  26415  plymulidp  26443  plydiveu  26459  taylplem1  26526  pserulm  26585  abelth  26604  abscxp2  26858  abscxpbnd  26918  logbgt0b  26958  ang180lem2  26975  ang180lem3  26976  isosctrlem1  26983  angpieqvd  26996  atandmtan  27085  birthdaylem3  27118  wilthlem2  27233  wilthimp  27236  isppw  27278  isppw2  27279  dvdsflsumcom  27352  chteq0  27373  perfectlem2  27394  dchrval  27398  dchrinvcl  27417  dchrptlem1  27428  bposlem3  27450  lgslem4  27464  lgsmod  27487  lgsdilem  27488  lgsdir2lem2  27490  lgsdir2  27494  lgsne0  27499  lgsmulsqcoprm  27507  lgseisenlem1  27539  2lgsoddprm  27580  2sqlem4  27585  chpo1ubb  27645  dchrisumn0  27685  pntrsumbnd2  27731  ostthlem1  27791  ostth3  27802  nosupbnd2lem1  27879  noinfbnd2lem1  27894  nocvxmin  27948  eqcuts2  27979  ltslpss  28101  madefi  28106  abslts  28442  eucliddivs  28569  peano5uzs  28597  z12bdaylem1  28663  elreno2  28688  idmot  28806  tgelrnln  28903  lnincplng  29066  plngmiropp  29076  lmimid  29103  lmiisolem  29105  hypcgrlem1  29109  brcgr  29250  colinearalglem4  29259  colinearalg  29260  axlowdimlem14  29305  axcontlem4  29317  cplgrop  29787  lfgriswlk  30036  pthdlem1  30115  crctcshwlkn0  30170  elwspths2on  30311  elwspths2onw  30312  clwlkclwwlklem2fv2  30347  frgrncvvdeqlem9  30658  nvss  30945  sspn  31088  nmoub3i  31125  nmblolbii  31151  blocnilem  31156  minvecolem4  31232  htthlem  31269  norm1  31601  norm1exi  31602  pjeq  31751  axpjpj  31772  normcan  31928  pjoi0  32069  nmopub2tALT  32261  nmfnleub2  32278  eighmorth  32316  nmbdoplbi  32376  nmcoplbi  32380  nmophmi  32383  nmbdfnlbi  32401  nmcfnlbi  32404  riesz3i  32414  cnlnadjlem7  32425  branmfn  32457  nmopleid  32491  hstle  32582  superpos  32706  cvexchlem  32720  foresf1o  32850  elabreximd  32856  prssad  32875  prssbd  32876  unidifsnne  32882  tpssad  32885  fresunsn  32970  f1o3d  32971  fmptco1f1o  32978  fgreu  33016  suppovss  33026  elsuppfnd  33027  fsupprnfi  33037  resf1o  33075  fpwrelmap  33078  argcj  33093  xrofsup  33112  eliccelico  33122  elicoelioo  33123  iocinif  33126  difioo  33127  hashne0  33154  elq2  33156  oexpled  33180  indf1ofs  33186  eliccioo  33250  cshf1o  33282  mgcmnt1d  33317  mgcmnt2d  33318  pwrssmgc  33320  mndlactf1o  33350  mndractf1o  33351  gsummpt2co  33368  gsumhashmul  33387  gsummulsubdishift1  33388  symgcom  33403  symgcom2  33404  odpmco  33406  pmtrcnel  33409  pmtridf1o  33414  cycpmco2lem6  33451  cycpmco2lem7  33452  cycpmco2  33453  cyc3co2  33460  cycpmconjv  33462  tocyccntz  33464  cyc3evpm  33470  cycpmconjslem2  33475  cycpmconjs  33476  fxpsubm  33492  fxpsubg  33493  fxpsubrg  33494  fxpsdrg  33495  archirngz  33509  unitnz  33558  elrgspnlem1  33562  elrgspnlem2  33563  elrgspnlem4  33565  elrgspnsubrun  33569  rloccring  33591  rlocf1  33594  rlocisunit  33596  domnpropd  33600  rrgsubm  33604  sdrgdvcl  33620  sdrginvcl  33621  fracfld  33629  lindssn  33691  linds2eq  33694  dvdsrspss  33700  nsgqusf1olem1  33722  nsgqusf1olem3  33724  unitpidl1  33732  elrspunidl  33736  rhmimaidl  33740  drngidlhash  33741  mxidlirredi  33754  mxidlirred  33755  ssmxidl  33757  drng0mxidl  33758  opprmxidlabs  33769  qsdrngilem  33776  qsdrngi  33777  qsdrng  33779  drnglring  33782  dflring2  33783  dflringlem  33784  dflringlem3  33786  dflring4  33788  fldlring  33789  rsprprmprmidl  33812  rsprprmprmidlb  33813  rprmasso2  33816  rprmirredlem  33820  rprmirredb  33822  1arithidomlem2  33826  1arithufdlem4  33837  1arithufd  33838  ressply1evls1  33855  ply1asclunit  33864  ply1dg1rt  33870  ply1mulrtss  33872  ply1dg3rt0irred  33874  ply1degltlss  33886  ply1gsumz  33889  mplidomlem  33917  evlextv  33932  esplyfv1  33959  esplyind  33965  vietadeg1  33968  lsssra  33978  exsslsb  33987  lbslsat  34006  lindsunlem  34014  lindsun  34015  dimkerim  34017  fedgmullem1  34019  fedgmullem2  34020  fedgmul  34021  dimlssid  34022  lvecendof1f1o  34023  assalactf1o  34025  sdrgfldext  34040  fldsdrgfldext  34051  fldgenfldext  34058  evls1fldgencl  34060  fldextrspunlsp  34064  fldextrspunlem1  34065  fldextrspunfld  34066  irngss  34077  0ringirng  34079  irngnzply1  34081  extdgfialglem1  34082  irngnminplynz  34102  minplyelirng  34105  irredminply  34106  algextdeglem2  34108  algextdeglem4  34110  constrconj  34135  constrextdg2lem  34138  constrext2chnlem  34140  iconstr  34156  constrsdrg  34165  cos9thpiminplylem1  34172  cos9thpiminplylem2  34173  cos9thpiminplylem3  34174  cos9thpiminplylem5  34176  madjusmdetlem2  34218  qtophaus  34226  locfinreflem  34230  zarclssn  34263  zarmxt1  34270  zarcmplem  34271  rhmpreimacn  34275  unitdivcld  34291  tpr2rico  34302  ordtrestNEW  34311  lmxrge0  34342  elzrhunit  34367  qqhf  34376  gsumesum  34449  esumfsup  34460  esumcvg  34476  issgon  34513  sigainb  34526  insiga  34527  isrnmeas  34590  measvunilem  34602  volmeas  34621  ddeval1  34624  ddeval0  34625  imambfm  34652  omssubadd  34690  carsgclctunlem3  34710  eulerpartlemf  34760  eulerpartlemgvv  34766  probun  34809  dstfrvunirn  34865  signslema  34949  signstfvn  34956  signsvtn0  34957  signstfvneq0  34959  signstres  34962  signstfveq0a  34963  breprexplemc  35019  logdivsqrle  35037  hgt750lemg  35041  tgoldbachgtda  35048  tgoldbachgt  35050  lpadmax  35072  lpadleft  35073  lpadright  35074  bnj529  35130  bnj548  35285  bnj570  35293  bnj852  35309  bnj929  35324  bnj1097  35369  bnj1118  35372  bnj1145  35381  funen1cnv  35477  fissorduni  35480  vonf1oonfo  35599  spthcycl  35621  acycgr0v  35640  derangen  35664  subfacp1lem2b  35673  subfacp1lem4  35675  subfacp1lem5  35676  derangfmla  35682  ptpconn  35725  mppspstlem  36063  wsuclem  36315  colinearex  36552  btwnconn1lem11  36589  btwnconn1lem12  36590  fwddifnp1  36657  nn0prpwlem  36853  ttctr  37024  dfttc2g  37037  regsfromregtco  37069  bj-snmoore  37775  bj-imdiridlem  37849  relowlpssretop  38030  fin2so  38278  matunitlindflem2  38288  ptrecube  38291  poimirlem8  38299  poimirlem13  38304  poimirlem15  38306  poimirlem24  38315  poimirlem25  38316  poimirlem26  38317  heicant  38326  mblfinlem2  38329  voliunnfl  38335  mbfresfi  38337  itg2addnclem  38342  itg2addnclem3  38344  itg2gt0cn  38346  ftc1cnnclem  38362  ftc1anclem5  38368  cover2  38386  indexdom  38405  sdclem1  38414  fdc  38416  equivbnd2  38463  heiborlem8  38489  heibor  38492  isdrngo2  38629  iscringd  38669  smprngopr  38723  prnc  38738  eqbrtr  38907  eqeltr  38909  islfld  39856  lkrshpor  39901  lfl1dim  39915  lfl1dim2N  39916  cmtcomlemN  40042  2lplnmN  40353  pmapjat1  40647  trlnid  40973  tendoex  41769  dia1dimid  41857  dibval2  41938  dihmeetlem2N  42093  dochlkr  42179  mapdcv  42454  hdmaplkr  42707  hdmapip0  42709  hlhillcs  42752  aks6d1c6lem4  42960  dvdsexpnn  43114  readvrec  43143  frlmvscadiccat  43300  psrmnd  43331  nacsfix  43463  3rexfrabdioph  43544  4rexfrabdioph  43545  6rexfrabdioph  43546  7rexfrabdioph  43547  eldioph4b  43558  pellexlem2  43577  pellexlem5  43580  jm2.26lem3  43748  numinfctb  43850  ordne0gt0  44008  omge1  44044  omlim2  44046  omord2lim  44047  omord2i  44048  tfsconcatfv  44088  tfsconcatb0  44091  oaun3lem1  44121  ntrclsfv1  44801  ntrneifv1  44825  ntrneifv2  44826  cvgdvgrat  45043  radcnvrat  45044  dvconstbi  45064  bccbc  45075  elpwgded  45293  elpwgdedVD  45645  sspwimpcf  45648  sspwimpcfVD  45649  sspwimpALT2  45656  ax6e2ndeqALT  45659  eliuniin  45837  eliuniin2  45858  qinioo  46271  dfxlim2v  46581  xlimliminflimsup  46596  cncfiooicclem1  46627  ibliooicc  46705  stoweidlem27  46761  stoweidlem28  46762  fourierdlem89  46929  fourierdlem91  46931  fourierdlem92  46932  smflimmpt  47544  odz2prm2pw  48335  perfectALTVlem2  48507  blen1b  49388  naryfvalelfv  49432  itscnhlc0yqe  49559  itsclquadb  49576  lubeldm2  49754  glbeldm2  49755  ipolub  49786  ipoglb  49789  fucofulem1  50108  functhinclem1  50242  thincciso  50251  prsthinc  50262  functermclem  50305  prstchom2ALT  50362  onetansqsecsq  50559  cotsqcscsq  50560  aacllem  50641