Theorem biimpar 477

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

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

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 396

This theorem is referenced by:  bitr  801  exbiri  807  biadanid  819  oplem1  1053  eqtr  2761  pm13.181  3025  opabss  5134  axprlem4  5344  axprlem5  5345  euotd  5421  brcogw  5766  somin1  6027  xpdifid  6060  funfni  6523  fncoOLD  6534  fnssres  6539  fn0  6548  fnimadisj  6549  fnimaeq0  6550  foimacnv  6717  fvelimab  6823  dffv2  6845  fvopab3ig  6853  dff3  6958  dffo4  6961  fpr2g  7069  f1eqcocnv  7153  f1eqcocnvOLD  7154  isomin  7188  f1ocnv2d  7500  fnexALT  7767  xp1st  7836  xp2nd  7837  frrlem3  8075  fpr2  8091  wfr3g  8109  wfrlem3OLD  8112  wfrlem4OLD  8114  wfr2  8138  iinon  8142  tfr3  8201  oawordri  8343  oaass  8354  omeulem1  8375  oeoa  8390  oeoe  8392  oeeulem  8394  ecelqsg  8519  elqsn0  8533  pwdom  8865  enfii  8932  marypha1lem  9122  wofib  9234  cantnff  9362  cantnfp1  9369  cantnf  9381  cnfcomlem  9387  frr3g  9445  r1sscl  9474  rankval3b  9515  infxpidm2  9704  numdom  9725  onssnum  9727  acni  9732  acni2  9733  dfac5  9815  djulepw  9879  infunsdom1  9900  infunsdom  9901  cofsmo  9956  cfsmolem  9957  fin1ai  9980  fin2i  9982  isf34lem1  10059  fin67  10082  itunisuc  10106  axdc3lem4  10140  zornn0g  10192  ttukeylem6  10201  brdom3  10215  tsken  10441  tskcard  10468  r1tskina  10469  intgru  10501  prlem934  10720  ltexprlem7  10729  supaddc  11872  mul2lt0rlt0  12761  xrmaxeq  12842  xrmineq  12843  xmulneg1  12932  ixxun  13024  difelfzle  13298  ssfzoulel  13409  elfznelfzo  13420  ico01fl0  13467  btwnzge0  13476  ltdifltdiv  13482  ioopnfsup  13512  icopnfsup  13513  modifeq2int  13581  suppssfz  13642  expmordi  13813  faclbnd4lem4  13938  hasheni  13990  hashgt0  14031  hashge1  14032  hashprb  14040  lennncl  14165  wrdsymb0  14180  ccatsymb  14215  ccatlid  14219  ccatass  14221  ccatswrd  14309  swrdccat2  14310  ccatpfx  14342  swrdccatfn  14365  swrdccat  14376  revccat  14407  2cshw  14454  cnpart  14879  resqreu  14892  recval  14962  abs1m  14975  abslem2  14979  fzomaxdiflem  14982  sqreulem  14999  sqreu  15000  limsupgre  15118  rlimdiv  15285  fsumparts  15446  climcnds  15491  expcnv  15504  ntrivcvg  15537  mod2eq1n2dvds  15984  ndvdssub  16046  sadcaddlem  16092  rplpwr  16195  dvdssqlem  16199  algcvgblem  16210  eucalgcvga  16219  isprm2lem  16314  powm2modprm  16432  coprimeprodsq  16437  pythagtriplem11  16454  pythagtriplem13  16456  pcadd2  16519  4sqlem11  16584  vdwlem6  16615  vdwlem8  16617  vdwlem10  16619  ramval  16637  ramcl2  16645  ramlb  16648  ram0  16651  mreintcl  17221  mrcval  17236  mrccl  17237  mrcuni  17247  mrcun  17248  acsfiel  17280  rescabs  17464  funcres  17527  setcmon  17718  setcepi  17719  fullestrcsetc  17784  funcsetcestrclem8  17795  fullsetcestrc  17799  yonffthlem  17916  pleval2i  17969  pospo  17978  poslubdg  18047  acsdrsel  18176  acsdrscl  18179  acsficl  18180  psss  18213  grpidd  18270  ismndd  18322  gsumsgrpccat  18393  gsumccatOLD  18394  gsumwmhm  18399  mulgaddcom  18642  subgmulg  18684  resghm  18765  conjnsg  18785  f1otrspeq  18970  pmtrval  18974  pmtrrn  18980  pmtrfinv  18984  pmtrprfval  19010  psgnunilem1  19016  psgnunilem5  19017  psgnunilem4  19020  psgneldm2i  19028  lsmelvalix  19161  pj1ghm  19224  efgredlemc  19266  frgp0  19281  qusabl  19381  cycsubgcyg  19417  gsumval3  19423  gsumcllem  19424  ablfac1c  19589  pgpfac1lem5  19597  isringd  19739  lspsneq0b  20190  lmodindp1  20191  lmhmf1o  20223  lmhmpreima  20225  reslmhm  20229  pwssplit3  20238  lspsncmp  20293  lspsneq  20299  znf1o  20671  dsmmlss  20861  frlmlbs  20914  frlmup1  20915  mpfind  21227  mhplss  21255  mat1  21504  chfacfisf  21911  chfacfisfcpmat  21912  uniopn  21954  ntrval  22095  clsval  22096  neival  22161  neiptopreu  22192  lpval  22198  restdis  22237  lmbrf  22319  cnpnei  22323  1stcrest  22512  hauspwdom  22560  lfinpfin  22583  txcnpi  22667  ptrescn  22698  xkococnlem  22718  qtopeu  22775  kqreglem1  22800  ptuncnv  22866  filss  22912  fsubbas  22926  fbasrn  22943  cfinfil  22952  ufinffr  22988  elfm3  23009  rnelfmlem  23011  rnelfm  23012  flimclslem  23043  flfval  23049  isfcf  23093  cnextfvval  23124  cnextf  23125  cnextcn  23126  ustelimasn  23282  trust  23289  restutop  23297  ustuqtop2  23302  utop2nei  23310  ucncn  23345  trcfilu  23354  cnextucn  23363  met1stc  23583  metustexhalf  23618  cfilucfil  23621  psmetutop  23629  nmoix  23799  nmoeq0  23806  idnghm  23813  blcvx  23867  xrsxmet  23878  iccntr  23890  icccmp  23894  iihalf1  24000  iihalf2  24002  xrhmeo  24015  cnheibor  24024  ipcau2  24303  lmmbrf  24331  iscauf  24349  cmetcaulem  24357  bcthlem4  24396  cmetcusp  24423  rrxcph  24461  minveclem4  24501  evthicc2  24529  cniccbdd  24530  ovollb2  24558  ovolunlem1a  24565  ovolunlem1  24566  voliun  24623  icombl  24633  ioombl  24634  iccvolcl  24636  ioovolcl  24639  mbfss  24715  mbfposb  24722  itg2const2  24811  itg2splitlem  24818  itg2gt0  24830  iblss2  24875  itgioo  24885  dvaddf  25011  dvmulf  25012  dvcobr  25015  dvcof  25017  rolle  25059  dvlip  25062  c1lip1  25066  dvivthlem1  25077  lhop1lem  25082  dvfsumlem1  25095  ftc1lem4  25108  ftc1lem5  25109  ply1divmo  25205  coe1termlem  25324  plydiveu  25363  taylplem1  25427  pserulm  25486  abelth  25505  abscxp2  25753  abscxpbnd  25811  logbgt0b  25848  ang180lem2  25865  ang180lem3  25866  isosctrlem1  25873  angpieqvd  25886  atandmtan  25975  birthdaylem3  26008  wilthlem2  26123  wilthimp  26126  isppw  26168  isppw2  26169  dvdsflsumcom  26242  chteq0  26262  perfectlem2  26283  dchrval  26287  dchrinvcl  26306  dchrptlem1  26317  bposlem3  26339  lgslem4  26353  lgsmod  26376  lgsdilem  26377  lgsdir2lem2  26379  lgsdir2  26383  lgsne0  26388  lgsmulsqcoprm  26396  lgseisenlem1  26428  2lgsoddprm  26469  2sqlem4  26474  chpo1ubb  26534  dchrisumn0  26574  pntrsumbnd2  26620  ostthlem1  26680  ostth3  26691  idmot  26802  tgelrnln  26895  lmimid  27059  lmiisolem  27061  hypcgrlem1  27064  brcgr  27171  colinearalglem4  27180  colinearalg  27181  axlowdimlem14  27226  axcontlem4  27238  cplgrop  27707  lfgriswlk  27958  pthdlem1  28035  crctcshwlkn0  28087  elwspths2on  28226  clwlkclwwlklem2fv2  28261  frgrncvvdeqlem9  28572  nvss  28856  sspn  28999  nmoub3i  29036  nmblolbii  29062  blocnilem  29067  minvecolem4  29143  htthlem  29180  norm1  29512  norm1exi  29513  pjeq  29662  axpjpj  29683  normcan  29839  pjoi0  29980  nmopub2tALT  30172  nmfnleub2  30189  eighmorth  30227  nmbdoplbi  30287  nmcoplbi  30291  nmophmi  30294  nmbdfnlbi  30312  nmcfnlbi  30315  riesz3i  30325  cnlnadjlem7  30336  branmfn  30368  nmopleid  30402  hstle  30493  superpos  30617  cvexchlem  30631  foresf1o  30751  elabreximd  30756  unidifsnne  30785  f1o3d  30863  fmptco1f1o  30869  funcnvmpt  30906  fgreu  30911  suppovss  30919  fsupprnfi  30928  resf1o  30967  fpwrelmap  30970  xrofsup  30992  eliccelico  31000  elicoelioo  31001  iocinif  31004  difioo  31005  eliccioo  31107  cshf1o  31136  mgcmnt1d  31177  mgcmnt2d  31178  pwrssmgc  31180  gsummpt2co  31210  gsumhashmul  31218  submomnd  31238  symgcom  31254  symgcom2  31255  odpmco  31257  pmtrcnel  31260  pmtridf1o  31263  cycpmco2lem6  31300  cycpmco2lem7  31301  cycpmco2  31302  cyc3co2  31309  cycpmconjv  31311  tocyccntz  31313  cyc3evpm  31319  cycpmconjslem2  31324  cycpmconjs  31325  archirngz  31345  ornglmullt  31408  orngrmullt  31409  lindssn  31475  linds2eq  31477  nsgqusf1olem1  31500  nsgqusf1olem3  31502  elrspunidl  31508  rhmimaidl  31511  prmidl2  31518  prmidl0  31528  qsidomlem1  31530  ssmxidl  31544  ply1scleq  31570  lbslsat  31601  lindsunlem  31607  lindsun  31608  dimkerim  31610  fedgmullem1  31612  fedgmullem2  31613  fedgmul  31614  madjusmdetlem2  31680  qtophaus  31688  locfinreflem  31692  zarclssn  31725  zarmxt1  31732  zarcmplem  31733  rhmpreimacn  31737  unitdivcld  31753  tpr2rico  31764  ordtrestNEW  31773  lmxrge0  31804  elzrhunit  31829  qqhf  31836  indf1ofs  31894  gsumesum  31927  esumfsup  31938  esumcvg  31954  issgon  31991  sigainb  32004  insiga  32005  isrnmeas  32068  measvunilem  32080  volmeas  32099  ddeval1  32102  ddeval0  32103  imambfm  32129  omssubadd  32167  carsgclctunlem3  32187  eulerpartlemf  32237  eulerpartlemgvv  32243  probun  32286  dstfrvunirn  32341  plymulx  32427  signslema  32441  signstfvn  32448  signsvtn0  32449  signstfvneq0  32451  signstres  32454  signstfveq0a  32455  breprexplemc  32512  logdivsqrle  32530  hgt750lemg  32534  tgoldbachgtda  32541  tgoldbachgt  32543  lpadmax  32562  lpadleft  32563  lpadright  32564  bnj529  32621  bnj548  32777  bnj570  32785  bnj852  32801  bnj929  32816  bnj1097  32861  bnj1118  32864  bnj1145  32873  funen1cnv  32960  spthcycl  32991  acycgr0v  33010  derangen  33034  subfacp1lem2b  33043  subfacp1lem4  33045  subfacp1lem5  33046  derangfmla  33052  ptpconn  33095  mppspstlem  33433  ttrcltr  33702  wsuclem  33746  nosupbnd2lem1  33845  noinfbnd2lem1  33860  nocvxmin  33900  eqscut2  33927  sltlpss  34014  colinearex  34289  btwnconn1lem11  34326  btwnconn1lem12  34327  fwddifnp1  34394  nn0prpwlem  34438  bj-snmoore  35211  bj-imdiridlem  35283  relowlpssretop  35462  fin2so  35691  matunitlindflem2  35701  ptrecube  35704  poimirlem8  35712  poimirlem13  35717  poimirlem15  35719  poimirlem24  35728  poimirlem25  35729  poimirlem26  35730  heicant  35739  mblfinlem2  35742  voliunnfl  35748  mbfresfi  35750  itg2addnclem  35755  itg2addnclem3  35757  itg2gt0cn  35759  ftc1cnnclem  35775  ftc1anclem5  35781  cover2  35799  indexdom  35819  sdclem1  35828  fdc  35830  equivbnd2  35877  heiborlem8  35903  heibor  35906  isdrngo2  36043  iscringd  36083  smprngopr  36137  prnc  36152  eqeltr  36308  islfld  37003  lkrshpor  37048  lfl1dim  37062  lfl1dim2N  37063  cmtcomlemN  37189  2lplnmN  37500  pmapjat1  37794  trlnid  38120  tendoex  38916  dia1dimid  39004  dibval2  39085  dihmeetlem2N  39240  dochlkr  39326  mapdcv  39601  hdmaplkr  39854  hdmapip0  39856  hlhillcs  39903  frlmvscadiccat  40163  mhphf  40208  dvdsexpnn  40261  nacsfix  40450  3rexfrabdioph  40535  4rexfrabdioph  40536  6rexfrabdioph  40537  7rexfrabdioph  40538  eldioph4b  40549  pellexlem2  40568  pellexlem5  40571  jm2.26lem3  40739  numinfctb  40844  ntrclsfv1  41554  ntrneifv1  41578  ntrneifv2  41579  cvgdvgrat  41820  radcnvrat  41821  dvconstbi  41841  bccbc  41852  elpwgded  42073  elpwgdedVD  42426  sspwimpcf  42429  sspwimpcfVD  42430  sspwimpALT2  42437  ax6e2ndeqALT  42440  eliuniin  42538  eliuniin2  42558  qinioo  42963  dfxlim2v  43278  xlimliminflimsup  43293  cncfiooicclem1  43324  ibliooicc  43402  stoweidlem27  43458  stoweidlem28  43459  fourierdlem89  43626  fourierdlem91  43628  fourierdlem92  43629  smflimmpt  44230  odz2prm2pw  44903  perfectALTVlem2  45062  blen1b  45822  naryfvalelfv  45866  itscnhlc0yqe  45993  itsclquadb  46010  lubeldm2  46138  glbeldm2  46139  ipolub  46162  ipoglb  46165  functhinclem1  46210  thincciso  46218  prsthinc  46223  prstchom2ALT  46246  onetansqsecsq  46349  cotsqcscsq  46350  aacllem  46391