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  802  exbiri  808  biadanid  820  oplem1  1054  eqtr  2759  pm13.181  3023  opabss  5153  axprlem4  5366  axprlem5  5367  euotd  5451  brcogw  5804  somin1  6067  xpdifid  6100  funfni  6585  fncoOLD  6596  fnssres  6601  fn0  6609  fnimadisj  6610  fnimaeq0  6611  foimacnv  6778  fvelimab  6891  dffv2  6913  fvopab3ig  6921  dff3  7026  dffo4  7029  fpr2g  7137  f1eqcocnv  7223  f1eqcocnvOLD  7224  isomin  7258  f1ocnv2d  7576  fnexALT  7853  xp1st  7923  xp2nd  7924  frrlem3  8166  fpr2  8182  wfr3g  8200  wfrlem3OLD  8203  wfrlem4OLD  8205  wfr2  8229  iinon  8233  tfr3  8292  oawordri  8444  oaass  8455  omeulem1  8476  oeoa  8491  oeoe  8493  oeeulem  8495  ecelqsg  8624  elqsn0  8638  pwdom  8986  enfii  9046  phpeqd  9072  ominf  9115  findcard3  9142  marypha1lem  9282  wofib  9394  cantnff  9523  cantnfp1  9530  cantnf  9542  cnfcomlem  9548  ttrcltr  9565  frr3g  9605  r1sscl  9634  rankval3b  9675  infxpidm2  9866  numdom  9887  onssnum  9889  acni  9894  acni2  9895  dfac5  9977  djulepw  10041  infunsdom1  10062  infunsdom  10063  cofsmo  10118  cfsmolem  10119  fin1ai  10142  fin2i  10144  isf34lem1  10221  fin67  10244  itunisuc  10268  axdc3lem4  10302  zornn0g  10354  ttukeylem6  10363  brdom3  10377  tsken  10603  tskcard  10630  r1tskina  10631  intgru  10663  prlem934  10882  ltexprlem7  10891  supaddc  12035  mul2lt0rlt0  12925  xrmaxeq  13006  xrmineq  13007  xmulneg1  13096  ixxun  13188  difelfzle  13462  ssfzoulel  13574  elfznelfzo  13585  ico01fl0  13632  btwnzge0  13641  ltdifltdiv  13647  ioopnfsup  13677  icopnfsup  13678  modifeq2int  13746  suppssfz  13807  expmordi  13978  faclbnd4lem4  14103  hasheni  14155  hashgt0  14195  hashge1  14196  hashprb  14204  lennncl  14329  wrdsymb0  14344  ccatsymb  14378  ccatlid  14382  ccatass  14384  ccatswrd  14471  swrdccat2  14472  ccatpfx  14504  swrdccatfn  14527  swrdccat  14538  revccat  14569  2cshw  14616  cnpart  15042  resqreu  15055  recval  15125  abs1m  15138  abslem2  15142  fzomaxdiflem  15145  sqreulem  15162  sqreu  15163  limsupgre  15281  rlimdiv  15448  fsumparts  15609  climcnds  15654  expcnv  15667  ntrivcvg  15700  mod2eq1n2dvds  16147  ndvdssub  16209  sadcaddlem  16255  rplpwr  16356  dvdssqlem  16360  algcvgblem  16371  eucalgcvga  16380  isprm2lem  16475  powm2modprm  16593  coprimeprodsq  16598  pythagtriplem11  16615  pythagtriplem13  16617  pcadd2  16680  4sqlem11  16745  vdwlem6  16776  vdwlem8  16778  vdwlem10  16780  ramval  16798  ramcl2  16806  ramlb  16809  ram0  16812  mreintcl  17393  mrcval  17408  mrccl  17409  mrcuni  17419  mrcun  17420  acsfiel  17452  rescabs  17636  rescabsOLD  17637  funcres  17700  setcmon  17891  setcepi  17892  fullestrcsetc  17957  funcsetcestrclem8  17968  fullsetcestrc  17972  yonffthlem  18089  pleval2i  18143  pospo  18152  poslubdg  18221  acsdrsel  18350  acsdrscl  18353  acsficl  18354  psss  18387  grpidd  18444  ismndd  18496  gsumsgrpccat  18567  gsumwmhm  18572  mulgaddcom  18815  subgmulg  18857  resghm  18938  conjnsg  18958  f1otrspeq  19143  pmtrval  19147  pmtrrn  19153  pmtrfinv  19157  pmtrprfval  19183  psgnunilem1  19189  psgnunilem5  19190  psgnunilem4  19193  psgneldm2i  19201  lsmelvalix  19334  pj1ghm  19396  efgredlemc  19438  frgp0  19453  qusabl  19553  cycsubgcyg  19589  gsumval3  19595  gsumcllem  19596  ablfac1c  19761  pgpfac1lem5  19769  isringd  19911  lspsneq0b  20373  lmodindp1  20374  lmhmf1o  20406  lmhmpreima  20408  reslmhm  20412  pwssplit3  20421  lspsncmp  20476  lspsneq  20482  znf1o  20857  dsmmlss  21049  frlmlbs  21102  frlmup1  21103  mpfind  21415  mhplss  21443  mat1  21694  chfacfisf  22101  chfacfisfcpmat  22102  uniopn  22144  ntrval  22285  clsval  22286  neival  22351  neiptopreu  22382  lpval  22388  restdis  22427  lmbrf  22509  cnpnei  22513  1stcrest  22702  hauspwdom  22750  lfinpfin  22773  txcnpi  22857  ptrescn  22888  xkococnlem  22908  qtopeu  22965  kqreglem1  22990  ptuncnv  23056  filss  23102  fsubbas  23116  fbasrn  23133  cfinfil  23142  ufinffr  23178  elfm3  23199  rnelfmlem  23201  rnelfm  23202  flimclslem  23233  flfval  23239  isfcf  23283  cnextfvval  23314  cnextf  23315  cnextcn  23316  ustelimasn  23472  trust  23479  restutop  23487  ustuqtop2  23492  utop2nei  23500  ucncn  23535  trcfilu  23544  cnextucn  23553  met1stc  23775  metustexhalf  23810  cfilucfil  23813  psmetutop  23821  nmoix  23991  nmoeq0  23998  idnghm  24005  blcvx  24059  xrsxmet  24070  iccntr  24082  icccmp  24086  iihalf1  24192  iihalf2  24194  xrhmeo  24207  cnheibor  24216  ipcau2  24496  lmmbrf  24524  iscauf  24542  cmetcaulem  24550  bcthlem4  24589  cmetcusp  24616  rrxcph  24654  minveclem4  24694  evthicc2  24722  cniccbdd  24723  ovollb2  24751  ovolunlem1a  24758  ovolunlem1  24759  voliun  24816  icombl  24826  ioombl  24827  iccvolcl  24829  ioovolcl  24832  mbfss  24908  mbfposb  24915  itg2const2  25004  itg2splitlem  25011  itg2gt0  25023  iblss2  25068  itgioo  25078  dvaddf  25204  dvmulf  25205  dvcobr  25208  dvcof  25210  rolle  25252  dvlip  25255  c1lip1  25259  dvivthlem1  25270  lhop1lem  25275  dvfsumlem1  25288  ftc1lem4  25301  ftc1lem5  25302  ply1divmo  25398  coe1termlem  25517  plydiveu  25556  taylplem1  25620  pserulm  25679  abelth  25698  abscxp2  25946  abscxpbnd  26004  logbgt0b  26041  ang180lem2  26058  ang180lem3  26059  isosctrlem1  26066  angpieqvd  26079  atandmtan  26168  birthdaylem3  26201  wilthlem2  26316  wilthimp  26319  isppw  26361  isppw2  26362  dvdsflsumcom  26435  chteq0  26455  perfectlem2  26476  dchrval  26480  dchrinvcl  26499  dchrptlem1  26510  bposlem3  26532  lgslem4  26546  lgsmod  26569  lgsdilem  26570  lgsdir2lem2  26572  lgsdir2  26576  lgsne0  26581  lgsmulsqcoprm  26589  lgseisenlem1  26621  2lgsoddprm  26662  2sqlem4  26667  chpo1ubb  26727  dchrisumn0  26767  pntrsumbnd2  26813  ostthlem1  26873  ostth3  26884  nosupbnd2lem1  26961  noinfbnd2lem1  26976  idmot  27100  tgelrnln  27193  lmimid  27357  lmiisolem  27359  hypcgrlem1  27362  brcgr  27470  colinearalglem4  27479  colinearalg  27480  axlowdimlem14  27525  axcontlem4  27537  cplgrop  28006  lfgriswlk  28257  pthdlem1  28335  crctcshwlkn0  28387  elwspths2on  28526  clwlkclwwlklem2fv2  28561  frgrncvvdeqlem9  28872  nvss  29156  sspn  29299  nmoub3i  29336  nmblolbii  29362  blocnilem  29367  minvecolem4  29443  htthlem  29480  norm1  29812  norm1exi  29813  pjeq  29962  axpjpj  29983  normcan  30139  pjoi0  30280  nmopub2tALT  30472  nmfnleub2  30489  eighmorth  30527  nmbdoplbi  30587  nmcoplbi  30591  nmophmi  30594  nmbdfnlbi  30612  nmcfnlbi  30615  riesz3i  30625  cnlnadjlem7  30636  branmfn  30668  nmopleid  30702  hstle  30793  superpos  30917  cvexchlem  30931  foresf1o  31051  elabreximd  31056  unidifsnne  31084  f1o3d  31162  fmptco1f1o  31168  funcnvmpt  31204  fgreu  31209  suppovss  31217  fsupprnfi  31226  resf1o  31265  fpwrelmap  31268  xrofsup  31290  eliccelico  31298  elicoelioo  31299  iocinif  31302  difioo  31303  eliccioo  31405  cshf1o  31434  mgcmnt1d  31475  mgcmnt2d  31476  pwrssmgc  31478  gsummpt2co  31508  gsumhashmul  31516  submomnd  31536  symgcom  31552  symgcom2  31553  odpmco  31555  pmtrcnel  31558  pmtridf1o  31561  cycpmco2lem6  31598  cycpmco2lem7  31599  cycpmco2  31600  cyc3co2  31607  cycpmconjv  31609  tocyccntz  31611  cyc3evpm  31617  cycpmconjslem2  31622  cycpmconjs  31623  archirngz  31643  sdrgdvcl  31693  sdrginvcl  31694  ornglmullt  31719  orngrmullt  31720  lindssn  31783  linds2eq  31785  nsgqusf1olem1  31808  nsgqusf1olem3  31810  elrspunidl  31816  rhmimaidl  31819  prmidl2  31826  prmidl0  31836  qsidomlem1  31838  ssmxidl  31852  ply1scleq  31878  lbslsat  31910  lindsunlem  31916  lindsun  31917  dimkerim  31919  fedgmullem1  31921  fedgmullem2  31922  fedgmul  31923  madjusmdetlem2  31989  qtophaus  31997  locfinreflem  32001  zarclssn  32034  zarmxt1  32041  zarcmplem  32042  rhmpreimacn  32046  unitdivcld  32062  tpr2rico  32073  ordtrestNEW  32082  lmxrge0  32113  elzrhunit  32140  qqhf  32147  indf1ofs  32205  gsumesum  32238  esumfsup  32249  esumcvg  32265  issgon  32302  sigainb  32315  insiga  32316  isrnmeas  32379  measvunilem  32391  volmeas  32410  ddeval1  32413  ddeval0  32414  imambfm  32442  omssubadd  32480  carsgclctunlem3  32500  eulerpartlemf  32550  eulerpartlemgvv  32556  probun  32599  dstfrvunirn  32654  plymulx  32740  signslema  32754  signstfvn  32761  signsvtn0  32762  signstfvneq0  32764  signstres  32767  signstfveq0a  32768  breprexplemc  32825  logdivsqrle  32843  hgt750lemg  32847  tgoldbachgtda  32854  tgoldbachgt  32856  lpadmax  32875  lpadleft  32876  lpadright  32877  bnj529  32933  bnj548  33089  bnj570  33097  bnj852  33113  bnj929  33128  bnj1097  33173  bnj1118  33176  bnj1145  33185  funen1cnv  33272  spthcycl  33303  acycgr0v  33322  derangen  33346  subfacp1lem2b  33355  subfacp1lem4  33357  subfacp1lem5  33358  derangfmla  33364  ptpconn  33407  mppspstlem  33745  wsuclem  34014  nocvxmin  34064  eqscut2  34091  sltlpss  34178  colinearex  34453  btwnconn1lem11  34490  btwnconn1lem12  34491  fwddifnp1  34558  nn0prpwlem  34602  bj-snmoore  35382  bj-imdiridlem  35454  relowlpssretop  35633  fin2so  35862  matunitlindflem2  35872  ptrecube  35875  poimirlem8  35883  poimirlem13  35888  poimirlem15  35890  poimirlem24  35899  poimirlem25  35900  poimirlem26  35901  heicant  35910  mblfinlem2  35913  voliunnfl  35919  mbfresfi  35921  itg2addnclem  35926  itg2addnclem3  35928  itg2gt0cn  35930  ftc1cnnclem  35946  ftc1anclem5  35952  cover2  35970  indexdom  35990  sdclem1  35999  fdc  36001  equivbnd2  36048  heiborlem8  36074  heibor  36077  isdrngo2  36214  iscringd  36254  smprngopr  36308  prnc  36323  eqbrtr  36487  eqeltr  36489  islfld  37322  lkrshpor  37367  lfl1dim  37381  lfl1dim2N  37382  cmtcomlemN  37508  2lplnmN  37820  pmapjat1  38114  trlnid  38440  tendoex  39236  dia1dimid  39324  dibval2  39405  dihmeetlem2N  39560  dochlkr  39646  mapdcv  39921  hdmaplkr  40174  hdmapip0  40176  hlhillcs  40223  frlmvscadiccat  40484  mhphf  40535  dvdsexpnn  40590  nacsfix  40784  3rexfrabdioph  40869  4rexfrabdioph  40870  6rexfrabdioph  40871  7rexfrabdioph  40872  eldioph4b  40883  pellexlem2  40902  pellexlem5  40905  jm2.26lem3  41074  numinfctb  41179  ntrclsfv1  41975  ntrneifv1  41999  ntrneifv2  42000  cvgdvgrat  42241  radcnvrat  42242  dvconstbi  42262  bccbc  42273  elpwgded  42494  elpwgdedVD  42847  sspwimpcf  42850  sspwimpcfVD  42851  sspwimpALT2  42858  ax6e2ndeqALT  42861  eliuniin  42958  eliuniin2  42979  qinioo  43398  dfxlim2v  43713  xlimliminflimsup  43728  cncfiooicclem1  43759  ibliooicc  43837  stoweidlem27  43893  stoweidlem28  43894  fourierdlem89  44061  fourierdlem91  44063  fourierdlem92  44064  smflimmpt  44674  odz2prm2pw  45355  perfectALTVlem2  45514  blen1b  46274  naryfvalelfv  46318  itscnhlc0yqe  46445  itsclquadb  46462  lubeldm2  46590  glbeldm2  46591  ipolub  46614  ipoglb  46617  functhinclem1  46662  thincciso  46670  prsthinc  46675  prstchom2ALT  46700  onetansqsecsq  46803  cotsqcscsq  46804  aacllem  46845