Theorem biimpar 502

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  exbiri  652  bitr  745  oplem1  1007  eqtr  2641  opabss  4714  euotd  4975  brcogw  5290  somin1  5529  xpdifid  5562  funfni  5991  fnco  5999  fnssres  6004  fn0  6011  fnimadisj  6012  fnimaeq0  6013  foco  6125  foimacnv  6154  fvelimab  6253  dffv2  6271  fvopab3ig  6278  dff3  6372  dffo4  6375  fpr2g  6475  f1eqcocnv  6556  isomin  6587  f1ocnv2d  6886  fnexALT  7132  xp1st  7198  xp2nd  7199  wfr3g  7413  wfrlem3  7416  wfrlem4  7418  iinon  7437  tfr3  7495  oawordri  7630  oaass  7641  omeulem1  7662  oeoa  7677  oeoe  7679  oeeulem  7681  ecelqsg  7802  elqsn0  7816  pwdom  8112  marypha1lem  8339  wofib  8450  cantnff  8571  cantnfp1  8578  cantnf  8590  cnfcomlem  8596  r1sscl  8648  rankval3b  8689  infxpidm2  8840  numdom  8861  onssnum  8863  acni  8868  acni2  8869  dfac5  8951  cdalepw  9018  infunsdom1  9035  infunsdom  9036  cofsmo  9091  cfsmolem  9092  fin1ai  9115  fin2i  9117  isf34lem1  9194  fin67  9217  itunisuc  9241  axdc3lem4  9275  zornn0g  9327  ttukeylem6  9336  brdom3  9350  tsken  9576  tskcard  9603  r1tskina  9604  intgru  9636  prlem934  9855  ltexprlem7  9864  supaddc  10990  mul2lt0rlt0  11932  xrmaxeq  12010  xrmineq  12011  xmulneg1  12099  ixxun  12191  difelfzle  12452  ssfzoulel  12562  elfznelfzo  12573  ico01fl0  12620  btwnzge0  12629  ltdifltdiv  12635  ioopnfsup  12663  icopnfsup  12664  modifeq2int  12732  suppssfz  12794  faclbnd4lem4  13083  hasheni  13136  hashgt0  13177  hashge1  13178  hashprb  13185  lennncl  13325  wrdsymb0  13339  ccatsymb  13366  ccatlid  13369  ccatass  13371  swrdid  13428  ccatswrd  13456  swrdccat2  13458  swrdccat  13493  revccat  13515  cnpart  13980  resqreu  13993  recval  14062  abs1m  14075  abslem2  14079  fzomaxdiflem  14082  sqreulem  14099  sqreu  14100  limsupgre  14212  rlimdiv  14376  fsumparts  14538  climcnds  14583  expcnv  14596  ntrivcvg  14629  mod2eq1n2dvds  15071  ndvdssub  15133  sadcaddlem  15179  rplpwr  15276  dvdssqlem  15279  algcvgblem  15290  eucalgcvga  15299  isprm2lem  15394  powm2modprm  15508  coprimeprodsq  15513  pythagtriplem11  15530  pythagtriplem13  15532  pcadd2  15594  4sqlem11  15659  vdwlem6  15690  vdwlem8  15692  vdwlem10  15694  ramval  15712  ramcl2  15720  ramlb  15723  ram0  15726  mreintcl  16255  mrcval  16270  mrccl  16271  mrcuni  16281  mrcun  16282  acsfiel  16315  rescabs  16493  funcres  16556  setcmon  16737  setcepi  16738  fullestrcsetc  16791  funcsetcestrclem8  16802  fullsetcestrc  16806  yonffthlem  16922  pleval2i  16964  pospo  16973  poslubdg  17149  acsdrsel  17167  acsdrscl  17170  acsficl  17171  psss  17214  grpidd  17268  ismndd  17313  gsumccat  17378  gsumwmhm  17382  mulgaddcom  17564  subgmulg  17608  resghm  17676  conjnsg  17696  f1otrspeq  17867  pmtrval  17871  pmtrrn  17877  pmtrfinv  17881  pmtrprfval  17907  psgnunilem1  17913  psgnunilem5  17914  psgnunilem4  17917  psgneldm2i  17925  lsmelvalix  18056  pj1ghm  18116  efgredlemc  18158  frgp0  18173  qusabl  18268  cycsubgcyg  18302  gsumval3  18308  gsumcllem  18309  ablfac1c  18470  pgpfac1lem5  18478  isringd  18585  lspsneq0b  19013  lmodindp1  19014  lmhmf1o  19046  lmhmpreima  19048  reslmhm  19052  pwssplit3  19061  lspsncmp  19116  lspsneq  19122  mpfind  19536  znf1o  19900  dsmmlss  20088  frlmlbs  20136  frlmup1  20137  mat1  20253  chfacfisf  20659  chfacfisfcpmat  20660  uniopn  20702  ntrval  20840  clsval  20841  neival  20906  neiptopreu  20937  lpval  20943  restdis  20982  lmbrf  21064  cnpnei  21068  1stcrest  21256  hauspwdom  21304  lfinpfin  21327  txcnpi  21411  ptrescn  21442  xkococnlem  21462  qtopeu  21519  kqreglem1  21544  ptuncnv  21610  filss  21657  fsubbas  21671  fbasrn  21688  cfinfil  21697  ufinffr  21733  elfm3  21754  rnelfmlem  21756  rnelfm  21757  flimclslem  21788  flfval  21794  isfcf  21838  cnextfvval  21869  cnextf  21870  cnextcn  21871  ustelimasn  22026  trust  22033  restutop  22041  ustuqtop2  22046  utop2nei  22054  ucncn  22089  trcfilu  22098  cnextucn  22107  met1stc  22326  metustexhalf  22361  cfilucfil  22364  psmetutop  22372  nmoix  22533  nmoeq0  22540  idnghm  22547  blcvx  22601  xrsxmet  22612  iccntr  22624  icccmp  22628  iihalf1  22730  iihalf2  22732  xrhmeo  22745  cnheibor  22754  ipcau2  23033  lmmbrf  23060  iscauf  23078  cmetcaulem  23086  bcthlem4  23124  cmetcusp  23150  rrxcph  23180  minveclem4  23203  evthicc2  23229  cniccbdd  23230  ovollb2  23257  ovolunlem1a  23264  ovolunlem1  23265  voliun  23322  icombl  23332  ioombl  23333  iccvolcl  23335  ioovolcl  23338  mbfss  23413  mbfposb  23420  itg2const2  23508  itg2splitlem  23515  itg2gt0  23527  iblss2  23572  itgioo  23582  dvaddf  23705  dvmulf  23706  dvcobr  23709  dvcof  23711  rolle  23753  dvlip  23756  c1lip1  23760  dvivthlem1  23771  lhop1lem  23776  dvfsumlem1  23789  ftc1lem4  23802  ftc1lem5  23803  ply1divmo  23895  coe1termlem  24014  plydiveu  24053  taylplem1  24117  pserulm  24176  abelth  24195  abscxp2  24439  abscxpbnd  24494  ang180lem2  24540  ang180lem3  24541  isosctrlem1  24548  angpieqvd  24558  atandmtan  24647  birthdaylem3  24680  wilthlem2  24795  wilthimp  24798  isppw  24840  isppw2  24841  dvdsflsumcom  24914  chteq0  24934  perfectlem2  24955  dchrval  24959  dchrinvcl  24978  dchrptlem1  24989  bposlem3  25011  lgsmod  25048  lgsdilem  25049  lgsdir2lem2  25051  lgsdir2  25055  lgsne0  25060  lgsmulsqcoprm  25068  lgseisenlem1  25100  2lgsoddprm  25141  2sqlem4  25146  chpo1ubb  25170  dchrisumn0  25210  pntrsumbnd2  25256  ostthlem1  25316  ostth3  25327  idmot  25432  tgelrnln  25525  lmimid  25686  lmiisolem  25688  hypcgrlem1  25691  brcgr  25780  colinearalglem4  25789  colinearalg  25790  axlowdimlem14  25835  axcontlem4  25847  cplgrop  26333  lfgriswlk  26585  pthdlem1  26662  crctcshwlkn0  26713  wlknwwlksnsur  26776  elwspths2on  26853  clwlkclwwlklem2fv2  26897  clwwlksgt0  26906  frgrncvvdeqlem9  27171  nvss  27448  sspn  27591  nmoub3i  27628  nmblolbii  27654  blocnilem  27659  minvecolem4  27736  htthlem  27774  norm1  28106  norm1exi  28107  pjeq  28258  axpjpj  28279  normcan  28435  pjoi0  28576  nmopub2tALT  28768  nmfnleub2  28785  eighmorth  28823  nmbdoplbi  28883  nmcoplbi  28887  nmophmi  28890  nmbdfnlbi  28908  nmcfnlbi  28911  riesz3i  28921  cnlnadjlem7  28932  branmfn  28964  nmopleid  28998  hstle  29089  superpos  29213  cvexchlem  29227  foresf1o  29343  elabreximd  29348  f1o3d  29431  fmptco1f1o  29434  funcnvmptOLD  29467  funcnvmpt  29468  fgreu  29471  resf1o  29505  fpwrelmap  29508  xrofsup  29533  eliccelico  29539  elicoelioo  29540  iocinif  29543  difioo  29544  eliccioo  29639  submomnd  29710  archirngz  29743  gsummpt2co  29780  ornglmullt  29807  orngrmullt  29808  pmtridf1o  29856  madjusmdetlem2  29894  qtophaus  29903  locfinreflem  29907  unitdivcld  29947  tpr2rico  29958  ordtrestNEW  29967  lmxrge0  29998  elzrhunit  30023  qqhf  30030  indf1ofs  30088  gsumesum  30121  esumfsup  30132  esumcvg  30148  issgon  30186  sigainb  30199  insiga  30200  isrnmeas  30263  measvunilem  30275  volmeas  30294  ddeval1  30297  ddeval0  30298  imambfm  30324  omssubadd  30362  carsgclctunlem3  30382  eulerpartlemf  30432  eulerpartlemgvv  30438  probun  30481  dstfrvunirn  30536  plymulx  30625  signslema  30639  signstfvn  30646  signsvtn0  30647  signstfvneq0  30649  signstres  30652  signstfveq0a  30653  breprexplemc  30710  logdivsqrle  30728  hgt750lemg  30732  tgoldbachgtda  30739  tgoldbachgt  30741  bnj529  30811  bnj548  30967  bnj570  30975  bnj852  30991  bnj929  31006  bnj1097  31049  bnj1118  31052  bnj1145  31061  derangen  31154  subfacp1lem2b  31163  subfacp1lem4  31165  subfacp1lem5  31166  derangfmla  31172  ptpconn  31215  mppspstlem  31468  wsuclem  31773  wsuclemOLD  31774  frr3g  31779  frrlem3  31782  nosupbnd2lem1  31861  nocvxmin  31894  colinearex  32167  btwnconn1lem11  32204  btwnconn1lem12  32205  fwddifnp1  32272  gtinfOLD  32314  nn0prpwlem  32317  bj-snmoore  33068  relowlpssretop  33212  fin2so  33396  matunitlindflem2  33406  ptrecube  33409  poimirlem8  33417  poimirlem13  33422  poimirlem15  33424  poimirlem24  33433  poimirlem25  33434  poimirlem26  33435  heicant  33444  mblfinlem2  33447  voliunnfl  33453  mbfresfi  33456  itg2addnclem  33461  itg2addnclem3  33463  itg2gt0cn  33465  ftc1cnnclem  33483  ftc1anclem5  33489  cover2  33508  indexdom  33529  sdclem1  33539  fdc  33541  equivbnd2  33591  heiborlem8  33617  heibor  33620  isdrngo2  33757  iscringd  33797  smprngopr  33851  prnc  33866  eqeltr  34001  islfld  34349  lkrshpor  34394  lfl1dim  34408  lfl1dim2N  34409  cmtcomlemN  34535  2lplnmN  34845  pmapjat1  35139  trlnid  35466  tendoex  36263  dia1dimid  36352  dibval2  36433  dihmeetlem2N  36588  dochlkr  36674  mapdcv  36949  hdmaplkr  37205  hdmapip0  37207  hlhillcs  37250  nacsfix  37275  3rexfrabdioph  37361  4rexfrabdioph  37362  6rexfrabdioph  37363  7rexfrabdioph  37364  eldioph4b  37375  pellexlem2  37394  pellexlem5  37397  expmordi  37512  jm2.26lem3  37568  numinfctb  37673  ntrclsfv1  38353  ntrneifv1  38377  ntrneifv2  38378  cvgdvgrat  38512  radcnvrat  38513  dvconstbi  38533  bccbc  38544  elpwgded  38780  elpwgdedVD  39153  sspwimpcf  39156  sspwimpcfVD  39157  sspwimpALT2  39164  ax6e2ndeqALT  39167  eliuniin  39279  eliuniin2  39303  qinioo  39762  dfxlim2v  40073  cncfiooicclem1  40106  ibliooicc  40187  stoweidlem27  40244  stoweidlem28  40245  fourierdlem89  40412  fourierdlem91  40414  fourierdlem92  40415  smflimmpt  41016  ccatpfx  41409  odz2prm2pw  41475  perfectALTVlem2  41631  blen1b  42382  onetansqsecsq  42502  cotsqcscsq  42503  aacllem  42547