Theorem biimpar 479

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  bitr  804  exbiri  810  biadanid  822  oplem1  1056  eqtr  2756  pm13.181  3024  opabss  5213  axprlem4  5425  axprlem5  5426  euotd  5514  brcogw  5869  somin1  6135  xpdifid  6168  funfni  6656  fncoOLD  6669  fnssres  6674  fn0  6682  fnimadisj  6683  fnimaeq0  6684  foimacnv  6851  fvelimab  6965  dffv2  6987  fvopab3ig  6995  dff3  7102  dffo4  7105  fpr2g  7213  f1eqcocnv  7299  f1eqcocnvOLD  7300  isomin  7334  f1ocnv2d  7659  fnexALT  7937  xp1st  8007  xp2nd  8008  frrlem3  8273  fpr2  8289  wfr3g  8307  wfrlem3OLD  8310  wfrlem4OLD  8312  wfr2  8336  iinon  8340  tfr3  8399  oawordri  8550  oaass  8561  omeulem1  8582  oeoa  8597  oeoe  8599  oeeulem  8601  ecelqsg  8766  elqsn0  8780  pwdom  9129  enfii  9189  phpeqd  9215  ominf  9258  findcard3  9285  marypha1lem  9428  wofib  9540  cantnff  9669  cantnfp1  9676  cantnf  9688  cnfcomlem  9694  ttrcltr  9711  frr3g  9751  r1sscl  9780  rankval3b  9821  infxpidm2  10012  numdom  10033  onssnum  10035  acni  10040  acni2  10041  dfac5  10123  djulepw  10187  infunsdom1  10208  infunsdom  10209  cofsmo  10264  cfsmolem  10265  fin1ai  10288  fin2i  10290  isf34lem1  10367  fin67  10390  itunisuc  10414  axdc3lem4  10448  zornn0g  10500  ttukeylem6  10509  brdom3  10523  tsken  10749  tskcard  10776  r1tskina  10777  intgru  10809  prlem934  11028  ltexprlem7  11037  supaddc  12181  mul2lt0rlt0  13076  xrmaxeq  13158  xrmineq  13159  xmulneg1  13248  ixxun  13340  difelfzle  13614  ssfzoulel  13726  elfznelfzo  13737  ico01fl0  13784  btwnzge0  13793  ltdifltdiv  13799  ioopnfsup  13829  icopnfsup  13830  modifeq2int  13898  suppssfz  13959  expmordi  14132  zzlesq  14170  faclbnd4lem4  14256  hasheni  14308  hashgt0  14348  hashge1  14349  hashprb  14357  lennncl  14484  wrdsymb0  14499  ccatsymb  14532  ccatlid  14536  ccatass  14538  ccatswrd  14618  swrdccat2  14619  ccatpfx  14651  swrdccatfn  14674  swrdccat  14685  revccat  14716  2cshw  14763  cnpart  15187  resqreu  15199  recval  15269  abs1m  15282  abslem2  15286  fzomaxdiflem  15289  sqreulem  15306  sqreu  15307  limsupgre  15425  rlimdiv  15592  fsumparts  15752  climcnds  15797  expcnv  15810  ntrivcvg  15843  mod2eq1n2dvds  16290  ndvdssub  16352  sadcaddlem  16398  rplpwr  16499  dvdssqlem  16503  algcvgblem  16514  eucalgcvga  16523  isprm2lem  16618  powm2modprm  16736  coprimeprodsq  16741  pythagtriplem11  16758  pythagtriplem13  16760  pcadd2  16823  4sqlem11  16888  vdwlem6  16919  vdwlem8  16921  vdwlem10  16923  ramval  16941  ramcl2  16949  ramlb  16952  ram0  16955  mreintcl  17539  mrcval  17554  mrccl  17555  mrcuni  17565  mrcun  17566  acsfiel  17598  rescabs  17782  rescabsOLD  17783  funcres  17846  setcmon  18037  setcepi  18038  fullestrcsetc  18103  funcsetcestrclem8  18114  fullsetcestrc  18118  yonffthlem  18235  pleval2i  18289  pospo  18298  poslubdg  18367  acsdrsel  18496  acsdrscl  18499  acsficl  18500  psss  18533  grpidd  18590  ismndd  18647  gsumsgrpccat  18721  gsumwmhm  18726  mulgaddcom  18978  subgmulg  19020  resghm  19108  conjnsg  19128  f1otrspeq  19315  pmtrval  19319  pmtrrn  19325  pmtrfinv  19329  pmtrprfval  19355  psgnunilem1  19361  psgnunilem5  19362  psgnunilem4  19365  psgneldm2i  19373  lsmelvalix  19509  pj1ghm  19571  efgredlemc  19613  frgp0  19628  qusabl  19733  cycsubgcyg  19769  gsumval3  19775  gsumcllem  19776  ablfac1c  19941  pgpfac1lem5  19949  isringd  20105  01eq0ring  20305  lspsneq0b  20624  lmodindp1  20625  lmhmf1o  20657  lmhmpreima  20659  reslmhm  20663  pwssplit3  20672  lspsncmp  20729  lspsneq  20735  znf1o  21107  dsmmlss  21299  frlmlbs  21352  frlmup1  21353  psrgrp  21517  mpfind  21670  mhplss  21698  mat1  21949  chfacfisf  22356  chfacfisfcpmat  22357  uniopn  22399  ntrval  22540  clsval  22541  neival  22606  neiptopreu  22637  lpval  22643  restdis  22682  lmbrf  22764  cnpnei  22768  1stcrest  22957  hauspwdom  23005  lfinpfin  23028  txcnpi  23112  ptrescn  23143  xkococnlem  23163  qtopeu  23220  kqreglem1  23245  ptuncnv  23311  filss  23357  fsubbas  23371  fbasrn  23388  cfinfil  23397  ufinffr  23433  elfm3  23454  rnelfmlem  23456  rnelfm  23457  flimclslem  23488  flfval  23494  isfcf  23538  cnextfvval  23569  cnextf  23570  cnextcn  23571  ustelimasn  23727  trust  23734  restutop  23742  ustuqtop2  23747  utop2nei  23755  ucncn  23790  trcfilu  23799  cnextucn  23808  met1stc  24030  metustexhalf  24065  cfilucfil  24068  psmetutop  24076  nmoix  24246  nmoeq0  24253  idnghm  24260  blcvx  24314  xrsxmet  24325  iccntr  24337  icccmp  24341  iihalf1  24447  iihalf2  24449  xrhmeo  24462  cnheibor  24471  ipcau2  24751  lmmbrf  24779  iscauf  24797  cmetcaulem  24805  bcthlem4  24844  cmetcusp  24871  rrxcph  24909  minveclem4  24949  evthicc2  24977  cniccbdd  24978  ovollb2  25006  ovolunlem1a  25013  ovolunlem1  25014  voliun  25071  icombl  25081  ioombl  25082  iccvolcl  25084  ioovolcl  25087  mbfss  25163  mbfposb  25170  itg2const2  25259  itg2splitlem  25266  itg2gt0  25278  iblss2  25323  itgioo  25333  dvaddf  25459  dvmulf  25460  dvcobr  25463  dvcof  25465  rolle  25507  dvlip  25510  c1lip1  25514  dvivthlem1  25525  lhop1lem  25530  dvfsumlem1  25543  ftc1lem4  25556  ftc1lem5  25557  ply1divmo  25653  coe1termlem  25772  plydiveu  25811  taylplem1  25875  pserulm  25934  abelth  25953  abscxp2  26201  abscxpbnd  26261  logbgt0b  26298  ang180lem2  26315  ang180lem3  26316  isosctrlem1  26323  angpieqvd  26336  atandmtan  26425  birthdaylem3  26458  wilthlem2  26573  wilthimp  26576  isppw  26618  isppw2  26619  dvdsflsumcom  26692  chteq0  26712  perfectlem2  26733  dchrval  26737  dchrinvcl  26756  dchrptlem1  26767  bposlem3  26789  lgslem4  26803  lgsmod  26826  lgsdilem  26827  lgsdir2lem2  26829  lgsdir2  26833  lgsne0  26838  lgsmulsqcoprm  26846  lgseisenlem1  26878  2lgsoddprm  26919  2sqlem4  26924  chpo1ubb  26984  dchrisumn0  27024  pntrsumbnd2  27070  ostthlem1  27130  ostth3  27141  nosupbnd2lem1  27218  noinfbnd2lem1  27233  nocvxmin  27280  eqscut2  27307  sltlpss  27401  idmot  27788  tgelrnln  27881  lmimid  28045  lmiisolem  28047  hypcgrlem1  28050  brcgr  28158  colinearalglem4  28167  colinearalg  28168  axlowdimlem14  28213  axcontlem4  28225  cplgrop  28694  lfgriswlk  28945  pthdlem1  29023  crctcshwlkn0  29075  elwspths2on  29214  clwlkclwwlklem2fv2  29249  frgrncvvdeqlem9  29560  nvss  29846  sspn  29989  nmoub3i  30026  nmblolbii  30052  blocnilem  30057  minvecolem4  30133  htthlem  30170  norm1  30502  norm1exi  30503  pjeq  30652  axpjpj  30673  normcan  30829  pjoi0  30970  nmopub2tALT  31162  nmfnleub2  31179  eighmorth  31217  nmbdoplbi  31277  nmcoplbi  31281  nmophmi  31284  nmbdfnlbi  31302  nmcfnlbi  31305  riesz3i  31315  cnlnadjlem7  31326  branmfn  31358  nmopleid  31392  hstle  31483  superpos  31607  cvexchlem  31621  foresf1o  31742  elabreximd  31747  unidifsnne  31773  f1o3d  31851  fmptco1f1o  31857  funcnvmpt  31892  fgreu  31897  suppovss  31906  fsupprnfi  31914  resf1o  31955  fpwrelmap  31958  xrofsup  31980  eliccelico  31988  elicoelioo  31989  iocinif  31992  difioo  31993  eliccioo  32097  cshf1o  32126  mgcmnt1d  32167  mgcmnt2d  32168  pwrssmgc  32170  gsummpt2co  32200  gsumhashmul  32208  submomnd  32228  symgcom  32244  symgcom2  32245  odpmco  32247  pmtrcnel  32250  pmtridf1o  32253  cycpmco2lem6  32290  cycpmco2lem7  32291  cycpmco2  32292  cyc3co2  32299  cycpmconjv  32301  tocyccntz  32303  cyc3evpm  32309  cycpmconjslem2  32314  cycpmconjs  32315  archirngz  32335  isdrng4  32395  sdrgdvcl  32397  sdrginvcl  32398  ornglmullt  32425  orngrmullt  32426  dvdsrspss  32491  lindssn  32494  linds2eq  32497  nsgqusf1olem1  32524  nsgqusf1olem3  32526  ghmqusker  32532  unitpidl1  32542  elrspunidl  32546  rhmimaidl  32550  drngidlhash  32552  prmidl2  32559  prmidl0  32569  qsidomlem1  32571  mxidlirredi  32587  mxidlirred  32588  ssmxidl  32590  drng0mxidl  32592  opprmxidlabs  32601  qsdrngilem  32608  qsdrngi  32609  qsdrng  32611  ply1scleq  32639  ply1asclunit  32654  ply1degltlss  32667  ply1gsumz  32669  lbslsat  32701  ply1degltdimlem  32707  lindsunlem  32709  lindsun  32710  dimkerim  32712  fedgmullem1  32714  fedgmullem2  32715  fedgmul  32716  irngss  32751  0ringirng  32753  irngnzply1  32755  irngnminplynz  32771  algextdeglem1  32772  madjusmdetlem2  32808  qtophaus  32816  locfinreflem  32820  zarclssn  32853  zarmxt1  32860  zarcmplem  32861  rhmpreimacn  32865  unitdivcld  32881  tpr2rico  32892  ordtrestNEW  32901  lmxrge0  32932  elzrhunit  32959  qqhf  32966  indf1ofs  33024  gsumesum  33057  esumfsup  33068  esumcvg  33084  issgon  33121  sigainb  33134  insiga  33135  isrnmeas  33198  measvunilem  33210  volmeas  33229  ddeval1  33232  ddeval0  33233  imambfm  33261  omssubadd  33299  carsgclctunlem3  33319  eulerpartlemf  33369  eulerpartlemgvv  33375  probun  33418  dstfrvunirn  33473  plymulx  33559  signslema  33573  signstfvn  33580  signsvtn0  33581  signstfvneq0  33583  signstres  33586  signstfveq0a  33587  breprexplemc  33644  logdivsqrle  33662  hgt750lemg  33666  tgoldbachgtda  33673  tgoldbachgt  33675  lpadmax  33694  lpadleft  33695  lpadright  33696  bnj529  33752  bnj548  33908  bnj570  33916  bnj852  33932  bnj929  33947  bnj1097  33992  bnj1118  33995  bnj1145  34004  funen1cnv  34091  spthcycl  34120  acycgr0v  34139  derangen  34163  subfacp1lem2b  34172  subfacp1lem4  34174  subfacp1lem5  34175  derangfmla  34181  ptpconn  34224  mppspstlem  34562  wsuclem  34797  colinearex  35032  btwnconn1lem11  35069  btwnconn1lem12  35070  fwddifnp1  35137  gg-dvcobr  35176  nn0prpwlem  35207  bj-snmoore  35994  bj-imdiridlem  36066  relowlpssretop  36245  fin2so  36475  matunitlindflem2  36485  ptrecube  36488  poimirlem8  36496  poimirlem13  36501  poimirlem15  36503  poimirlem24  36512  poimirlem25  36513  poimirlem26  36514  heicant  36523  mblfinlem2  36526  voliunnfl  36532  mbfresfi  36534  itg2addnclem  36539  itg2addnclem3  36541  itg2gt0cn  36543  ftc1cnnclem  36559  ftc1anclem5  36565  cover2  36583  indexdom  36602  sdclem1  36611  fdc  36613  equivbnd2  36660  heiborlem8  36686  heibor  36689  isdrngo2  36826  iscringd  36866  smprngopr  36920  prnc  36935  eqbrtr  37098  eqeltr  37100  islfld  37932  lkrshpor  37977  lfl1dim  37991  lfl1dim2N  37992  cmtcomlemN  38118  2lplnmN  38430  pmapjat1  38724  trlnid  39050  tendoex  39846  dia1dimid  39934  dibval2  40015  dihmeetlem2N  40170  dochlkr  40256  mapdcv  40531  hdmaplkr  40784  hdmapip0  40786  hlhillcs  40833  frlmvscadiccat  41080  dvdsexpnn  41231  nacsfix  41450  3rexfrabdioph  41535  4rexfrabdioph  41536  6rexfrabdioph  41537  7rexfrabdioph  41538  eldioph4b  41549  pellexlem2  41568  pellexlem5  41571  jm2.26lem3  41740  numinfctb  41845  ordne0gt0  42011  omge1  42047  omlim2  42049  omord2lim  42050  omord2i  42051  tfsconcatfv  42091  tfsconcatb0  42094  oaun3lem1  42124  ntrclsfv1  42806  ntrneifv1  42830  ntrneifv2  42831  cvgdvgrat  43072  radcnvrat  43073  dvconstbi  43093  bccbc  43104  elpwgded  43325  elpwgdedVD  43678  sspwimpcf  43681  sspwimpcfVD  43682  sspwimpALT2  43689  ax6e2ndeqALT  43692  eliuniin  43788  eliuniin2  43809  qinioo  44248  dfxlim2v  44563  xlimliminflimsup  44578  cncfiooicclem1  44609  ibliooicc  44687  stoweidlem27  44743  stoweidlem28  44744  fourierdlem89  44911  fourierdlem91  44913  fourierdlem92  44914  smflimmpt  45526  odz2prm2pw  46231  perfectALTVlem2  46390  isrngd  46672  blen1b  47274  naryfvalelfv  47318  itscnhlc0yqe  47445  itsclquadb  47462  lubeldm2  47589  glbeldm2  47590  ipolub  47613  ipoglb  47616  functhinclem1  47661  thincciso  47669  prsthinc  47674  prstchom2ALT  47699  onetansqsecsq  47806  cotsqcscsq  47807  aacllem  47848