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  2754  pm13.181  3012  opabss  5160  axprlem4OLD  5372  axprlem5OLD  5373  euotd  5459  brcogw  5815  somin1  6088  xpdifid  6124  funfni  6596  fnssres  6613  fn0  6621  fnimadisj  6622  fnimaeq0  6623  foimacnv  6789  fvelimab  6904  dffv2  6927  fvopab3ig  6935  dff3  7043  dffo4  7046  fpr2g  7155  ralima  7181  f1eqcocnv  7245  isomin  7281  f1ocnv2d  7609  fnexALT  7893  xp1st  7963  xp2nd  7964  frrlem3  8228  fpr2  8244  wfr3g  8259  wfr2  8267  iinon  8270  tfr3  8328  oawordri  8475  oaass  8486  omeulem1  8507  oeoa  8523  oeoe  8525  oeeulem  8527  elqsn0  8719  pwdom  9055  enfii  9108  phpeqd  9134  ominf  9162  findcard3  9181  marypha1lem  9334  wofib  9448  cantnff  9581  cantnfp1  9588  cantnf  9600  cnfcomlem  9606  ttrcltr  9623  frr3g  9666  r1sscl  9695  rankval3b  9736  infxpidm2  9925  numdom  9946  onssnum  9948  acni  9953  acni2  9954  dfac5  10037  djulepw  10101  infunsdom1  10120  infunsdom  10121  cofsmo  10177  cfsmolem  10178  fin1ai  10201  fin2i  10203  isf34lem1  10280  fin67  10303  itunisuc  10327  axdc3lem4  10361  zornn0g  10413  ttukeylem6  10422  brdom3  10436  tsken  10663  tskcard  10690  r1tskina  10691  intgru  10723  prlem934  10942  ltexprlem7  10951  supaddc  12107  mul2lt0rlt0  13007  xrmaxeq  13092  xrmineq  13093  xmulneg1  13182  ixxun  13275  difelfzle  13555  ssfzoulel  13674  elfznelfzo  13687  ico01fl0  13737  btwnzge0  13746  ltdifltdiv  13752  ioopnfsup  13782  icopnfsup  13783  modifeq2int  13854  suppssfz  13915  expmordi  14088  zzlesq  14127  faclbnd4lem4  14217  hasheni  14269  hashgt0  14309  hashge1  14310  hashprb  14318  lennncl  14455  wrdsymb0  14470  ccatsymb  14504  ccatlid  14508  ccatass  14510  ccatswrd  14590  swrdccat2  14591  ccatpfx  14622  swrdccatfn  14645  swrdccat  14656  revccat  14687  2cshw  14734  cnpart  15161  resqreu  15173  recval  15244  abs1m  15257  abslem2  15261  fzomaxdiflem  15264  sqreulem  15281  sqreu  15282  limsupgre  15402  rlimdiv  15567  fsumparts  15727  climcnds  15772  expcnv  15785  ntrivcvg  15818  mod2eq1n2dvds  16272  ndvdssub  16334  sadcaddlem  16382  rplpwr  16483  dvdssqlem  16491  algcvgblem  16502  eucalgcvga  16511  isprm2lem  16606  powm2modprm  16729  coprimeprodsq  16734  pythagtriplem11  16751  pythagtriplem13  16753  pcadd2  16816  4sqlem11  16881  vdwlem6  16912  vdwlem8  16914  vdwlem10  16916  ramval  16934  ramcl2  16942  ramlb  16945  ram0  16948  mreintcl  17512  mrcval  17531  mrccl  17532  mrcuni  17542  mrcun  17543  acsfiel  17575  rescabs  17755  funcres  17818  setcmon  18009  setcepi  18010  fullestrcsetc  18072  funcsetcestrclem8  18083  fullsetcestrc  18087  yonffthlem  18203  pleval2i  18255  pospo  18264  poslubdg  18333  acsdrsel  18464  acsdrscl  18467  acsficl  18468  psss  18501  chnind  18542  chnub  18543  chnccats1  18546  chnccat  18547  grpidd  18594  ismndd  18679  gsumsgrpccat  18763  gsumwmhm  18768  mulgaddcom  19026  subgmulg  19068  resghm  19159  conjnsg  19181  ghmqusker  19214  f1otrspeq  19374  pmtrval  19378  pmtrrn  19384  pmtrfinv  19388  pmtrprfval  19414  psgnunilem1  19420  psgnunilem5  19421  psgnunilem4  19424  psgneldm2i  19432  lsmelvalix  19568  pj1ghm  19630  efgredlemc  19672  frgp0  19687  qusabl  19792  cycsubgcyg  19828  gsumval3  19834  gsumcllem  19835  ablfac1c  20000  pgpfac1lem5  20008  submomnd  20059  isrngd  20106  isringd  20224  01eq0ring  20461  ornglmullt  20800  orngrmullt  20801  lspsneq0b  20962  lmodindp1  20963  lmhmf1o  20996  lmhmpreima  20998  reslmhm  21002  pwssplit3  21011  lspsncmp  21069  lspsneq  21075  znf1o  21504  dsmmlss  21697  frlmlbs  21750  frlmup1  21751  psrgrp  21910  mpfind  22068  psdmul  22107  ply1scleq  22247  mat1  22389  chfacfisf  22796  chfacfisfcpmat  22797  uniopn  22839  ntrval  22978  clsval  22979  neival  23044  neiptopreu  23075  lpval  23081  restdis  23120  lmbrf  23202  cnpnei  23206  1stcrest  23395  hauspwdom  23443  lfinpfin  23466  txcnpi  23550  ptrescn  23581  xkococnlem  23601  qtopeu  23658  kqreglem1  23683  ptuncnv  23749  filss  23795  fsubbas  23809  fbasrn  23826  cfinfil  23835  ufinffr  23871  elfm3  23892  rnelfmlem  23894  rnelfm  23895  flimclslem  23926  flfval  23932  isfcf  23976  cnextfvval  24007  cnextf  24008  cnextcn  24009  ustelimasn  24165  trust  24171  restutop  24179  ustuqtop2  24184  utop2nei  24192  ucncn  24226  trcfilu  24235  cnextucn  24244  met1stc  24463  metustexhalf  24498  cfilucfil  24501  psmetutop  24509  nmoix  24671  nmoeq0  24678  idnghm  24685  blcvx  24740  xrsxmet  24752  iccntr  24764  icccmp  24768  iihalf1  24879  iihalf2  24882  xrhmeo  24898  cnheibor  24908  ipcau2  25188  lmmbrf  25216  iscauf  25234  cmetcaulem  25242  bcthlem4  25281  cmetcusp  25308  rrxcph  25346  minveclem4  25386  evthicc2  25415  cniccbdd  25416  ovollb2  25444  ovolunlem1a  25451  ovolunlem1  25452  voliun  25509  icombl  25519  ioombl  25520  iccvolcl  25522  ioovolcl  25525  mbfss  25601  mbfposb  25608  itg2const2  25696  itg2splitlem  25703  itg2gt0  25715  iblss2  25761  itgioo  25771  dvaddf  25899  dvmulf  25900  dvcobr  25903  dvcobrOLD  25904  dvcof  25906  rolle  25948  dvlip  25952  c1lip1  25956  dvivthlem1  25967  lhop1lem  25972  dvfsumlem1  25986  ftc1lem4  26000  ftc1lem5  26001  ply1divmo  26095  coe1termlem  26217  plydiveu  26260  taylplem1  26324  pserulm  26385  abelth  26405  abscxp2  26656  abscxpbnd  26717  logbgt0b  26757  ang180lem2  26774  ang180lem3  26775  isosctrlem1  26782  angpieqvd  26795  atandmtan  26884  birthdaylem3  26917  wilthlem2  27033  wilthimp  27036  isppw  27078  isppw2  27079  dvdsflsumcom  27152  chteq0  27174  perfectlem2  27195  dchrval  27199  dchrinvcl  27218  dchrptlem1  27229  bposlem3  27251  lgslem4  27265  lgsmod  27288  lgsdilem  27289  lgsdir2lem2  27291  lgsdir2  27295  lgsne0  27300  lgsmulsqcoprm  27308  lgseisenlem1  27340  2lgsoddprm  27381  2sqlem4  27386  chpo1ubb  27446  dchrisumn0  27486  pntrsumbnd2  27532  ostthlem1  27592  ostth3  27603  nosupbnd2lem1  27681  noinfbnd2lem1  27696  nocvxmin  27745  eqscut2  27774  sltlpss  27880  madefi  27885  absslt  28217  eucliddivs  28334  peano5uzs  28362  elreno2  28440  idmot  28558  tgelrnln  28651  lmimid  28815  lmiisolem  28817  hypcgrlem1  28820  brcgr  28922  colinearalglem4  28931  colinearalg  28932  axlowdimlem14  28977  axcontlem4  28989  cplgrop  29459  lfgriswlk  29709  pthdlem1  29788  crctcshwlkn0  29843  elwspths2on  29984  elwspths2onw  29985  clwlkclwwlklem2fv2  30020  frgrncvvdeqlem9  30331  nvss  30617  sspn  30760  nmoub3i  30797  nmblolbii  30823  blocnilem  30828  minvecolem4  30904  htthlem  30941  norm1  31273  norm1exi  31274  pjeq  31423  axpjpj  31444  normcan  31600  pjoi0  31741  nmopub2tALT  31933  nmfnleub2  31950  eighmorth  31988  nmbdoplbi  32048  nmcoplbi  32052  nmophmi  32055  nmbdfnlbi  32073  nmcfnlbi  32076  riesz3i  32086  cnlnadjlem7  32097  branmfn  32129  nmopleid  32163  hstle  32254  superpos  32378  cvexchlem  32392  foresf1o  32528  elabreximd  32534  prssad  32553  prssbd  32554  unidifsnne  32560  tpssad  32563  fresunsn  32652  f1o3d  32653  fmptco1f1o  32660  funcnvmpt  32694  fgreu  32699  suppovss  32709  elsuppfnd  32710  fsupprnfi  32720  resf1o  32758  fpwrelmap  32761  argcj  32777  xrofsup  32796  eliccelico  32806  elicoelioo  32807  iocinif  32810  difioo  32811  hashpss  32838  hashne0  32839  elq2  32841  oexpled  32877  indf1ofs  32897  eliccioo  32961  cshf1o  32993  mgcmnt1d  33028  mgcmnt2d  33029  pwrssmgc  33031  mndlactf1o  33061  mndractf1o  33062  gsummpt2co  33080  gsumhashmul  33099  gsummulsubdishift1  33100  symgcom  33114  symgcom2  33115  odpmco  33117  pmtrcnel  33120  pmtridf1o  33125  cycpmco2lem6  33162  cycpmco2lem7  33163  cycpmco2  33164  cyc3co2  33171  cycpmconjv  33173  tocyccntz  33175  cyc3evpm  33181  cycpmconjslem2  33186  cycpmconjs  33187  fxpsubm  33203  fxpsubg  33204  fxpsubrg  33205  fxpsdrg  33206  archirngz  33220  unitnz  33270  elrgspnlem1  33273  elrgspnlem2  33274  elrgspnlem4  33276  elrgspnsubrun  33280  rloccring  33301  rlocf1  33304  domnpropd  33308  rrgsubm  33315  isdrng4  33326  sdrgdvcl  33330  sdrginvcl  33331  fracfld  33339  lindssn  33408  linds2eq  33411  dvdsrspss  33417  nsgqusf1olem1  33443  nsgqusf1olem3  33445  unitpidl1  33454  elrspunidl  33458  rhmimaidl  33462  drngidlhash  33464  prmidl2  33471  prmidl0  33480  qsidomlem1  33482  ssdifidlprm  33488  mxidlirredi  33501  mxidlirred  33502  ssmxidl  33504  drng0mxidl  33506  opprmxidlabs  33517  qsdrngilem  33524  qsdrngi  33525  qsdrng  33527  rsprprmprmidl  33552  rsprprmprmidlb  33553  rprmasso2  33556  rprmirredlem  33560  rprmirredb  33562  1arithidomlem2  33566  1arithufdlem4  33577  1arithufd  33578  ressply1evls1  33595  ply1asclunit  33604  ply1dg1rt  33610  ply1mulrtss  33612  ply1dg3rt0irred  33614  ply1degltlss  33626  ply1gsumz  33629  evlextv  33656  esplyfv1  33676  esplyind  33680  vietadeg1  33683  lsssra  33693  exsslsb  33702  lbslsat  33722  lindsunlem  33730  lindsun  33731  dimkerim  33733  fedgmullem1  33735  fedgmullem2  33736  fedgmul  33737  dimlssid  33738  lvecendof1f1o  33739  assalactf1o  33741  sdrgfldext  33756  fldsdrgfldext  33767  fldgenfldext  33774  evls1fldgencl  33776  fldextrspunlsp  33780  fldextrspunlem1  33781  fldextrspunfld  33782  irngss  33793  0ringirng  33795  irngnzply1  33797  extdgfialglem1  33798  irngnminplynz  33818  minplyelirng  33821  irredminply  33822  algextdeglem2  33824  algextdeglem4  33826  constrconj  33851  constrextdg2lem  33854  constrext2chnlem  33856  iconstr  33872  constrsdrg  33881  cos9thpiminplylem1  33888  cos9thpiminplylem2  33889  cos9thpiminplylem3  33890  cos9thpiminplylem5  33892  madjusmdetlem2  33934  qtophaus  33942  locfinreflem  33946  zarclssn  33979  zarmxt1  33986  zarcmplem  33987  rhmpreimacn  33991  unitdivcld  34007  tpr2rico  34018  ordtrestNEW  34027  lmxrge0  34058  elzrhunit  34083  qqhf  34092  gsumesum  34165  esumfsup  34176  esumcvg  34192  issgon  34229  sigainb  34242  insiga  34243  isrnmeas  34306  measvunilem  34318  volmeas  34337  ddeval1  34340  ddeval0  34341  imambfm  34368  omssubadd  34406  carsgclctunlem3  34426  eulerpartlemf  34476  eulerpartlemgvv  34482  probun  34525  dstfrvunirn  34581  plymulx  34654  signslema  34668  signstfvn  34675  signsvtn0  34676  signstfvneq0  34678  signstres  34681  signstfveq0a  34682  breprexplemc  34738  logdivsqrle  34756  hgt750lemg  34760  tgoldbachgtda  34767  tgoldbachgt  34769  lpadmax  34788  lpadleft  34789  lpadright  34790  bnj529  34846  bnj548  35002  bnj570  35010  bnj852  35026  bnj929  35041  bnj1097  35086  bnj1118  35089  bnj1145  35098  funen1cnv  35193  fissorduni  35195  spthcycl  35272  acycgr0v  35291  derangen  35315  subfacp1lem2b  35324  subfacp1lem4  35326  subfacp1lem5  35327  derangfmla  35333  ptpconn  35376  mppspstlem  35714  wsuclem  35966  colinearex  36203  btwnconn1lem11  36240  btwnconn1lem12  36241  fwddifnp1  36308  nn0prpwlem  36465  bj-snmoore  37257  bj-imdiridlem  37329  relowlpssretop  37508  fin2so  37747  matunitlindflem2  37757  ptrecube  37760  poimirlem8  37768  poimirlem13  37773  poimirlem15  37775  poimirlem24  37784  poimirlem25  37785  poimirlem26  37786  heicant  37795  mblfinlem2  37798  voliunnfl  37804  mbfresfi  37806  itg2addnclem  37811  itg2addnclem3  37813  itg2gt0cn  37815  ftc1cnnclem  37831  ftc1anclem5  37837  cover2  37855  indexdom  37874  sdclem1  37883  fdc  37885  equivbnd2  37932  heiborlem8  37958  heibor  37961  isdrngo2  38098  iscringd  38138  smprngopr  38192  prnc  38207  eqbrtr  38373  eqeltr  38375  islfld  39261  lkrshpor  39306  lfl1dim  39320  lfl1dim2N  39321  cmtcomlemN  39447  2lplnmN  39758  pmapjat1  40052  trlnid  40378  tendoex  41174  dia1dimid  41262  dibval2  41343  dihmeetlem2N  41498  dochlkr  41584  mapdcv  41859  hdmaplkr  42112  hdmapip0  42114  hlhillcs  42157  aks6d1c6lem4  42366  dvdsexpnn  42530  readvrec  42559  frlmvscadiccat  42703  psrmnd  42740  nacsfix  42896  3rexfrabdioph  42981  4rexfrabdioph  42982  6rexfrabdioph  42983  7rexfrabdioph  42984  eldioph4b  42995  pellexlem2  43014  pellexlem5  43017  jm2.26lem3  43185  numinfctb  43287  ordne0gt0  43445  omge1  43481  omlim2  43483  omord2lim  43484  omord2i  43485  tfsconcatfv  43525  tfsconcatb0  43528  oaun3lem1  43558  ntrclsfv1  44238  ntrneifv1  44262  ntrneifv2  44263  cvgdvgrat  44496  radcnvrat  44497  dvconstbi  44517  bccbc  44528  elpwgded  44747  elpwgdedVD  45099  sspwimpcf  45102  sspwimpcfVD  45103  sspwimpALT2  45110  ax6e2ndeqALT  45113  eliuniin  45285  eliuniin2  45306  qinioo  45723  dfxlim2v  46033  xlimliminflimsup  46048  cncfiooicclem1  46079  ibliooicc  46157  stoweidlem27  46213  stoweidlem28  46214  fourierdlem89  46381  fourierdlem91  46383  fourierdlem92  46384  smflimmpt  46996  odz2prm2pw  47751  perfectALTVlem2  47910  blen1b  48776  naryfvalelfv  48820  itscnhlc0yqe  48947  itsclquadb  48964  lubeldm2  49143  glbeldm2  49144  ipolub  49175  ipoglb  49178  fucofulem1  49497  functhinclem1  49631  thincciso  49640  prsthinc  49651  functermclem  49694  prstchom2ALT  49751  onetansqsecsq  49948  cotsqcscsq  49949  aacllem  49988