Theorem biimpar 478

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

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

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 397

This theorem is referenced by:  bitr  803  exbiri  809  biadanid  821  oplem1  1055  eqtr  2755  pm13.181  3023  opabss  5211  axprlem4  5423  axprlem5  5424  euotd  5512  brcogw  5866  somin1  6131  xpdifid  6164  funfni  6652  fncoOLD  6665  fnssres  6670  fn0  6678  fnimadisj  6679  fnimaeq0  6680  foimacnv  6847  fvelimab  6961  dffv2  6983  fvopab3ig  6991  dff3  7098  dffo4  7101  fpr2g  7209  f1eqcocnv  7295  f1eqcocnvOLD  7296  isomin  7330  f1ocnv2d  7655  fnexALT  7933  xp1st  8003  xp2nd  8004  frrlem3  8269  fpr2  8285  wfr3g  8303  wfrlem3OLD  8306  wfrlem4OLD  8308  wfr2  8332  iinon  8336  tfr3  8395  oawordri  8546  oaass  8557  omeulem1  8578  oeoa  8593  oeoe  8595  oeeulem  8597  ecelqsg  8762  elqsn0  8776  pwdom  9125  enfii  9185  phpeqd  9211  ominf  9254  findcard3  9281  marypha1lem  9424  wofib  9536  cantnff  9665  cantnfp1  9672  cantnf  9684  cnfcomlem  9690  ttrcltr  9707  frr3g  9747  r1sscl  9776  rankval3b  9817  infxpidm2  10008  numdom  10029  onssnum  10031  acni  10036  acni2  10037  dfac5  10119  djulepw  10183  infunsdom1  10204  infunsdom  10205  cofsmo  10260  cfsmolem  10261  fin1ai  10284  fin2i  10286  isf34lem1  10363  fin67  10386  itunisuc  10410  axdc3lem4  10444  zornn0g  10496  ttukeylem6  10505  brdom3  10519  tsken  10745  tskcard  10772  r1tskina  10773  intgru  10805  prlem934  11024  ltexprlem7  11033  supaddc  12177  mul2lt0rlt0  13072  xrmaxeq  13154  xrmineq  13155  xmulneg1  13244  ixxun  13336  difelfzle  13610  ssfzoulel  13722  elfznelfzo  13733  ico01fl0  13780  btwnzge0  13789  ltdifltdiv  13795  ioopnfsup  13825  icopnfsup  13826  modifeq2int  13894  suppssfz  13955  expmordi  14128  zzlesq  14166  faclbnd4lem4  14252  hasheni  14304  hashgt0  14344  hashge1  14345  hashprb  14353  lennncl  14480  wrdsymb0  14495  ccatsymb  14528  ccatlid  14532  ccatass  14534  ccatswrd  14614  swrdccat2  14615  ccatpfx  14647  swrdccatfn  14670  swrdccat  14681  revccat  14712  2cshw  14759  cnpart  15183  resqreu  15195  recval  15265  abs1m  15278  abslem2  15282  fzomaxdiflem  15285  sqreulem  15302  sqreu  15303  limsupgre  15421  rlimdiv  15588  fsumparts  15748  climcnds  15793  expcnv  15806  ntrivcvg  15839  mod2eq1n2dvds  16286  ndvdssub  16348  sadcaddlem  16394  rplpwr  16495  dvdssqlem  16499  algcvgblem  16510  eucalgcvga  16519  isprm2lem  16614  powm2modprm  16732  coprimeprodsq  16737  pythagtriplem11  16754  pythagtriplem13  16756  pcadd2  16819  4sqlem11  16884  vdwlem6  16915  vdwlem8  16917  vdwlem10  16919  ramval  16937  ramcl2  16945  ramlb  16948  ram0  16951  mreintcl  17535  mrcval  17550  mrccl  17551  mrcuni  17561  mrcun  17562  acsfiel  17594  rescabs  17778  rescabsOLD  17779  funcres  17842  setcmon  18033  setcepi  18034  fullestrcsetc  18099  funcsetcestrclem8  18110  fullsetcestrc  18114  yonffthlem  18231  pleval2i  18285  pospo  18294  poslubdg  18363  acsdrsel  18492  acsdrscl  18495  acsficl  18496  psss  18529  grpidd  18586  ismndd  18643  gsumsgrpccat  18717  gsumwmhm  18722  mulgaddcom  18972  subgmulg  19014  resghm  19102  conjnsg  19122  f1otrspeq  19309  pmtrval  19313  pmtrrn  19319  pmtrfinv  19323  pmtrprfval  19349  psgnunilem1  19355  psgnunilem5  19356  psgnunilem4  19359  psgneldm2i  19367  lsmelvalix  19503  pj1ghm  19565  efgredlemc  19607  frgp0  19622  qusabl  19727  cycsubgcyg  19763  gsumval3  19769  gsumcllem  19770  ablfac1c  19935  pgpfac1lem5  19943  isringd  20098  01eq0ring  20297  lspsneq0b  20616  lmodindp1  20617  lmhmf1o  20649  lmhmpreima  20651  reslmhm  20655  pwssplit3  20664  lspsncmp  20721  lspsneq  20727  znf1o  21098  dsmmlss  21290  frlmlbs  21343  frlmup1  21344  psrgrp  21508  mpfind  21661  mhplss  21689  mat1  21940  chfacfisf  22347  chfacfisfcpmat  22348  uniopn  22390  ntrval  22531  clsval  22532  neival  22597  neiptopreu  22628  lpval  22634  restdis  22673  lmbrf  22755  cnpnei  22759  1stcrest  22948  hauspwdom  22996  lfinpfin  23019  txcnpi  23103  ptrescn  23134  xkococnlem  23154  qtopeu  23211  kqreglem1  23236  ptuncnv  23302  filss  23348  fsubbas  23362  fbasrn  23379  cfinfil  23388  ufinffr  23424  elfm3  23445  rnelfmlem  23447  rnelfm  23448  flimclslem  23479  flfval  23485  isfcf  23529  cnextfvval  23560  cnextf  23561  cnextcn  23562  ustelimasn  23718  trust  23725  restutop  23733  ustuqtop2  23738  utop2nei  23746  ucncn  23781  trcfilu  23790  cnextucn  23799  met1stc  24021  metustexhalf  24056  cfilucfil  24059  psmetutop  24067  nmoix  24237  nmoeq0  24244  idnghm  24251  blcvx  24305  xrsxmet  24316  iccntr  24328  icccmp  24332  iihalf1  24438  iihalf2  24440  xrhmeo  24453  cnheibor  24462  ipcau2  24742  lmmbrf  24770  iscauf  24788  cmetcaulem  24796  bcthlem4  24835  cmetcusp  24862  rrxcph  24900  minveclem4  24940  evthicc2  24968  cniccbdd  24969  ovollb2  24997  ovolunlem1a  25004  ovolunlem1  25005  voliun  25062  icombl  25072  ioombl  25073  iccvolcl  25075  ioovolcl  25078  mbfss  25154  mbfposb  25161  itg2const2  25250  itg2splitlem  25257  itg2gt0  25269  iblss2  25314  itgioo  25324  dvaddf  25450  dvmulf  25451  dvcobr  25454  dvcof  25456  rolle  25498  dvlip  25501  c1lip1  25505  dvivthlem1  25516  lhop1lem  25521  dvfsumlem1  25534  ftc1lem4  25547  ftc1lem5  25548  ply1divmo  25644  coe1termlem  25763  plydiveu  25802  taylplem1  25866  pserulm  25925  abelth  25944  abscxp2  26192  abscxpbnd  26250  logbgt0b  26287  ang180lem2  26304  ang180lem3  26305  isosctrlem1  26312  angpieqvd  26325  atandmtan  26414  birthdaylem3  26447  wilthlem2  26562  wilthimp  26565  isppw  26607  isppw2  26608  dvdsflsumcom  26681  chteq0  26701  perfectlem2  26722  dchrval  26726  dchrinvcl  26745  dchrptlem1  26756  bposlem3  26778  lgslem4  26792  lgsmod  26815  lgsdilem  26816  lgsdir2lem2  26818  lgsdir2  26822  lgsne0  26827  lgsmulsqcoprm  26835  lgseisenlem1  26867  2lgsoddprm  26908  2sqlem4  26913  chpo1ubb  26973  dchrisumn0  27013  pntrsumbnd2  27059  ostthlem1  27119  ostth3  27130  nosupbnd2lem1  27207  noinfbnd2lem1  27222  nocvxmin  27269  eqscut2  27296  sltlpss  27390  idmot  27777  tgelrnln  27870  lmimid  28034  lmiisolem  28036  hypcgrlem1  28039  brcgr  28147  colinearalglem4  28156  colinearalg  28157  axlowdimlem14  28202  axcontlem4  28214  cplgrop  28683  lfgriswlk  28934  pthdlem1  29012  crctcshwlkn0  29064  elwspths2on  29203  clwlkclwwlklem2fv2  29238  frgrncvvdeqlem9  29549  nvss  29833  sspn  29976  nmoub3i  30013  nmblolbii  30039  blocnilem  30044  minvecolem4  30120  htthlem  30157  norm1  30489  norm1exi  30490  pjeq  30639  axpjpj  30660  normcan  30816  pjoi0  30957  nmopub2tALT  31149  nmfnleub2  31166  eighmorth  31204  nmbdoplbi  31264  nmcoplbi  31268  nmophmi  31271  nmbdfnlbi  31289  nmcfnlbi  31292  riesz3i  31302  cnlnadjlem7  31313  branmfn  31345  nmopleid  31379  hstle  31470  superpos  31594  cvexchlem  31608  foresf1o  31729  elabreximd  31734  unidifsnne  31760  f1o3d  31838  fmptco1f1o  31844  funcnvmpt  31879  fgreu  31884  suppovss  31893  fsupprnfi  31901  resf1o  31942  fpwrelmap  31945  xrofsup  31967  eliccelico  31975  elicoelioo  31976  iocinif  31979  difioo  31980  eliccioo  32084  cshf1o  32113  mgcmnt1d  32154  mgcmnt2d  32155  pwrssmgc  32157  gsummpt2co  32187  gsumhashmul  32195  submomnd  32215  symgcom  32231  symgcom2  32232  odpmco  32234  pmtrcnel  32237  pmtridf1o  32240  cycpmco2lem6  32277  cycpmco2lem7  32278  cycpmco2  32279  cyc3co2  32286  cycpmconjv  32288  tocyccntz  32290  cyc3evpm  32296  cycpmconjslem2  32301  cycpmconjs  32302  archirngz  32322  isdrng4  32383  sdrgdvcl  32385  sdrginvcl  32386  ornglmullt  32413  orngrmullt  32414  dvdsrspss  32479  lindssn  32482  linds2eq  32485  nsgqusf1olem1  32512  nsgqusf1olem3  32514  ghmqusker  32520  unitpidl1  32530  elrspunidl  32534  rhmimaidl  32538  drngidlhash  32540  prmidl2  32547  prmidl0  32557  qsidomlem1  32559  mxidlirredi  32575  mxidlirred  32576  ssmxidl  32578  drng0mxidl  32580  opprmxidlabs  32589  qsdrngilem  32596  qsdrngi  32597  qsdrng  32599  ply1scleq  32627  ply1asclunit  32642  ply1degltlss  32655  ply1gsumz  32657  lbslsat  32689  ply1degltdimlem  32695  lindsunlem  32697  lindsun  32698  dimkerim  32700  fedgmullem1  32702  fedgmullem2  32703  fedgmul  32704  irngss  32739  0ringirng  32741  irngnzply1  32743  irngnminplynz  32759  algextdeglem1  32760  madjusmdetlem2  32796  qtophaus  32804  locfinreflem  32808  zarclssn  32841  zarmxt1  32848  zarcmplem  32849  rhmpreimacn  32853  unitdivcld  32869  tpr2rico  32880  ordtrestNEW  32889  lmxrge0  32920  elzrhunit  32947  qqhf  32954  indf1ofs  33012  gsumesum  33045  esumfsup  33056  esumcvg  33072  issgon  33109  sigainb  33122  insiga  33123  isrnmeas  33186  measvunilem  33198  volmeas  33217  ddeval1  33220  ddeval0  33221  imambfm  33249  omssubadd  33287  carsgclctunlem3  33307  eulerpartlemf  33357  eulerpartlemgvv  33363  probun  33406  dstfrvunirn  33461  plymulx  33547  signslema  33561  signstfvn  33568  signsvtn0  33569  signstfvneq0  33571  signstres  33574  signstfveq0a  33575  breprexplemc  33632  logdivsqrle  33650  hgt750lemg  33654  tgoldbachgtda  33661  tgoldbachgt  33663  lpadmax  33682  lpadleft  33683  lpadright  33684  bnj529  33740  bnj548  33896  bnj570  33904  bnj852  33920  bnj929  33935  bnj1097  33980  bnj1118  33983  bnj1145  33992  funen1cnv  34079  spthcycl  34108  acycgr0v  34127  derangen  34151  subfacp1lem2b  34160  subfacp1lem4  34162  subfacp1lem5  34163  derangfmla  34169  ptpconn  34212  mppspstlem  34550  wsuclem  34785  colinearex  35020  btwnconn1lem11  35057  btwnconn1lem12  35058  fwddifnp1  35125  gg-dvcobr  35164  nn0prpwlem  35195  bj-snmoore  35982  bj-imdiridlem  36054  relowlpssretop  36233  fin2so  36463  matunitlindflem2  36473  ptrecube  36476  poimirlem8  36484  poimirlem13  36489  poimirlem15  36491  poimirlem24  36500  poimirlem25  36501  poimirlem26  36502  heicant  36511  mblfinlem2  36514  voliunnfl  36520  mbfresfi  36522  itg2addnclem  36527  itg2addnclem3  36529  itg2gt0cn  36531  ftc1cnnclem  36547  ftc1anclem5  36553  cover2  36571  indexdom  36590  sdclem1  36599  fdc  36601  equivbnd2  36648  heiborlem8  36674  heibor  36677  isdrngo2  36814  iscringd  36854  smprngopr  36908  prnc  36923  eqbrtr  37086  eqeltr  37088  islfld  37920  lkrshpor  37965  lfl1dim  37979  lfl1dim2N  37980  cmtcomlemN  38106  2lplnmN  38418  pmapjat1  38712  trlnid  39038  tendoex  39834  dia1dimid  39922  dibval2  40003  dihmeetlem2N  40158  dochlkr  40244  mapdcv  40519  hdmaplkr  40772  hdmapip0  40774  hlhillcs  40821  frlmvscadiccat  41077  dvdsexpnn  41226  nacsfix  41435  3rexfrabdioph  41520  4rexfrabdioph  41521  6rexfrabdioph  41522  7rexfrabdioph  41523  eldioph4b  41534  pellexlem2  41553  pellexlem5  41556  jm2.26lem3  41725  numinfctb  41830  ordne0gt0  41996  omge1  42032  omlim2  42034  omord2lim  42035  omord2i  42036  tfsconcatfv  42076  tfsconcatb0  42079  oaun3lem1  42109  ntrclsfv1  42791  ntrneifv1  42815  ntrneifv2  42816  cvgdvgrat  43057  radcnvrat  43058  dvconstbi  43078  bccbc  43089  elpwgded  43310  elpwgdedVD  43663  sspwimpcf  43666  sspwimpcfVD  43667  sspwimpALT2  43674  ax6e2ndeqALT  43677  eliuniin  43773  eliuniin2  43794  qinioo  44234  dfxlim2v  44549  xlimliminflimsup  44564  cncfiooicclem1  44595  ibliooicc  44673  stoweidlem27  44729  stoweidlem28  44730  fourierdlem89  44897  fourierdlem91  44899  fourierdlem92  44900  smflimmpt  45512  odz2prm2pw  46217  perfectALTVlem2  46376  isrngd  46658  blen1b  47227  naryfvalelfv  47271  itscnhlc0yqe  47398  itsclquadb  47415  lubeldm2  47542  glbeldm2  47543  ipolub  47566  ipoglb  47569  functhinclem1  47614  thincciso  47622  prsthinc  47627  prstchom2ALT  47652  onetansqsecsq  47759  cotsqcscsq  47760  aacllem  47801