Theorem biimpar 481

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

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

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 400

This theorem is referenced by:  bitr  805  exbiri  811  biadanid  823  oplem1  1057  eqtr  2760  opabss  5117  axprlem4  5319  axprlem5  5320  euotd  5396  brcogw  5737  somin1  5998  xpdifid  6031  funfni  6484  fncoOLD  6495  fnssres  6500  fn0  6509  fnimadisj  6510  fnimaeq0  6511  foimacnv  6678  fvelimab  6784  dffv2  6806  fvopab3ig  6814  dff3  6919  dffo4  6922  fpr2g  7027  f1eqcocnv  7111  f1eqcocnvOLD  7112  isomin  7146  f1ocnv2d  7458  fnexALT  7724  xp1st  7793  xp2nd  7794  frrlem3  8029  fpr2  8044  wfr3g  8053  wfrlem3  8056  wfrlem4  8058  iinon  8077  tfr3  8135  oawordri  8278  oaass  8289  omeulem1  8310  oeoa  8325  oeoe  8327  oeeulem  8329  ecelqsg  8454  elqsn0  8468  pwdom  8798  enfii  8864  marypha1lem  9049  wofib  9161  cantnff  9289  cantnfp1  9296  cantnf  9308  cnfcomlem  9314  frr3g  9372  r1sscl  9401  rankval3b  9442  infxpidm2  9631  numdom  9652  onssnum  9654  acni  9659  acni2  9660  dfac5  9742  djulepw  9806  infunsdom1  9827  infunsdom  9828  cofsmo  9883  cfsmolem  9884  fin1ai  9907  fin2i  9909  isf34lem1  9986  fin67  10009  itunisuc  10033  axdc3lem4  10067  zornn0g  10119  ttukeylem6  10128  brdom3  10142  tsken  10368  tskcard  10395  r1tskina  10396  intgru  10428  prlem934  10647  ltexprlem7  10656  supaddc  11799  mul2lt0rlt0  12688  xrmaxeq  12769  xrmineq  12770  xmulneg1  12859  ixxun  12951  difelfzle  13225  ssfzoulel  13336  elfznelfzo  13347  ico01fl0  13394  btwnzge0  13403  ltdifltdiv  13409  ioopnfsup  13437  icopnfsup  13438  modifeq2int  13506  suppssfz  13567  expmordi  13737  faclbnd4lem4  13862  hasheni  13914  hashgt0  13955  hashge1  13956  hashprb  13964  lennncl  14089  wrdsymb0  14104  ccatsymb  14139  ccatlid  14143  ccatass  14145  ccatswrd  14233  swrdccat2  14234  ccatpfx  14266  swrdccatfn  14289  swrdccat  14300  revccat  14331  2cshw  14378  cnpart  14803  resqreu  14816  recval  14886  abs1m  14899  abslem2  14903  fzomaxdiflem  14906  sqreulem  14923  sqreu  14924  limsupgre  15042  rlimdiv  15209  fsumparts  15370  climcnds  15415  expcnv  15428  ntrivcvg  15461  mod2eq1n2dvds  15908  ndvdssub  15970  sadcaddlem  16016  rplpwr  16119  dvdssqlem  16123  algcvgblem  16134  eucalgcvga  16143  isprm2lem  16238  powm2modprm  16356  coprimeprodsq  16361  pythagtriplem11  16378  pythagtriplem13  16380  pcadd2  16443  4sqlem11  16508  vdwlem6  16539  vdwlem8  16541  vdwlem10  16543  ramval  16561  ramcl2  16569  ramlb  16572  ram0  16575  mreintcl  17098  mrcval  17113  mrccl  17114  mrcuni  17124  mrcun  17125  acsfiel  17157  rescabs  17339  funcres  17402  setcmon  17593  setcepi  17594  fullestrcsetc  17658  funcsetcestrclem8  17669  fullsetcestrc  17673  yonffthlem  17790  pleval2i  17842  pospo  17851  poslubdg  17920  acsdrsel  18049  acsdrscl  18052  acsficl  18053  psss  18086  grpidd  18143  ismndd  18195  gsumsgrpccat  18266  gsumccatOLD  18267  gsumwmhm  18272  mulgaddcom  18515  subgmulg  18557  resghm  18638  conjnsg  18658  f1otrspeq  18839  pmtrval  18843  pmtrrn  18849  pmtrfinv  18853  pmtrprfval  18879  psgnunilem1  18885  psgnunilem5  18886  psgnunilem4  18889  psgneldm2i  18897  lsmelvalix  19030  pj1ghm  19093  efgredlemc  19135  frgp0  19150  qusabl  19250  cycsubgcyg  19286  gsumval3  19292  gsumcllem  19293  ablfac1c  19458  pgpfac1lem5  19466  isringd  19603  lspsneq0b  20050  lmodindp1  20051  lmhmf1o  20083  lmhmpreima  20085  reslmhm  20089  pwssplit3  20098  lspsncmp  20153  lspsneq  20159  znf1o  20516  dsmmlss  20706  frlmlbs  20759  frlmup1  20760  mpfind  21067  mhplss  21095  mat1  21344  chfacfisf  21751  chfacfisfcpmat  21752  uniopn  21794  ntrval  21933  clsval  21934  neival  21999  neiptopreu  22030  lpval  22036  restdis  22075  lmbrf  22157  cnpnei  22161  1stcrest  22350  hauspwdom  22398  lfinpfin  22421  txcnpi  22505  ptrescn  22536  xkococnlem  22556  qtopeu  22613  kqreglem1  22638  ptuncnv  22704  filss  22750  fsubbas  22764  fbasrn  22781  cfinfil  22790  ufinffr  22826  elfm3  22847  rnelfmlem  22849  rnelfm  22850  flimclslem  22881  flfval  22887  isfcf  22931  cnextfvval  22962  cnextf  22963  cnextcn  22964  ustelimasn  23120  trust  23127  restutop  23135  ustuqtop2  23140  utop2nei  23148  ucncn  23182  trcfilu  23191  cnextucn  23200  met1stc  23419  metustexhalf  23454  cfilucfil  23457  psmetutop  23465  nmoix  23627  nmoeq0  23634  idnghm  23641  blcvx  23695  xrsxmet  23706  iccntr  23718  icccmp  23722  iihalf1  23828  iihalf2  23830  xrhmeo  23843  cnheibor  23852  ipcau2  24131  lmmbrf  24159  iscauf  24177  cmetcaulem  24185  bcthlem4  24224  cmetcusp  24251  rrxcph  24289  minveclem4  24329  evthicc2  24357  cniccbdd  24358  ovollb2  24386  ovolunlem1a  24393  ovolunlem1  24394  voliun  24451  icombl  24461  ioombl  24462  iccvolcl  24464  ioovolcl  24467  mbfss  24543  mbfposb  24550  itg2const2  24639  itg2splitlem  24646  itg2gt0  24658  iblss2  24703  itgioo  24713  dvaddf  24839  dvmulf  24840  dvcobr  24843  dvcof  24845  rolle  24887  dvlip  24890  c1lip1  24894  dvivthlem1  24905  lhop1lem  24910  dvfsumlem1  24923  ftc1lem4  24936  ftc1lem5  24937  ply1divmo  25033  coe1termlem  25152  plydiveu  25191  taylplem1  25255  pserulm  25314  abelth  25333  abscxp2  25581  abscxpbnd  25639  logbgt0b  25676  ang180lem2  25693  ang180lem3  25694  isosctrlem1  25701  angpieqvd  25714  atandmtan  25803  birthdaylem3  25836  wilthlem2  25951  wilthimp  25954  isppw  25996  isppw2  25997  dvdsflsumcom  26070  chteq0  26090  perfectlem2  26111  dchrval  26115  dchrinvcl  26134  dchrptlem1  26145  bposlem3  26167  lgslem4  26181  lgsmod  26204  lgsdilem  26205  lgsdir2lem2  26207  lgsdir2  26211  lgsne0  26216  lgsmulsqcoprm  26224  lgseisenlem1  26256  2lgsoddprm  26297  2sqlem4  26302  chpo1ubb  26362  dchrisumn0  26402  pntrsumbnd2  26448  ostthlem1  26508  ostth3  26519  idmot  26628  tgelrnln  26721  lmimid  26885  lmiisolem  26887  hypcgrlem1  26890  brcgr  26991  colinearalglem4  27000  colinearalg  27001  axlowdimlem14  27046  axcontlem4  27058  cplgrop  27525  lfgriswlk  27776  pthdlem1  27853  crctcshwlkn0  27905  elwspths2on  28044  clwlkclwwlklem2fv2  28079  frgrncvvdeqlem9  28390  nvss  28674  sspn  28817  nmoub3i  28854  nmblolbii  28880  blocnilem  28885  minvecolem4  28961  htthlem  28998  norm1  29330  norm1exi  29331  pjeq  29480  axpjpj  29501  normcan  29657  pjoi0  29798  nmopub2tALT  29990  nmfnleub2  30007  eighmorth  30045  nmbdoplbi  30105  nmcoplbi  30109  nmophmi  30112  nmbdfnlbi  30130  nmcfnlbi  30133  riesz3i  30143  cnlnadjlem7  30154  branmfn  30186  nmopleid  30220  hstle  30311  superpos  30435  cvexchlem  30449  foresf1o  30569  elabreximd  30574  unidifsnne  30603  f1o3d  30681  fmptco1f1o  30687  funcnvmpt  30724  fgreu  30729  suppovss  30737  fsupprnfi  30746  resf1o  30785  fpwrelmap  30788  xrofsup  30810  eliccelico  30818  elicoelioo  30819  iocinif  30822  difioo  30823  eliccioo  30925  cshf1o  30954  mgcmnt1d  30994  mgcmnt2d  30995  pwrssmgc  30997  gsummpt2co  31027  gsumhashmul  31035  submomnd  31055  symgcom  31071  symgcom2  31072  odpmco  31074  pmtrcnel  31077  pmtridf1o  31080  cycpmco2lem6  31117  cycpmco2lem7  31118  cycpmco2  31119  cyc3co2  31126  cycpmconjv  31128  tocyccntz  31130  cyc3evpm  31136  cycpmconjslem2  31141  cycpmconjs  31142  archirngz  31162  ornglmullt  31225  orngrmullt  31226  lindssn  31287  linds2eq  31289  nsgqusf1olem1  31312  nsgqusf1olem3  31314  elrspunidl  31320  rhmimaidl  31323  prmidl2  31330  prmidl0  31340  qsidomlem1  31342  ssmxidl  31356  ply1scleq  31382  lbslsat  31413  lindsunlem  31419  lindsun  31420  dimkerim  31422  fedgmullem1  31424  fedgmullem2  31425  fedgmul  31426  madjusmdetlem2  31492  qtophaus  31500  locfinreflem  31504  zarclssn  31537  zarmxt1  31544  zarcmplem  31545  rhmpreimacn  31549  unitdivcld  31565  tpr2rico  31576  ordtrestNEW  31585  lmxrge0  31616  elzrhunit  31641  qqhf  31648  indf1ofs  31706  gsumesum  31739  esumfsup  31750  esumcvg  31766  issgon  31803  sigainb  31816  insiga  31817  isrnmeas  31880  measvunilem  31892  volmeas  31911  ddeval1  31914  ddeval0  31915  imambfm  31941  omssubadd  31979  carsgclctunlem3  31999  eulerpartlemf  32049  eulerpartlemgvv  32055  probun  32098  dstfrvunirn  32153  plymulx  32239  signslema  32253  signstfvn  32260  signsvtn0  32261  signstfvneq0  32263  signstres  32266  signstfveq0a  32267  breprexplemc  32324  logdivsqrle  32342  hgt750lemg  32346  tgoldbachgtda  32353  tgoldbachgt  32355  lpadmax  32374  lpadleft  32375  lpadright  32376  bnj529  32433  bnj548  32590  bnj570  32598  bnj852  32614  bnj929  32629  bnj1097  32674  bnj1118  32677  bnj1145  32686  funen1cnv  32773  spthcycl  32804  acycgr0v  32823  derangen  32847  subfacp1lem2b  32856  subfacp1lem4  32858  subfacp1lem5  32859  derangfmla  32865  ptpconn  32908  mppspstlem  33246  ttrcltr  33515  wsuclem  33556  nosupbnd2lem1  33655  noinfbnd2lem1  33670  nocvxmin  33710  eqscut2  33737  sltlpss  33824  colinearex  34099  btwnconn1lem11  34136  btwnconn1lem12  34137  fwddifnp1  34204  nn0prpwlem  34248  bj-snmoore  35019  bj-imdiridlem  35091  relowlpssretop  35272  fin2so  35501  matunitlindflem2  35511  ptrecube  35514  poimirlem8  35522  poimirlem13  35527  poimirlem15  35529  poimirlem24  35538  poimirlem25  35539  poimirlem26  35540  heicant  35549  mblfinlem2  35552  voliunnfl  35558  mbfresfi  35560  itg2addnclem  35565  itg2addnclem3  35567  itg2gt0cn  35569  ftc1cnnclem  35585  ftc1anclem5  35591  cover2  35609  indexdom  35629  sdclem1  35638  fdc  35640  equivbnd2  35687  heiborlem8  35713  heibor  35716  isdrngo2  35853  iscringd  35893  smprngopr  35947  prnc  35962  eqeltr  36118  islfld  36813  lkrshpor  36858  lfl1dim  36872  lfl1dim2N  36873  cmtcomlemN  36999  2lplnmN  37310  pmapjat1  37604  trlnid  37930  tendoex  38726  dia1dimid  38814  dibval2  38895  dihmeetlem2N  39050  dochlkr  39136  mapdcv  39411  hdmaplkr  39664  hdmapip0  39666  hlhillcs  39709  frlmvscadiccat  39950  mhphf  39995  dvdsexpnn  40048  nacsfix  40237  3rexfrabdioph  40322  4rexfrabdioph  40323  6rexfrabdioph  40324  7rexfrabdioph  40325  eldioph4b  40336  pellexlem2  40355  pellexlem5  40358  jm2.26lem3  40526  numinfctb  40631  ntrclsfv1  41342  ntrneifv1  41366  ntrneifv2  41367  cvgdvgrat  41604  radcnvrat  41605  dvconstbi  41625  bccbc  41636  elpwgded  41857  elpwgdedVD  42210  sspwimpcf  42213  sspwimpcfVD  42214  sspwimpALT2  42221  ax6e2ndeqALT  42224  eliuniin  42322  eliuniin2  42342  qinioo  42748  dfxlim2v  43063  xlimliminflimsup  43078  cncfiooicclem1  43109  ibliooicc  43187  stoweidlem27  43243  stoweidlem28  43244  fourierdlem89  43411  fourierdlem91  43413  fourierdlem92  43414  smflimmpt  44015  odz2prm2pw  44688  perfectALTVlem2  44847  blen1b  45607  naryfvalelfv  45651  itscnhlc0yqe  45778  itsclquadb  45795  lubeldm2  45923  glbeldm2  45924  ipolub  45947  ipoglb  45950  functhinclem1  45995  thincciso  46003  prsthinc  46008  prstchom2ALT  46031  onetansqsecsq  46134  cotsqcscsq  46135  aacllem  46176