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

Syntax hints:   → wi 4   ↔ wb 206   ∧ 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 207  df-an 396

This theorem is referenced by:  bitr  804  exbiri  810  biadanid  822  bibiad  839  oplem1  1056  eqtr  2749  pm13.181  3007  opabss  5171  axprlem4OLD  5384  axprlem5OLD  5385  euotd  5473  brcogw  5832  somin1  6106  xpdifid  6141  funfni  6624  fnssres  6641  fn0  6649  fnimadisj  6650  fnimaeq0  6651  foimacnv  6817  fvelimab  6933  dffv2  6956  fvopab3ig  6964  dff3  7072  dffo4  7075  fpr2g  7185  ralima  7211  f1eqcocnv  7276  isomin  7312  f1ocnv2d  7642  fnexALT  7929  xp1st  8000  xp2nd  8001  frrlem3  8267  fpr2  8283  wfr3g  8298  wfr2  8306  iinon  8309  tfr3  8367  oawordri  8514  oaass  8525  omeulem1  8546  oeoa  8561  oeoe  8563  oeeulem  8565  elqsn0  8757  pwdom  9093  enfii  9150  phpeqd  9176  ominf  9205  findcard3  9229  marypha1lem  9384  wofib  9498  cantnff  9627  cantnfp1  9634  cantnf  9646  cnfcomlem  9652  ttrcltr  9669  frr3g  9709  r1sscl  9738  rankval3b  9779  infxpidm2  9970  numdom  9991  onssnum  9993  acni  9998  acni2  9999  dfac5  10082  djulepw  10146  infunsdom1  10165  infunsdom  10166  cofsmo  10222  cfsmolem  10223  fin1ai  10246  fin2i  10248  isf34lem1  10325  fin67  10348  itunisuc  10372  axdc3lem4  10406  zornn0g  10458  ttukeylem6  10467  brdom3  10481  tsken  10707  tskcard  10734  r1tskina  10735  intgru  10767  prlem934  10986  ltexprlem7  10995  supaddc  12150  mul2lt0rlt0  13055  xrmaxeq  13139  xrmineq  13140  xmulneg1  13229  ixxun  13322  difelfzle  13602  ssfzoulel  13721  elfznelfzo  13733  ico01fl0  13781  btwnzge0  13790  ltdifltdiv  13796  ioopnfsup  13826  icopnfsup  13827  modifeq2int  13898  suppssfz  13959  expmordi  14132  zzlesq  14171  faclbnd4lem4  14261  hasheni  14313  hashgt0  14353  hashge1  14354  hashprb  14362  lennncl  14499  wrdsymb0  14514  ccatsymb  14547  ccatlid  14551  ccatass  14553  ccatswrd  14633  swrdccat2  14634  ccatpfx  14666  swrdccatfn  14689  swrdccat  14700  revccat  14731  2cshw  14778  cnpart  15206  resqreu  15218  recval  15289  abs1m  15302  abslem2  15306  fzomaxdiflem  15309  sqreulem  15326  sqreu  15327  limsupgre  15447  rlimdiv  15612  fsumparts  15772  climcnds  15817  expcnv  15830  ntrivcvg  15863  mod2eq1n2dvds  16317  ndvdssub  16379  sadcaddlem  16427  rplpwr  16528  dvdssqlem  16536  algcvgblem  16547  eucalgcvga  16556  isprm2lem  16651  powm2modprm  16774  coprimeprodsq  16779  pythagtriplem11  16796  pythagtriplem13  16798  pcadd2  16861  4sqlem11  16926  vdwlem6  16957  vdwlem8  16959  vdwlem10  16961  ramval  16979  ramcl2  16987  ramlb  16990  ram0  16993  mreintcl  17556  mrcval  17571  mrccl  17572  mrcuni  17582  mrcun  17583  acsfiel  17615  rescabs  17795  funcres  17858  setcmon  18049  setcepi  18050  fullestrcsetc  18112  funcsetcestrclem8  18123  fullsetcestrc  18127  yonffthlem  18243  pleval2i  18295  pospo  18304  poslubdg  18373  acsdrsel  18502  acsdrscl  18505  acsficl  18506  psss  18539  grpidd  18598  ismndd  18683  gsumsgrpccat  18767  gsumwmhm  18772  mulgaddcom  19030  subgmulg  19072  resghm  19164  conjnsg  19186  ghmqusker  19219  f1otrspeq  19377  pmtrval  19381  pmtrrn  19387  pmtrfinv  19391  pmtrprfval  19417  psgnunilem1  19423  psgnunilem5  19424  psgnunilem4  19427  psgneldm2i  19435  lsmelvalix  19571  pj1ghm  19633  efgredlemc  19675  frgp0  19690  qusabl  19795  cycsubgcyg  19831  gsumval3  19837  gsumcllem  19838  ablfac1c  20003  pgpfac1lem5  20011  isrngd  20082  isringd  20200  01eq0ring  20439  lspsneq0b  20919  lmodindp1  20920  lmhmf1o  20953  lmhmpreima  20955  reslmhm  20959  pwssplit3  20968  lspsncmp  21026  lspsneq  21032  znf1o  21461  dsmmlss  21653  frlmlbs  21706  frlmup1  21707  psrgrp  21865  mpfind  22014  psdmul  22053  ply1scleq  22192  mat1  22334  chfacfisf  22741  chfacfisfcpmat  22742  uniopn  22784  ntrval  22923  clsval  22924  neival  22989  neiptopreu  23020  lpval  23026  restdis  23065  lmbrf  23147  cnpnei  23151  1stcrest  23340  hauspwdom  23388  lfinpfin  23411  txcnpi  23495  ptrescn  23526  xkococnlem  23546  qtopeu  23603  kqreglem1  23628  ptuncnv  23694  filss  23740  fsubbas  23754  fbasrn  23771  cfinfil  23780  ufinffr  23816  elfm3  23837  rnelfmlem  23839  rnelfm  23840  flimclslem  23871  flfval  23877  isfcf  23921  cnextfvval  23952  cnextf  23953  cnextcn  23954  ustelimasn  24110  trust  24117  restutop  24125  ustuqtop2  24130  utop2nei  24138  ucncn  24172  trcfilu  24181  cnextucn  24190  met1stc  24409  metustexhalf  24444  cfilucfil  24447  psmetutop  24455  nmoix  24617  nmoeq0  24624  idnghm  24631  blcvx  24686  xrsxmet  24698  iccntr  24710  icccmp  24714  iihalf1  24825  iihalf2  24828  xrhmeo  24844  cnheibor  24854  ipcau2  25134  lmmbrf  25162  iscauf  25180  cmetcaulem  25188  bcthlem4  25227  cmetcusp  25254  rrxcph  25292  minveclem4  25332  evthicc2  25361  cniccbdd  25362  ovollb2  25390  ovolunlem1a  25397  ovolunlem1  25398  voliun  25455  icombl  25465  ioombl  25466  iccvolcl  25468  ioovolcl  25471  mbfss  25547  mbfposb  25554  itg2const2  25642  itg2splitlem  25649  itg2gt0  25661  iblss2  25707  itgioo  25717  dvaddf  25845  dvmulf  25846  dvcobr  25849  dvcobrOLD  25850  dvcof  25852  rolle  25894  dvlip  25898  c1lip1  25902  dvivthlem1  25913  lhop1lem  25918  dvfsumlem1  25932  ftc1lem4  25946  ftc1lem5  25947  ply1divmo  26041  coe1termlem  26163  plydiveu  26206  taylplem1  26270  pserulm  26331  abelth  26351  abscxp2  26602  abscxpbnd  26663  logbgt0b  26703  ang180lem2  26720  ang180lem3  26721  isosctrlem1  26728  angpieqvd  26741  atandmtan  26830  birthdaylem3  26863  wilthlem2  26979  wilthimp  26982  isppw  27024  isppw2  27025  dvdsflsumcom  27098  chteq0  27120  perfectlem2  27141  dchrval  27145  dchrinvcl  27164  dchrptlem1  27175  bposlem3  27197  lgslem4  27211  lgsmod  27234  lgsdilem  27235  lgsdir2lem2  27237  lgsdir2  27241  lgsne0  27246  lgsmulsqcoprm  27254  lgseisenlem1  27286  2lgsoddprm  27327  2sqlem4  27332  chpo1ubb  27392  dchrisumn0  27432  pntrsumbnd2  27478  ostthlem1  27538  ostth3  27549  nosupbnd2lem1  27627  noinfbnd2lem1  27642  nocvxmin  27690  eqscut2  27718  sltlpss  27819  madefi  27824  absslt  28151  eucliddivs  28265  peano5uzs  28292  idmot  28464  tgelrnln  28557  lmimid  28721  lmiisolem  28723  hypcgrlem1  28726  brcgr  28827  colinearalglem4  28836  colinearalg  28837  axlowdimlem14  28882  axcontlem4  28894  cplgrop  29364  lfgriswlk  29616  pthdlem1  29696  crctcshwlkn0  29751  elwspths2on  29890  clwlkclwwlklem2fv2  29925  frgrncvvdeqlem9  30236  nvss  30522  sspn  30665  nmoub3i  30702  nmblolbii  30728  blocnilem  30733  minvecolem4  30809  htthlem  30846  norm1  31178  norm1exi  31179  pjeq  31328  axpjpj  31349  normcan  31505  pjoi0  31646  nmopub2tALT  31838  nmfnleub2  31855  eighmorth  31893  nmbdoplbi  31953  nmcoplbi  31957  nmophmi  31960  nmbdfnlbi  31978  nmcfnlbi  31981  riesz3i  31991  cnlnadjlem7  32002  branmfn  32034  nmopleid  32068  hstle  32159  superpos  32283  cvexchlem  32297  foresf1o  32433  elabreximd  32439  prssad  32458  prssbd  32459  unidifsnne  32465  tpssad  32468  f1o3d  32551  fmptco1f1o  32557  funcnvmpt  32591  fgreu  32596  suppovss  32604  elsuppfnd  32605  fsupprnfi  32615  resf1o  32653  fpwrelmap  32656  argcj  32672  xrofsup  32690  eliccelico  32700  elicoelioo  32701  iocinif  32704  difioo  32705  hashpss  32734  hashne0  32735  elq2  32736  oexpled  32772  indf1ofs  32789  eliccioo  32851  cshf1o  32884  mgcmnt1d  32923  mgcmnt2d  32924  pwrssmgc  32926  chnind  32937  chnub  32938  chnccats1  32941  mndlactf1o  32971  mndractf1o  32972  gsummpt2co  32988  gsumhashmul  33001  submomnd  33024  symgcom  33040  symgcom2  33041  odpmco  33043  pmtrcnel  33046  pmtridf1o  33051  cycpmco2lem6  33088  cycpmco2lem7  33089  cycpmco2  33090  cyc3co2  33097  cycpmconjv  33099  tocyccntz  33101  cyc3evpm  33107  cycpmconjslem2  33112  cycpmconjs  33113  fxpsubm  33129  archirngz  33143  unitnz  33190  elrgspnlem1  33193  elrgspnlem2  33194  elrgspnlem4  33196  elrgspnsubrun  33200  rloccring  33221  rlocf1  33224  domnpropd  33227  rrgsubm  33234  isdrng4  33245  sdrgdvcl  33249  sdrginvcl  33250  fracfld  33258  ornglmullt  33285  orngrmullt  33286  lindssn  33349  linds2eq  33352  dvdsrspss  33358  nsgqusf1olem1  33384  nsgqusf1olem3  33386  unitpidl1  33395  elrspunidl  33399  rhmimaidl  33403  drngidlhash  33405  prmidl2  33412  prmidl0  33421  qsidomlem1  33423  ssdifidlprm  33429  mxidlirredi  33442  mxidlirred  33443  ssmxidl  33445  drng0mxidl  33447  opprmxidlabs  33458  qsdrngilem  33465  qsdrngi  33466  qsdrng  33468  rsprprmprmidl  33493  rsprprmprmidlb  33494  rprmasso2  33497  rprmirredlem  33501  rprmirredb  33503  1arithidomlem2  33507  1arithufdlem4  33518  1arithufd  33519  ressply1evls1  33534  ply1asclunit  33543  ply1dg1rt  33548  ply1mulrtss  33550  ply1dg3rt0irred  33551  ply1degltlss  33562  ply1gsumz  33564  lsssra  33584  exsslsb  33592  lbslsat  33612  lindsunlem  33620  lindsun  33621  dimkerim  33623  fedgmullem1  33625  fedgmullem2  33626  fedgmul  33627  dimlssid  33628  lvecendof1f1o  33629  assalactf1o  33631  sdrgfldext  33646  fldsdrgfldext  33657  fldgenfldext  33663  evls1fldgencl  33665  fldextrspunlsp  33669  fldextrspunlem1  33670  fldextrspunfld  33671  irngss  33682  0ringirng  33684  irngnzply1  33686  irngnminplynz  33702  minplyelirng  33705  irredminply  33706  algextdeglem2  33708  algextdeglem4  33710  constrconj  33735  constrextdg2lem  33738  constrext2chnlem  33740  iconstr  33756  constrsdrg  33765  cos9thpiminplylem1  33772  cos9thpiminplylem2  33773  cos9thpiminplylem3  33774  cos9thpiminplylem5  33776  madjusmdetlem2  33818  qtophaus  33826  locfinreflem  33830  zarclssn  33863  zarmxt1  33870  zarcmplem  33871  rhmpreimacn  33875  unitdivcld  33891  tpr2rico  33902  ordtrestNEW  33911  lmxrge0  33942  elzrhunit  33967  qqhf  33976  gsumesum  34049  esumfsup  34060  esumcvg  34076  issgon  34113  sigainb  34126  insiga  34127  isrnmeas  34190  measvunilem  34202  volmeas  34221  ddeval1  34224  ddeval0  34225  imambfm  34253  omssubadd  34291  carsgclctunlem3  34311  eulerpartlemf  34361  eulerpartlemgvv  34367  probun  34410  dstfrvunirn  34466  plymulx  34539  signslema  34553  signstfvn  34560  signsvtn0  34561  signstfvneq0  34563  signstres  34566  signstfveq0a  34567  breprexplemc  34623  logdivsqrle  34641  hgt750lemg  34645  tgoldbachgtda  34652  tgoldbachgt  34654  lpadmax  34673  lpadleft  34674  lpadright  34675  bnj529  34731  bnj548  34887  bnj570  34895  bnj852  34911  bnj929  34926  bnj1097  34971  bnj1118  34974  bnj1145  34983  funen1cnv  35078  spthcycl  35116  acycgr0v  35135  derangen  35159  subfacp1lem2b  35168  subfacp1lem4  35170  subfacp1lem5  35171  derangfmla  35177  ptpconn  35220  mppspstlem  35558  wsuclem  35813  colinearex  36048  btwnconn1lem11  36085  btwnconn1lem12  36086  fwddifnp1  36153  nn0prpwlem  36310  bj-snmoore  37101  bj-imdiridlem  37173  relowlpssretop  37352  fin2so  37601  matunitlindflem2  37611  ptrecube  37614  poimirlem8  37622  poimirlem13  37627  poimirlem15  37629  poimirlem24  37638  poimirlem25  37639  poimirlem26  37640  heicant  37649  mblfinlem2  37652  voliunnfl  37658  mbfresfi  37660  itg2addnclem  37665  itg2addnclem3  37667  itg2gt0cn  37669  ftc1cnnclem  37685  ftc1anclem5  37691  cover2  37709  indexdom  37728  sdclem1  37737  fdc  37739  equivbnd2  37786  heiborlem8  37812  heibor  37815  isdrngo2  37952  iscringd  37992  smprngopr  38046  prnc  38061  eqbrtr  38220  eqeltr  38222  islfld  39055  lkrshpor  39100  lfl1dim  39114  lfl1dim2N  39115  cmtcomlemN  39241  2lplnmN  39553  pmapjat1  39847  trlnid  40173  tendoex  40969  dia1dimid  41057  dibval2  41138  dihmeetlem2N  41293  dochlkr  41379  mapdcv  41654  hdmaplkr  41907  hdmapip0  41909  hlhillcs  41952  aks6d1c6lem4  42161  dvdsexpnn  42321  readvrec  42350  frlmvscadiccat  42494  psrmnd  42533  nacsfix  42700  3rexfrabdioph  42785  4rexfrabdioph  42786  6rexfrabdioph  42787  7rexfrabdioph  42788  eldioph4b  42799  pellexlem2  42818  pellexlem5  42821  jm2.26lem3  42990  numinfctb  43092  ordne0gt0  43250  omge1  43286  omlim2  43288  omord2lim  43289  omord2i  43290  tfsconcatfv  43330  tfsconcatb0  43333  oaun3lem1  43363  ntrclsfv1  44044  ntrneifv1  44068  ntrneifv2  44069  cvgdvgrat  44302  radcnvrat  44303  dvconstbi  44323  bccbc  44334  elpwgded  44554  elpwgdedVD  44906  sspwimpcf  44909  sspwimpcfVD  44910  sspwimpALT2  44917  ax6e2ndeqALT  44920  eliuniin  45093  eliuniin2  45114  qinioo  45533  dfxlim2v  45845  xlimliminflimsup  45860  cncfiooicclem1  45891  ibliooicc  45969  stoweidlem27  46025  stoweidlem28  46026  fourierdlem89  46193  fourierdlem91  46195  fourierdlem92  46196  smflimmpt  46808  odz2prm2pw  47564  perfectALTVlem2  47723  blen1b  48577  naryfvalelfv  48621  itscnhlc0yqe  48748  itsclquadb  48765  lubeldm2  48944  glbeldm2  48945  ipolub  48976  ipoglb  48979  fucofulem1  49299  functhinclem1  49433  thincciso  49442  prsthinc  49453  functermclem  49496  prstchom2ALT  49553  onetansqsecsq  49750  cotsqcscsq  49751  aacllem  49790