Theorem biimpar 476

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

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

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 395

This theorem is referenced by:  bitr  801  exbiri  807  biadanid  819  oplem1  1053  eqtr  2753  pm13.181  3021  opabss  5211  axprlem4  5423  axprlem5  5424  euotd  5512  brcogw  5867  somin1  6133  xpdifid  6166  funfni  6654  fncoOLD  6667  fnssres  6672  fn0  6680  fnimadisj  6681  fnimaeq0  6682  foimacnv  6849  fvelimab  6963  dffv2  6985  fvopab3ig  6993  dff3  7100  dffo4  7103  fpr2g  7214  f1eqcocnv  7301  f1eqcocnvOLD  7302  isomin  7336  f1ocnv2d  7661  fnexALT  7939  xp1st  8009  xp2nd  8010  frrlem3  8275  fpr2  8291  wfr3g  8309  wfrlem3OLD  8312  wfrlem4OLD  8314  wfr2  8338  iinon  8342  tfr3  8401  oawordri  8552  oaass  8563  omeulem1  8584  oeoa  8599  oeoe  8601  oeeulem  8603  ecelqsg  8768  elqsn0  8782  pwdom  9131  enfii  9191  phpeqd  9217  ominf  9260  findcard3  9287  marypha1lem  9430  wofib  9542  cantnff  9671  cantnfp1  9678  cantnf  9690  cnfcomlem  9696  ttrcltr  9713  frr3g  9753  r1sscl  9782  rankval3b  9823  infxpidm2  10014  numdom  10035  onssnum  10037  acni  10042  acni2  10043  dfac5  10125  djulepw  10189  infunsdom1  10210  infunsdom  10211  cofsmo  10266  cfsmolem  10267  fin1ai  10290  fin2i  10292  isf34lem1  10369  fin67  10392  itunisuc  10416  axdc3lem4  10450  zornn0g  10502  ttukeylem6  10511  brdom3  10525  tsken  10751  tskcard  10778  r1tskina  10779  intgru  10811  prlem934  11030  ltexprlem7  11039  supaddc  12185  mul2lt0rlt0  13080  xrmaxeq  13162  xrmineq  13163  xmulneg1  13252  ixxun  13344  difelfzle  13618  ssfzoulel  13730  elfznelfzo  13741  ico01fl0  13788  btwnzge0  13797  ltdifltdiv  13803  ioopnfsup  13833  icopnfsup  13834  modifeq2int  13902  suppssfz  13963  expmordi  14136  zzlesq  14174  faclbnd4lem4  14260  hasheni  14312  hashgt0  14352  hashge1  14353  hashprb  14361  lennncl  14488  wrdsymb0  14503  ccatsymb  14536  ccatlid  14540  ccatass  14542  ccatswrd  14622  swrdccat2  14623  ccatpfx  14655  swrdccatfn  14678  swrdccat  14689  revccat  14720  2cshw  14767  cnpart  15191  resqreu  15203  recval  15273  abs1m  15286  abslem2  15290  fzomaxdiflem  15293  sqreulem  15310  sqreu  15311  limsupgre  15429  rlimdiv  15596  fsumparts  15756  climcnds  15801  expcnv  15814  ntrivcvg  15847  mod2eq1n2dvds  16294  ndvdssub  16356  sadcaddlem  16402  rplpwr  16503  dvdssqlem  16507  algcvgblem  16518  eucalgcvga  16527  isprm2lem  16622  powm2modprm  16740  coprimeprodsq  16745  pythagtriplem11  16762  pythagtriplem13  16764  pcadd2  16827  4sqlem11  16892  vdwlem6  16923  vdwlem8  16925  vdwlem10  16927  ramval  16945  ramcl2  16953  ramlb  16956  ram0  16959  mreintcl  17543  mrcval  17558  mrccl  17559  mrcuni  17569  mrcun  17570  acsfiel  17602  rescabs  17786  rescabsOLD  17787  funcres  17850  setcmon  18041  setcepi  18042  fullestrcsetc  18107  funcsetcestrclem8  18118  fullsetcestrc  18122  yonffthlem  18239  pleval2i  18293  pospo  18302  poslubdg  18371  acsdrsel  18500  acsdrscl  18503  acsficl  18504  psss  18537  grpidd  18596  ismndd  18681  gsumsgrpccat  18757  gsumwmhm  18762  mulgaddcom  19014  subgmulg  19056  resghm  19146  conjnsg  19168  f1otrspeq  19356  pmtrval  19360  pmtrrn  19366  pmtrfinv  19370  pmtrprfval  19396  psgnunilem1  19402  psgnunilem5  19403  psgnunilem4  19406  psgneldm2i  19414  lsmelvalix  19550  pj1ghm  19612  efgredlemc  19654  frgp0  19669  qusabl  19774  cycsubgcyg  19810  gsumval3  19816  gsumcllem  19817  ablfac1c  19982  pgpfac1lem5  19990  isrngd  20067  isringd  20179  01eq0ring  20419  lspsneq0b  20768  lmodindp1  20769  lmhmf1o  20801  lmhmpreima  20803  reslmhm  20807  pwssplit3  20816  lspsncmp  20874  lspsneq  20880  znf1o  21326  dsmmlss  21518  frlmlbs  21571  frlmup1  21572  psrgrp  21736  mpfind  21889  mhplss  21917  mat1  22169  chfacfisf  22576  chfacfisfcpmat  22577  uniopn  22619  ntrval  22760  clsval  22761  neival  22826  neiptopreu  22857  lpval  22863  restdis  22902  lmbrf  22984  cnpnei  22988  1stcrest  23177  hauspwdom  23225  lfinpfin  23248  txcnpi  23332  ptrescn  23363  xkococnlem  23383  qtopeu  23440  kqreglem1  23465  ptuncnv  23531  filss  23577  fsubbas  23591  fbasrn  23608  cfinfil  23617  ufinffr  23653  elfm3  23674  rnelfmlem  23676  rnelfm  23677  flimclslem  23708  flfval  23714  isfcf  23758  cnextfvval  23789  cnextf  23790  cnextcn  23791  ustelimasn  23947  trust  23954  restutop  23962  ustuqtop2  23967  utop2nei  23975  ucncn  24010  trcfilu  24019  cnextucn  24028  met1stc  24250  metustexhalf  24285  cfilucfil  24288  psmetutop  24296  nmoix  24466  nmoeq0  24473  idnghm  24480  blcvx  24534  xrsxmet  24545  iccntr  24557  icccmp  24561  iihalf1  24672  iihalf2  24675  xrhmeo  24691  cnheibor  24701  ipcau2  24982  lmmbrf  25010  iscauf  25028  cmetcaulem  25036  bcthlem4  25075  cmetcusp  25102  rrxcph  25140  minveclem4  25180  evthicc2  25209  cniccbdd  25210  ovollb2  25238  ovolunlem1a  25245  ovolunlem1  25246  voliun  25303  icombl  25313  ioombl  25314  iccvolcl  25316  ioovolcl  25319  mbfss  25395  mbfposb  25402  itg2const2  25491  itg2splitlem  25498  itg2gt0  25510  iblss2  25555  itgioo  25565  dvaddf  25693  dvmulf  25694  dvcobr  25697  dvcobrOLD  25698  dvcof  25700  rolle  25742  dvlip  25745  c1lip1  25749  dvivthlem1  25760  lhop1lem  25765  dvfsumlem1  25778  ftc1lem4  25791  ftc1lem5  25792  ply1divmo  25888  coe1termlem  26007  plydiveu  26047  taylplem1  26111  pserulm  26170  abelth  26189  abscxp2  26437  abscxpbnd  26497  logbgt0b  26534  ang180lem2  26551  ang180lem3  26552  isosctrlem1  26559  angpieqvd  26572  atandmtan  26661  birthdaylem3  26694  wilthlem2  26809  wilthimp  26812  isppw  26854  isppw2  26855  dvdsflsumcom  26928  chteq0  26948  perfectlem2  26969  dchrval  26973  dchrinvcl  26992  dchrptlem1  27003  bposlem3  27025  lgslem4  27039  lgsmod  27062  lgsdilem  27063  lgsdir2lem2  27065  lgsdir2  27069  lgsne0  27074  lgsmulsqcoprm  27082  lgseisenlem1  27114  2lgsoddprm  27155  2sqlem4  27160  chpo1ubb  27220  dchrisumn0  27260  pntrsumbnd2  27306  ostthlem1  27366  ostth3  27377  nosupbnd2lem1  27454  noinfbnd2lem1  27469  nocvxmin  27516  eqscut2  27544  sltlpss  27638  idmot  28055  tgelrnln  28148  lmimid  28312  lmiisolem  28314  hypcgrlem1  28317  brcgr  28425  colinearalglem4  28434  colinearalg  28435  axlowdimlem14  28480  axcontlem4  28492  cplgrop  28961  lfgriswlk  29212  pthdlem1  29290  crctcshwlkn0  29342  elwspths2on  29481  clwlkclwwlklem2fv2  29516  frgrncvvdeqlem9  29827  nvss  30113  sspn  30256  nmoub3i  30293  nmblolbii  30319  blocnilem  30324  minvecolem4  30400  htthlem  30437  norm1  30769  norm1exi  30770  pjeq  30919  axpjpj  30940  normcan  31096  pjoi0  31237  nmopub2tALT  31429  nmfnleub2  31446  eighmorth  31484  nmbdoplbi  31544  nmcoplbi  31548  nmophmi  31551  nmbdfnlbi  31569  nmcfnlbi  31572  riesz3i  31582  cnlnadjlem7  31593  branmfn  31625  nmopleid  31659  hstle  31750  superpos  31874  cvexchlem  31888  foresf1o  32009  elabreximd  32014  unidifsnne  32040  f1o3d  32118  fmptco1f1o  32124  funcnvmpt  32159  fgreu  32164  suppovss  32173  fsupprnfi  32181  resf1o  32222  fpwrelmap  32225  xrofsup  32247  eliccelico  32255  elicoelioo  32256  iocinif  32259  difioo  32260  eliccioo  32364  cshf1o  32393  mgcmnt1d  32434  mgcmnt2d  32435  pwrssmgc  32437  gsummpt2co  32470  gsumhashmul  32478  submomnd  32498  symgcom  32514  symgcom2  32515  odpmco  32517  pmtrcnel  32520  pmtridf1o  32523  cycpmco2lem6  32560  cycpmco2lem7  32561  cycpmco2  32562  cyc3co2  32569  cycpmconjv  32571  tocyccntz  32573  cyc3evpm  32579  cycpmconjslem2  32584  cycpmconjs  32585  archirngz  32605  isdrng4  32665  sdrgdvcl  32667  sdrginvcl  32668  ornglmullt  32695  orngrmullt  32696  dvdsrspss  32765  lindssn  32768  linds2eq  32771  nsgqusf1olem1  32798  nsgqusf1olem3  32800  ghmqusker  32806  unitpidl1  32816  elrspunidl  32820  rhmimaidl  32824  drngidlhash  32826  prmidl2  32833  prmidl0  32843  qsidomlem1  32845  mxidlirredi  32861  mxidlirred  32862  ssmxidl  32864  drng0mxidl  32866  opprmxidlabs  32875  qsdrngilem  32882  qsdrngi  32883  qsdrng  32885  ply1scleq  32913  ply1asclunit  32928  ply1degltlss  32942  ply1gsumz  32944  lsssra  32963  lbslsat  32989  ply1degltdimlem  32995  lindsunlem  32997  lindsun  32998  dimkerim  33000  fedgmullem1  33002  fedgmullem2  33003  fedgmul  33004  evls1fldgencl  33033  irngss  33040  0ringirng  33042  irngnzply1  33044  irngnminplynz  33060  algextdeglem2  33063  algextdeglem4  33065  madjusmdetlem2  33106  qtophaus  33114  locfinreflem  33118  zarclssn  33151  zarmxt1  33158  zarcmplem  33159  rhmpreimacn  33163  unitdivcld  33179  tpr2rico  33190  ordtrestNEW  33199  lmxrge0  33230  elzrhunit  33257  qqhf  33264  indf1ofs  33322  gsumesum  33355  esumfsup  33366  esumcvg  33382  issgon  33419  sigainb  33432  insiga  33433  isrnmeas  33496  measvunilem  33508  volmeas  33527  ddeval1  33530  ddeval0  33531  imambfm  33559  omssubadd  33597  carsgclctunlem3  33617  eulerpartlemf  33667  eulerpartlemgvv  33673  probun  33716  dstfrvunirn  33771  plymulx  33857  signslema  33871  signstfvn  33878  signsvtn0  33879  signstfvneq0  33881  signstres  33884  signstfveq0a  33885  breprexplemc  33942  logdivsqrle  33960  hgt750lemg  33964  tgoldbachgtda  33971  tgoldbachgt  33973  lpadmax  33992  lpadleft  33993  lpadright  33994  bnj529  34050  bnj548  34206  bnj570  34214  bnj852  34230  bnj929  34245  bnj1097  34290  bnj1118  34293  bnj1145  34302  funen1cnv  34389  spthcycl  34418  acycgr0v  34437  derangen  34461  subfacp1lem2b  34470  subfacp1lem4  34472  subfacp1lem5  34473  derangfmla  34479  ptpconn  34522  mppspstlem  34860  wsuclem  35101  colinearex  35336  btwnconn1lem11  35373  btwnconn1lem12  35374  fwddifnp1  35441  nn0prpwlem  35510  bj-snmoore  36297  bj-imdiridlem  36369  relowlpssretop  36548  fin2so  36778  matunitlindflem2  36788  ptrecube  36791  poimirlem8  36799  poimirlem13  36804  poimirlem15  36806  poimirlem24  36815  poimirlem25  36816  poimirlem26  36817  heicant  36826  mblfinlem2  36829  voliunnfl  36835  mbfresfi  36837  itg2addnclem  36842  itg2addnclem3  36844  itg2gt0cn  36846  ftc1cnnclem  36862  ftc1anclem5  36868  cover2  36886  indexdom  36905  sdclem1  36914  fdc  36916  equivbnd2  36963  heiborlem8  36989  heibor  36992  isdrngo2  37129  iscringd  37169  smprngopr  37223  prnc  37238  eqbrtr  37401  eqeltr  37403  islfld  38235  lkrshpor  38280  lfl1dim  38294  lfl1dim2N  38295  cmtcomlemN  38421  2lplnmN  38733  pmapjat1  39027  trlnid  39353  tendoex  40149  dia1dimid  40237  dibval2  40318  dihmeetlem2N  40473  dochlkr  40559  mapdcv  40834  hdmaplkr  41087  hdmapip0  41089  hlhillcs  41136  frlmvscadiccat  41386  dvdsexpnn  41533  nacsfix  41752  3rexfrabdioph  41837  4rexfrabdioph  41838  6rexfrabdioph  41839  7rexfrabdioph  41840  eldioph4b  41851  pellexlem2  41870  pellexlem5  41873  jm2.26lem3  42042  numinfctb  42147  ordne0gt0  42313  omge1  42349  omlim2  42351  omord2lim  42352  omord2i  42353  tfsconcatfv  42393  tfsconcatb0  42396  oaun3lem1  42426  ntrclsfv1  43108  ntrneifv1  43132  ntrneifv2  43133  cvgdvgrat  43374  radcnvrat  43375  dvconstbi  43395  bccbc  43406  elpwgded  43627  elpwgdedVD  43980  sspwimpcf  43983  sspwimpcfVD  43984  sspwimpALT2  43991  ax6e2ndeqALT  43994  eliuniin  44089  eliuniin2  44110  qinioo  44546  dfxlim2v  44861  xlimliminflimsup  44876  cncfiooicclem1  44907  ibliooicc  44985  stoweidlem27  45041  stoweidlem28  45042  fourierdlem89  45209  fourierdlem91  45211  fourierdlem92  45212  smflimmpt  45824  odz2prm2pw  46529  perfectALTVlem2  46688  blen1b  47361  naryfvalelfv  47405  itscnhlc0yqe  47532  itsclquadb  47549  lubeldm2  47676  glbeldm2  47677  ipolub  47700  ipoglb  47703  functhinclem1  47748  thincciso  47756  prsthinc  47761  prstchom2ALT  47786  onetansqsecsq  47893  cotsqcscsq  47894  aacllem  47935