Theorem biimpar 480

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  bitr  803  exbiri  809  oplem1  1051  eqtr  2843  opabss  5132  axprlem4  5329  axprlem5  5330  euotd  5405  brcogw  5741  somin1  5995  xpdifid  6027  funfni  6459  fnco  6467  fnssres  6472  fn0  6481  fnimadisj  6482  fnimaeq0  6483  foco  6604  foimacnv  6634  fvelimab  6739  dffv2  6758  fvopab3ig  6766  dff3  6868  dffo4  6871  fpr2g  6976  f1eqcocnv  7059  isomin  7092  f1ocnv2d  7400  fnexALT  7654  xp1st  7723  xp2nd  7724  wfr3g  7955  wfrlem3  7958  wfrlem4  7960  iinon  7979  tfr3  8037  oawordri  8178  oaass  8189  omeulem1  8210  oeoa  8225  oeoe  8227  oeeulem  8229  ecelqsg  8354  elqsn0  8368  pwdom  8671  marypha1lem  8899  wofib  9011  cantnff  9139  cantnfp1  9146  cantnf  9158  cnfcomlem  9164  r1sscl  9216  rankval3b  9257  infxpidm2  9445  numdom  9466  onssnum  9468  acni  9473  acni2  9474  dfac5  9556  djulepw  9620  infunsdom1  9637  infunsdom  9638  cofsmo  9693  cfsmolem  9694  fin1ai  9717  fin2i  9719  isf34lem1  9796  fin67  9819  itunisuc  9843  axdc3lem4  9877  zornn0g  9929  ttukeylem6  9938  brdom3  9952  tsken  10178  tskcard  10205  r1tskina  10206  intgru  10238  prlem934  10457  ltexprlem7  10466  supaddc  11610  mul2lt0rlt0  12494  xrmaxeq  12575  xrmineq  12576  xmulneg1  12665  ixxun  12757  difelfzle  13023  ssfzoulel  13134  elfznelfzo  13145  ico01fl0  13192  btwnzge0  13201  ltdifltdiv  13207  ioopnfsup  13235  icopnfsup  13236  modifeq2int  13304  suppssfz  13365  expmordi  13534  faclbnd4lem4  13659  hasheni  13711  hashgt0  13752  hashge1  13753  hashprb  13761  lennncl  13886  wrdsymb0  13903  ccatsymb  13938  ccatlid  13942  ccatass  13944  ccatswrd  14032  swrdccat2  14033  ccatpfx  14065  swrdccatfn  14088  swrdccat  14099  revccat  14130  2cshw  14177  cnpart  14601  resqreu  14614  recval  14684  abs1m  14697  abslem2  14701  fzomaxdiflem  14704  sqreulem  14721  sqreu  14722  limsupgre  14840  rlimdiv  15004  fsumparts  15163  climcnds  15208  expcnv  15221  ntrivcvg  15255  mod2eq1n2dvds  15698  ndvdssub  15762  sadcaddlem  15808  rplpwr  15909  dvdssqlem  15912  algcvgblem  15923  eucalgcvga  15932  isprm2lem  16027  powm2modprm  16142  coprimeprodsq  16147  pythagtriplem11  16164  pythagtriplem13  16166  pcadd2  16228  4sqlem11  16293  vdwlem6  16324  vdwlem8  16326  vdwlem10  16328  ramval  16346  ramcl2  16354  ramlb  16357  ram0  16360  mreintcl  16868  mrcval  16883  mrccl  16884  mrcuni  16894  mrcun  16895  acsfiel  16927  rescabs  17105  funcres  17168  setcmon  17349  setcepi  17350  fullestrcsetc  17403  funcsetcestrclem8  17414  fullsetcestrc  17418  yonffthlem  17534  pleval2i  17576  pospo  17585  poslubdg  17761  acsdrsel  17779  acsdrscl  17782  acsficl  17783  psss  17826  grpidd  17883  ismndd  17935  gsumsgrpccat  18006  gsumccatOLD  18007  gsumwmhm  18012  mulgaddcom  18253  subgmulg  18295  resghm  18376  conjnsg  18396  f1otrspeq  18577  pmtrval  18581  pmtrrn  18587  pmtrfinv  18591  pmtrprfval  18617  psgnunilem1  18623  psgnunilem5  18624  psgnunilem4  18627  psgneldm2i  18635  lsmelvalix  18768  pj1ghm  18831  efgredlemc  18873  frgp0  18888  qusabl  18987  cycsubgcyg  19023  gsumval3  19029  gsumcllem  19030  ablfac1c  19195  pgpfac1lem5  19203  isringd  19337  lspsneq0b  19787  lmodindp1  19788  lmhmf1o  19820  lmhmpreima  19822  reslmhm  19826  pwssplit3  19835  lspsncmp  19890  lspsneq  19896  mpfind  20322  mhplss  20344  znf1o  20700  dsmmlss  20890  frlmlbs  20943  frlmup1  20944  mat1  21058  chfacfisf  21464  chfacfisfcpmat  21465  uniopn  21507  ntrval  21646  clsval  21647  neival  21712  neiptopreu  21743  lpval  21749  restdis  21788  lmbrf  21870  cnpnei  21874  1stcrest  22063  hauspwdom  22111  lfinpfin  22134  txcnpi  22218  ptrescn  22249  xkococnlem  22269  qtopeu  22326  kqreglem1  22351  ptuncnv  22417  filss  22463  fsubbas  22477  fbasrn  22494  cfinfil  22503  ufinffr  22539  elfm3  22560  rnelfmlem  22562  rnelfm  22563  flimclslem  22594  flfval  22600  isfcf  22644  cnextfvval  22675  cnextf  22676  cnextcn  22677  ustelimasn  22833  trust  22840  restutop  22848  ustuqtop2  22853  utop2nei  22861  ucncn  22896  trcfilu  22905  cnextucn  22914  met1stc  23133  metustexhalf  23168  cfilucfil  23171  psmetutop  23179  nmoix  23340  nmoeq0  23347  idnghm  23354  blcvx  23408  xrsxmet  23419  iccntr  23431  icccmp  23435  iihalf1  23537  iihalf2  23539  xrhmeo  23552  cnheibor  23561  ipcau2  23839  lmmbrf  23867  iscauf  23885  cmetcaulem  23893  bcthlem4  23932  cmetcusp  23959  rrxcph  23997  minveclem4  24037  evthicc2  24063  cniccbdd  24064  ovollb2  24092  ovolunlem1a  24099  ovolunlem1  24100  voliun  24157  icombl  24167  ioombl  24168  iccvolcl  24170  ioovolcl  24173  mbfss  24249  mbfposb  24256  itg2const2  24344  itg2splitlem  24351  itg2gt0  24363  iblss2  24408  itgioo  24418  dvaddf  24541  dvmulf  24542  dvcobr  24545  dvcof  24547  rolle  24589  dvlip  24592  c1lip1  24596  dvivthlem1  24607  lhop1lem  24612  dvfsumlem1  24625  ftc1lem4  24638  ftc1lem5  24639  ply1divmo  24731  coe1termlem  24850  plydiveu  24889  taylplem1  24953  pserulm  25012  abelth  25031  abscxp2  25278  abscxpbnd  25336  logbgt0b  25373  ang180lem2  25390  ang180lem3  25391  isosctrlem1  25398  angpieqvd  25411  atandmtan  25500  birthdaylem3  25533  wilthlem2  25648  wilthimp  25651  isppw  25693  isppw2  25694  dvdsflsumcom  25767  chteq0  25787  perfectlem2  25808  dchrval  25812  dchrinvcl  25831  dchrptlem1  25842  bposlem3  25864  lgslem4  25878  lgsmod  25901  lgsdilem  25902  lgsdir2lem2  25904  lgsdir2  25908  lgsne0  25913  lgsmulsqcoprm  25921  lgseisenlem1  25953  2lgsoddprm  25994  2sqlem4  25999  chpo1ubb  26059  dchrisumn0  26099  pntrsumbnd2  26145  ostthlem1  26205  ostth3  26216  idmot  26325  tgelrnln  26418  lmimid  26582  lmiisolem  26584  hypcgrlem1  26587  brcgr  26688  colinearalglem4  26697  colinearalg  26698  axlowdimlem14  26743  axcontlem4  26755  cplgrop  27221  lfgriswlk  27472  pthdlem1  27549  crctcshwlkn0  27601  elwspths2on  27741  clwlkclwwlklem2fv2  27776  frgrncvvdeqlem9  28088  nvss  28372  sspn  28515  nmoub3i  28552  nmblolbii  28578  blocnilem  28583  minvecolem4  28659  htthlem  28696  norm1  29028  norm1exi  29029  pjeq  29178  axpjpj  29199  normcan  29355  pjoi0  29496  nmopub2tALT  29688  nmfnleub2  29705  eighmorth  29743  nmbdoplbi  29803  nmcoplbi  29807  nmophmi  29810  nmbdfnlbi  29828  nmcfnlbi  29831  riesz3i  29841  cnlnadjlem7  29852  branmfn  29884  nmopleid  29918  hstle  30009  superpos  30133  cvexchlem  30147  foresf1o  30267  elabreximd  30272  unidifsnne  30298  f1o3d  30374  fmptco1f1o  30380  funcnvmpt  30414  fgreu  30419  suppovss  30428  resf1o  30468  fpwrelmap  30471  xrofsup  30494  eliccelico  30502  elicoelioo  30503  iocinif  30506  difioo  30507  eliccioo  30609  cshf1o  30638  gsummpt2co  30688  submomnd  30713  symgcom  30729  symgcom2  30730  odpmco  30732  pmtrcnel  30735  pmtridf1o  30738  cycpmco2lem6  30775  cycpmco2lem7  30776  cycpmco2  30777  cyc3co2  30784  cycpmconjv  30786  tocyccntz  30788  cyc3evpm  30794  cycpmconjslem2  30799  cycpmconjs  30800  archirngz  30820  ornglmullt  30882  orngrmullt  30883  lindssn  30941  linds2eq  30943  prmidl2  30960  qsidomlem1  30967  ssmxidl  30981  lbslsat  31016  lindsunlem  31022  lindsun  31023  dimkerim  31025  fedgmullem1  31027  fedgmullem2  31028  fedgmul  31029  madjusmdetlem2  31095  qtophaus  31102  locfinreflem  31106  unitdivcld  31146  tpr2rico  31157  ordtrestNEW  31166  lmxrge0  31197  elzrhunit  31222  qqhf  31229  indf1ofs  31287  gsumesum  31320  esumfsup  31331  esumcvg  31347  issgon  31384  sigainb  31397  insiga  31398  isrnmeas  31461  measvunilem  31473  volmeas  31492  ddeval1  31495  ddeval0  31496  imambfm  31522  omssubadd  31560  carsgclctunlem3  31580  eulerpartlemf  31630  eulerpartlemgvv  31636  probun  31679  dstfrvunirn  31734  plymulx  31820  signslema  31834  signstfvn  31841  signsvtn0  31842  signstfvneq0  31844  signstres  31847  signstfveq0a  31848  breprexplemc  31905  logdivsqrle  31923  hgt750lemg  31927  tgoldbachgtda  31934  tgoldbachgt  31936  lpadmax  31955  lpadleft  31956  lpadright  31957  bnj529  32014  bnj548  32171  bnj570  32179  bnj852  32195  bnj929  32210  bnj1097  32255  bnj1118  32258  bnj1145  32267  funen1cnv  32359  spthcycl  32378  acycgr0v  32397  derangen  32421  subfacp1lem2b  32430  subfacp1lem4  32432  subfacp1lem5  32433  derangfmla  32439  ptpconn  32482  mppspstlem  32820  wsuclem  33114  frr3g  33123  frrlem3  33127  fpr2  33142  nosupbnd2lem1  33217  nocvxmin  33250  colinearex  33523  btwnconn1lem11  33560  btwnconn1lem12  33561  fwddifnp1  33628  nn0prpwlem  33672  bj-snmoore  34407  relowlpssretop  34647  fin2so  34881  matunitlindflem2  34891  ptrecube  34894  poimirlem8  34902  poimirlem13  34907  poimirlem15  34909  poimirlem24  34918  poimirlem25  34919  poimirlem26  34920  heicant  34929  mblfinlem2  34932  voliunnfl  34938  mbfresfi  34940  itg2addnclem  34945  itg2addnclem3  34947  itg2gt0cn  34949  ftc1cnnclem  34967  ftc1anclem5  34973  cover2  34991  indexdom  35011  sdclem1  35020  fdc  35022  equivbnd2  35072  heiborlem8  35098  heibor  35101  isdrngo2  35238  iscringd  35278  smprngopr  35332  prnc  35347  eqeltr  35503  islfld  36200  lkrshpor  36245  lfl1dim  36259  lfl1dim2N  36260  cmtcomlemN  36386  2lplnmN  36697  pmapjat1  36991  trlnid  37317  tendoex  38113  dia1dimid  38201  dibval2  38282  dihmeetlem2N  38437  dochlkr  38523  mapdcv  38798  hdmaplkr  39051  hdmapip0  39053  hlhillcs  39096  frlmvscadiccat  39152  nacsfix  39316  3rexfrabdioph  39401  4rexfrabdioph  39402  6rexfrabdioph  39403  7rexfrabdioph  39404  eldioph4b  39415  pellexlem2  39434  pellexlem5  39437  jm2.26lem3  39605  numinfctb  39710  ntrclsfv1  40412  ntrneifv1  40436  ntrneifv2  40437  cvgdvgrat  40652  radcnvrat  40653  dvconstbi  40673  bccbc  40684  elpwgded  40905  elpwgdedVD  41258  sspwimpcf  41261  sspwimpcfVD  41262  sspwimpALT2  41269  ax6e2ndeqALT  41272  eliuniin  41372  eliuniin2  41393  qinioo  41818  dfxlim2v  42135  xlimliminflimsup  42150  cncfiooicclem1  42183  ibliooicc  42263  stoweidlem27  42319  stoweidlem28  42320  fourierdlem89  42487  fourierdlem91  42489  fourierdlem92  42490  smflimmpt  43091  odz2prm2pw  43732  perfectALTVlem2  43894  blen1b  44655  itscnhlc0yqe  44753  itsclquadb  44770  onetansqsecsq  44867  cotsqcscsq  44868  aacllem  44909