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

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

This theorem is referenced by:  bitr  801  exbiri  807  oplem1  1049  eqtr  2816  opabss  5026  axprlem4  5218  axprlem5  5219  euotd  5294  brcogw  5625  somin1  5869  xpdifid  5901  funfni  6327  fnco  6335  fnssres  6340  fn0  6347  fnimadisj  6348  fnimaeq0  6349  foco  6470  foimacnv  6500  fvelimab  6605  dffv2  6623  fvopab3ig  6631  dff3  6729  dffo4  6732  fpr2g  6840  f1eqcocnv  6922  isomin  6953  f1ocnv2d  7256  fnexALT  7508  xp1st  7577  xp2nd  7578  wfr3g  7804  wfrlem3  7807  wfrlem4  7809  wfrlem4OLD  7810  iinon  7829  tfr3  7887  oawordri  8026  oaass  8037  omeulem1  8058  oeoa  8073  oeoe  8075  oeeulem  8077  ecelqsg  8202  elqsn0  8216  pwdom  8516  marypha1lem  8743  wofib  8855  cantnff  8983  cantnfp1  8990  cantnf  9002  cnfcomlem  9008  r1sscl  9060  rankval3b  9101  infxpidm2  9289  numdom  9310  onssnum  9312  acni  9317  acni2  9318  dfac5  9400  djulepw  9464  infunsdom1  9481  infunsdom  9482  cofsmo  9537  cfsmolem  9538  fin1ai  9561  fin2i  9563  isf34lem1  9640  fin67  9663  itunisuc  9687  axdc3lem4  9721  zornn0g  9773  ttukeylem6  9782  brdom3  9796  tsken  10022  tskcard  10049  r1tskina  10050  intgru  10082  prlem934  10301  ltexprlem7  10310  supaddc  11456  mul2lt0rlt0  12341  xrmaxeq  12422  xrmineq  12423  xmulneg1  12512  ixxun  12604  difelfzle  12870  ssfzoulel  12981  elfznelfzo  12992  ico01fl0  13039  btwnzge0  13048  ltdifltdiv  13054  ioopnfsup  13082  icopnfsup  13083  modifeq2int  13151  suppssfz  13212  expmordi  13381  faclbnd4lem4  13506  hasheni  13558  hashgt0  13597  hashge1  13598  hashprb  13606  lennncl  13730  wrdsymb0  13747  ccatsymb  13780  ccatlid  13784  ccatass  13786  ccatswrd  13866  swrdccat2  13867  ccatpfx  13899  swrdccat  13933  revccat  13964  cnpart  14433  resqreu  14446  recval  14516  abs1m  14529  abslem2  14533  fzomaxdiflem  14536  sqreulem  14553  sqreu  14554  limsupgre  14672  rlimdiv  14836  fsumparts  14994  climcnds  15039  expcnv  15052  ntrivcvg  15086  mod2eq1n2dvds  15529  ndvdssub  15593  sadcaddlem  15639  rplpwr  15736  dvdssqlem  15739  algcvgblem  15750  eucalgcvga  15759  isprm2lem  15854  powm2modprm  15969  coprimeprodsq  15974  pythagtriplem11  15991  pythagtriplem13  15993  pcadd2  16055  4sqlem11  16120  vdwlem6  16151  vdwlem8  16153  vdwlem10  16155  ramval  16173  ramcl2  16181  ramlb  16184  ram0  16187  mreintcl  16695  mrcval  16710  mrccl  16711  mrcuni  16721  mrcun  16722  acsfiel  16754  rescabs  16932  funcres  16995  setcmon  17176  setcepi  17177  fullestrcsetc  17230  funcsetcestrclem8  17241  fullsetcestrc  17245  yonffthlem  17361  pleval2i  17403  pospo  17412  poslubdg  17588  acsdrsel  17606  acsdrscl  17609  acsficl  17610  psss  17653  grpidd  17707  ismndd  17752  gsumccat  17817  gsumwmhm  17821  mulgaddcom  18005  subgmulg  18047  resghm  18115  conjnsg  18135  f1otrspeq  18306  pmtrval  18310  pmtrrn  18316  pmtrfinv  18320  pmtrprfval  18346  psgnunilem1  18352  psgnunilem5  18353  psgnunilem4  18356  psgneldm2i  18364  lsmelvalix  18496  pj1ghm  18556  efgredlemc  18598  frgp0  18613  qusabl  18708  cycsubgcyg  18742  gsumval3  18748  gsumcllem  18749  ablfac1c  18910  pgpfac1lem5  18918  isringd  19025  lspsneq0b  19475  lmodindp1  19476  lmhmf1o  19508  lmhmpreima  19510  reslmhm  19514  pwssplit3  19523  lspsncmp  19578  lspsneq  19584  rnasclassa  19811  mpfind  20003  mhplss  20025  znf1o  20380  dsmmlss  20570  frlmlbs  20623  frlmup1  20624  mat1  20740  chfacfisf  21146  chfacfisfcpmat  21147  uniopn  21189  ntrval  21328  clsval  21329  neival  21394  neiptopreu  21425  lpval  21431  restdis  21470  lmbrf  21552  cnpnei  21556  1stcrest  21745  hauspwdom  21793  lfinpfin  21816  txcnpi  21900  ptrescn  21931  xkococnlem  21951  qtopeu  22008  kqreglem1  22033  ptuncnv  22099  filss  22145  fsubbas  22159  fbasrn  22176  cfinfil  22185  ufinffr  22221  elfm3  22242  rnelfmlem  22244  rnelfm  22245  flimclslem  22276  flfval  22282  isfcf  22326  cnextfvval  22357  cnextf  22358  cnextcn  22359  ustelimasn  22514  trust  22521  restutop  22529  ustuqtop2  22534  utop2nei  22542  ucncn  22577  trcfilu  22586  cnextucn  22595  met1stc  22814  metustexhalf  22849  cfilucfil  22852  psmetutop  22860  nmoix  23021  nmoeq0  23028  idnghm  23035  blcvx  23089  xrsxmet  23100  iccntr  23112  icccmp  23116  iihalf1  23218  iihalf2  23220  xrhmeo  23233  cnheibor  23242  ipcau2  23520  lmmbrf  23548  iscauf  23566  cmetcaulem  23574  bcthlem4  23613  cmetcusp  23640  rrxcph  23678  minveclem4  23718  evthicc2  23744  cniccbdd  23745  ovollb2  23773  ovolunlem1a  23780  ovolunlem1  23781  voliun  23838  icombl  23848  ioombl  23849  iccvolcl  23851  ioovolcl  23854  mbfss  23930  mbfposb  23937  itg2const2  24025  itg2splitlem  24032  itg2gt0  24044  iblss2  24089  itgioo  24099  dvaddf  24222  dvmulf  24223  dvcobr  24226  dvcof  24228  rolle  24270  dvlip  24273  c1lip1  24277  dvivthlem1  24288  lhop1lem  24293  dvfsumlem1  24306  ftc1lem4  24319  ftc1lem5  24320  ply1divmo  24412  coe1termlem  24531  plydiveu  24570  taylplem1  24634  pserulm  24693  abelth  24712  abscxp2  24957  abscxpbnd  25015  logbgt0b  25052  ang180lem2  25069  ang180lem3  25070  isosctrlem1  25077  angpieqvd  25090  atandmtan  25179  birthdaylem3  25213  wilthlem2  25328  wilthimp  25331  isppw  25373  isppw2  25374  dvdsflsumcom  25447  chteq0  25467  perfectlem2  25488  dchrval  25492  dchrinvcl  25511  dchrptlem1  25522  bposlem3  25544  lgslem4  25558  lgsmod  25581  lgsdilem  25582  lgsdir2lem2  25584  lgsdir2  25588  lgsne0  25593  lgsmulsqcoprm  25601  lgseisenlem1  25633  2lgsoddprm  25674  2sqlem4  25679  chpo1ubb  25739  dchrisumn0  25779  pntrsumbnd2  25825  ostthlem1  25885  ostth3  25896  idmot  26005  tgelrnln  26098  lmimid  26262  lmiisolem  26264  hypcgrlem1  26267  brcgr  26369  colinearalglem4  26378  colinearalg  26379  axlowdimlem14  26424  axcontlem4  26436  cplgrop  26902  lfgriswlk  27155  pthdlem1  27234  crctcshwlkn0  27286  elwspths2on  27426  clwlkclwwlklem2fv2  27461  frgrncvvdeqlem9  27778  nvss  28061  sspn  28204  nmoub3i  28241  nmblolbii  28267  blocnilem  28272  minvecolem4  28348  htthlem  28385  norm1  28717  norm1exi  28718  pjeq  28867  axpjpj  28888  normcan  29044  pjoi0  29185  nmopub2tALT  29377  nmfnleub2  29394  eighmorth  29432  nmbdoplbi  29492  nmcoplbi  29496  nmophmi  29499  nmbdfnlbi  29517  nmcfnlbi  29520  riesz3i  29530  cnlnadjlem7  29541  branmfn  29573  nmopleid  29607  hstle  29698  superpos  29822  cvexchlem  29836  foresf1o  29957  elabreximd  29962  unidifsnne  29985  f1o3d  30062  fmptco1f1o  30068  funcnvmpt  30102  fgreu  30107  suppovss  30116  resf1o  30154  fpwrelmap  30157  xrofsup  30180  eliccelico  30188  elicoelioo  30189  iocinif  30192  difioo  30193  eliccioo  30291  cshf1o  30310  submomnd  30371  symgcom  30386  symgcom2  30387  odpmco  30389  pmtrcnel  30392  cyc3co2  30419  cycpmconjv  30421  tocyccntz  30423  cyc3evpm  30430  cycpmconjslem2  30435  cycpmconjs  30436  archirngz  30456  gsummpt2co  30495  ornglmullt  30534  orngrmullt  30535  lindssn  30585  linds2eq  30587  lbslsat  30618  lindsunlem  30624  lindsun  30625  dimkerim  30627  fedgmullem1  30629  fedgmullem2  30630  fedgmul  30631  pmtridf1o  30670  madjusmdetlem2  30708  qtophaus  30717  locfinreflem  30721  unitdivcld  30761  tpr2rico  30772  ordtrestNEW  30781  lmxrge0  30812  elzrhunit  30837  qqhf  30844  indf1ofs  30902  gsumesum  30935  esumfsup  30946  esumcvg  30962  issgon  30999  sigainb  31012  insiga  31013  isrnmeas  31076  measvunilem  31088  volmeas  31107  ddeval1  31110  ddeval0  31111  imambfm  31137  omssubadd  31175  carsgclctunlem3  31195  eulerpartlemf  31245  eulerpartlemgvv  31251  probun  31294  dstfrvunirn  31349  plymulx  31435  signslema  31449  signstfvn  31456  signsvtn0  31457  signstfvneq0  31459  signstres  31462  signstfveq0a  31463  breprexplemc  31520  logdivsqrle  31538  hgt750lemg  31542  tgoldbachgtda  31549  tgoldbachgt  31551  lpadmax  31570  lpadleft  31571  lpadright  31572  bnj529  31629  bnj548  31785  bnj570  31793  bnj852  31809  bnj929  31824  bnj1097  31867  bnj1118  31870  bnj1145  31879  funen1cnv  31971  spthcycl  31984  acycgr0v  32003  derangen  32027  subfacp1lem2b  32036  subfacp1lem4  32038  subfacp1lem5  32039  derangfmla  32045  ptpconn  32088  mppspstlem  32426  wsuclem  32721  frr3g  32730  frrlem3  32734  fpr2  32749  nosupbnd2lem1  32824  nocvxmin  32857  colinearex  33130  btwnconn1lem11  33167  btwnconn1lem12  33168  fwddifnp1  33235  nn0prpwlem  33279  bj-snmoore  34005  relowlpssretop  34176  fin2so  34410  matunitlindflem2  34420  ptrecube  34423  poimirlem8  34431  poimirlem13  34436  poimirlem15  34438  poimirlem24  34447  poimirlem25  34448  poimirlem26  34449  heicant  34458  mblfinlem2  34461  voliunnfl  34467  mbfresfi  34469  itg2addnclem  34474  itg2addnclem3  34476  itg2gt0cn  34478  ftc1cnnclem  34496  ftc1anclem5  34502  cover2  34521  indexdom  34541  sdclem1  34550  fdc  34552  equivbnd2  34602  heiborlem8  34628  heibor  34631  isdrngo2  34768  iscringd  34808  smprngopr  34862  prnc  34877  eqeltr  35033  islfld  35729  lkrshpor  35774  lfl1dim  35788  lfl1dim2N  35789  cmtcomlemN  35915  2lplnmN  36226  pmapjat1  36520  trlnid  36846  tendoex  37642  dia1dimid  37730  dibval2  37811  dihmeetlem2N  37966  dochlkr  38052  mapdcv  38327  hdmaplkr  38580  hdmapip0  38582  hlhillcs  38625  frlmvscadiccat  38672  nacsfix  38794  3rexfrabdioph  38879  4rexfrabdioph  38880  6rexfrabdioph  38881  7rexfrabdioph  38882  eldioph4b  38893  pellexlem2  38912  pellexlem5  38915  jm2.26lem3  39083  numinfctb  39188  ntrclsfv1  39890  ntrneifv1  39914  ntrneifv2  39915  cvgdvgrat  40183  radcnvrat  40184  dvconstbi  40204  bccbc  40215  elpwgded  40437  elpwgdedVD  40790  sspwimpcf  40793  sspwimpcfVD  40794  sspwimpALT2  40801  ax6e2ndeqALT  40804  eliuniin  40904  eliuniin2  40926  qinioo  41353  dfxlim2v  41670  xlimliminflimsup  41685  cncfiooicclem1  41717  ibliooicc  41797  stoweidlem27  41854  stoweidlem28  41855  fourierdlem89  42022  fourierdlem91  42024  fourierdlem92  42025  smflimmpt  42626  odz2prm2pw  43207  perfectALTVlem2  43369  blen1b  44129  itscnhlc0yqe  44227  itsclquadb  44244  onetansqsecsq  44340  cotsqcscsq  44341  aacllem  44382