MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  biimpar Structured version   Visualization version   GIF version

Theorem biimpar 479
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
StepHypRef Expression
1 biimpa.1 . . 3 (𝜑 → (𝜓𝜒))
21biimprd 248 . 2 (𝜑 → (𝜒𝜓))
32imp 408 1 ((𝜑𝜒) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397
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 398
This theorem is referenced by:  bitr  804  exbiri  810  biadanid  822  oplem1  1056  eqtr  2760  pm13.181  3027  opabss  5170  axprlem4  5382  axprlem5  5383  euotd  5471  brcogw  5825  somin1  6088  xpdifid  6121  funfni  6609  fncoOLD  6620  fnssres  6625  fn0  6633  fnimadisj  6634  fnimaeq0  6635  foimacnv  6802  fvelimab  6915  dffv2  6937  fvopab3ig  6945  dff3  7051  dffo4  7054  fpr2g  7162  f1eqcocnv  7248  f1eqcocnvOLD  7249  isomin  7283  f1ocnv2d  7607  fnexALT  7884  xp1st  7954  xp2nd  7955  frrlem3  8220  fpr2  8236  wfr3g  8254  wfrlem3OLD  8257  wfrlem4OLD  8259  wfr2  8283  iinon  8287  tfr3  8346  oawordri  8498  oaass  8509  omeulem1  8530  oeoa  8545  oeoe  8547  oeeulem  8549  ecelqsg  8712  elqsn0  8726  pwdom  9074  enfii  9134  phpeqd  9160  ominf  9203  findcard3  9230  marypha1lem  9370  wofib  9482  cantnff  9611  cantnfp1  9618  cantnf  9630  cnfcomlem  9636  ttrcltr  9653  frr3g  9693  r1sscl  9722  rankval3b  9763  infxpidm2  9954  numdom  9975  onssnum  9977  acni  9982  acni2  9983  dfac5  10065  djulepw  10129  infunsdom1  10150  infunsdom  10151  cofsmo  10206  cfsmolem  10207  fin1ai  10230  fin2i  10232  isf34lem1  10309  fin67  10332  itunisuc  10356  axdc3lem4  10390  zornn0g  10442  ttukeylem6  10451  brdom3  10465  tsken  10691  tskcard  10718  r1tskina  10719  intgru  10751  prlem934  10970  ltexprlem7  10979  supaddc  12123  mul2lt0rlt0  13018  xrmaxeq  13099  xrmineq  13100  xmulneg1  13189  ixxun  13281  difelfzle  13555  ssfzoulel  13667  elfznelfzo  13678  ico01fl0  13725  btwnzge0  13734  ltdifltdiv  13740  ioopnfsup  13770  icopnfsup  13771  modifeq2int  13839  suppssfz  13900  expmordi  14073  zzlesq  14111  faclbnd4lem4  14197  hasheni  14249  hashgt0  14289  hashge1  14290  hashprb  14298  lennncl  14423  wrdsymb0  14438  ccatsymb  14471  ccatlid  14475  ccatass  14477  ccatswrd  14557  swrdccat2  14558  ccatpfx  14590  swrdccatfn  14613  swrdccat  14624  revccat  14655  2cshw  14702  cnpart  15126  resqreu  15138  recval  15208  abs1m  15221  abslem2  15225  fzomaxdiflem  15228  sqreulem  15245  sqreu  15246  limsupgre  15364  rlimdiv  15531  fsumparts  15692  climcnds  15737  expcnv  15750  ntrivcvg  15783  mod2eq1n2dvds  16230  ndvdssub  16292  sadcaddlem  16338  rplpwr  16439  dvdssqlem  16443  algcvgblem  16454  eucalgcvga  16463  isprm2lem  16558  powm2modprm  16676  coprimeprodsq  16681  pythagtriplem11  16698  pythagtriplem13  16700  pcadd2  16763  4sqlem11  16828  vdwlem6  16859  vdwlem8  16861  vdwlem10  16863  ramval  16881  ramcl2  16889  ramlb  16892  ram0  16895  mreintcl  17476  mrcval  17491  mrccl  17492  mrcuni  17502  mrcun  17503  acsfiel  17535  rescabs  17719  rescabsOLD  17720  funcres  17783  setcmon  17974  setcepi  17975  fullestrcsetc  18040  funcsetcestrclem8  18051  fullsetcestrc  18055  yonffthlem  18172  pleval2i  18226  pospo  18235  poslubdg  18304  acsdrsel  18433  acsdrscl  18436  acsficl  18437  psss  18470  grpidd  18527  ismndd  18579  gsumsgrpccat  18651  gsumwmhm  18656  mulgaddcom  18901  subgmulg  18943  resghm  19025  conjnsg  19045  f1otrspeq  19230  pmtrval  19234  pmtrrn  19240  pmtrfinv  19244  pmtrprfval  19270  psgnunilem1  19276  psgnunilem5  19277  psgnunilem4  19280  psgneldm2i  19288  lsmelvalix  19424  pj1ghm  19486  efgredlemc  19528  frgp0  19543  qusabl  19644  cycsubgcyg  19679  gsumval3  19685  gsumcllem  19686  ablfac1c  19851  pgpfac1lem5  19859  isringd  20010  lspsneq0b  20477  lmodindp1  20478  lmhmf1o  20510  lmhmpreima  20512  reslmhm  20516  pwssplit3  20525  lspsncmp  20580  lspsneq  20586  znf1o  20961  dsmmlss  21153  frlmlbs  21206  frlmup1  21207  psrgrp  21369  mpfind  21520  mhplss  21548  mat1  21799  chfacfisf  22206  chfacfisfcpmat  22207  uniopn  22249  ntrval  22390  clsval  22391  neival  22456  neiptopreu  22487  lpval  22493  restdis  22532  lmbrf  22614  cnpnei  22618  1stcrest  22807  hauspwdom  22855  lfinpfin  22878  txcnpi  22962  ptrescn  22993  xkococnlem  23013  qtopeu  23070  kqreglem1  23095  ptuncnv  23161  filss  23207  fsubbas  23221  fbasrn  23238  cfinfil  23247  ufinffr  23283  elfm3  23304  rnelfmlem  23306  rnelfm  23307  flimclslem  23338  flfval  23344  isfcf  23388  cnextfvval  23419  cnextf  23420  cnextcn  23421  ustelimasn  23577  trust  23584  restutop  23592  ustuqtop2  23597  utop2nei  23605  ucncn  23640  trcfilu  23649  cnextucn  23658  met1stc  23880  metustexhalf  23915  cfilucfil  23918  psmetutop  23926  nmoix  24096  nmoeq0  24103  idnghm  24110  blcvx  24164  xrsxmet  24175  iccntr  24187  icccmp  24191  iihalf1  24297  iihalf2  24299  xrhmeo  24312  cnheibor  24321  ipcau2  24601  lmmbrf  24629  iscauf  24647  cmetcaulem  24655  bcthlem4  24694  cmetcusp  24721  rrxcph  24759  minveclem4  24799  evthicc2  24827  cniccbdd  24828  ovollb2  24856  ovolunlem1a  24863  ovolunlem1  24864  voliun  24921  icombl  24931  ioombl  24932  iccvolcl  24934  ioovolcl  24937  mbfss  25013  mbfposb  25020  itg2const2  25109  itg2splitlem  25116  itg2gt0  25128  iblss2  25173  itgioo  25183  dvaddf  25309  dvmulf  25310  dvcobr  25313  dvcof  25315  rolle  25357  dvlip  25360  c1lip1  25364  dvivthlem1  25375  lhop1lem  25380  dvfsumlem1  25393  ftc1lem4  25406  ftc1lem5  25407  ply1divmo  25503  coe1termlem  25622  plydiveu  25661  taylplem1  25725  pserulm  25784  abelth  25803  abscxp2  26051  abscxpbnd  26109  logbgt0b  26146  ang180lem2  26163  ang180lem3  26164  isosctrlem1  26171  angpieqvd  26184  atandmtan  26273  birthdaylem3  26306  wilthlem2  26421  wilthimp  26424  isppw  26466  isppw2  26467  dvdsflsumcom  26540  chteq0  26560  perfectlem2  26581  dchrval  26585  dchrinvcl  26604  dchrptlem1  26615  bposlem3  26637  lgslem4  26651  lgsmod  26674  lgsdilem  26675  lgsdir2lem2  26677  lgsdir2  26681  lgsne0  26686  lgsmulsqcoprm  26694  lgseisenlem1  26726  2lgsoddprm  26767  2sqlem4  26772  chpo1ubb  26832  dchrisumn0  26872  pntrsumbnd2  26918  ostthlem1  26978  ostth3  26989  nosupbnd2lem1  27066  noinfbnd2lem1  27081  nocvxmin  27121  eqscut2  27148  sltlpss  27239  idmot  27482  tgelrnln  27575  lmimid  27739  lmiisolem  27741  hypcgrlem1  27744  brcgr  27852  colinearalglem4  27861  colinearalg  27862  axlowdimlem14  27907  axcontlem4  27919  cplgrop  28388  lfgriswlk  28639  pthdlem1  28717  crctcshwlkn0  28769  elwspths2on  28908  clwlkclwwlklem2fv2  28943  frgrncvvdeqlem9  29254  nvss  29538  sspn  29681  nmoub3i  29718  nmblolbii  29744  blocnilem  29749  minvecolem4  29825  htthlem  29862  norm1  30194  norm1exi  30195  pjeq  30344  axpjpj  30365  normcan  30521  pjoi0  30662  nmopub2tALT  30854  nmfnleub2  30871  eighmorth  30909  nmbdoplbi  30969  nmcoplbi  30973  nmophmi  30976  nmbdfnlbi  30994  nmcfnlbi  30997  riesz3i  31007  cnlnadjlem7  31018  branmfn  31050  nmopleid  31084  hstle  31175  superpos  31299  cvexchlem  31313  foresf1o  31434  elabreximd  31439  unidifsnne  31466  f1o3d  31544  fmptco1f1o  31550  funcnvmpt  31586  fgreu  31591  suppovss  31601  fsupprnfi  31610  resf1o  31650  fpwrelmap  31653  xrofsup  31675  eliccelico  31683  elicoelioo  31684  iocinif  31687  difioo  31688  eliccioo  31790  cshf1o  31819  mgcmnt1d  31860  mgcmnt2d  31861  pwrssmgc  31863  gsummpt2co  31893  gsumhashmul  31901  submomnd  31921  symgcom  31937  symgcom2  31938  odpmco  31940  pmtrcnel  31943  pmtridf1o  31946  cycpmco2lem6  31983  cycpmco2lem7  31984  cycpmco2  31985  cyc3co2  31992  cycpmconjv  31994  tocyccntz  31996  cyc3evpm  32002  cycpmconjslem2  32007  cycpmconjs  32008  archirngz  32028  sdrgdvcl  32079  sdrginvcl  32080  ornglmullt  32105  orngrmullt  32106  lindssn  32169  linds2eq  32171  nsgqusf1olem1  32194  nsgqusf1olem3  32196  ghmqusker  32201  elrspunidl  32206  rhmimaidl  32209  prmidl2  32216  prmidl0  32226  qsidomlem1  32228  ssmxidl  32242  ply1scleq  32269  lbslsat  32316  lindsunlem  32322  lindsun  32323  dimkerim  32325  fedgmullem1  32327  fedgmullem2  32328  fedgmul  32329  irngss  32364  0ringirng  32366  irngnzply1  32368  madjusmdetlem2  32412  qtophaus  32420  locfinreflem  32424  zarclssn  32457  zarmxt1  32464  zarcmplem  32465  rhmpreimacn  32469  unitdivcld  32485  tpr2rico  32496  ordtrestNEW  32505  lmxrge0  32536  elzrhunit  32563  qqhf  32570  indf1ofs  32628  gsumesum  32661  esumfsup  32672  esumcvg  32688  issgon  32725  sigainb  32738  insiga  32739  isrnmeas  32802  measvunilem  32814  volmeas  32833  ddeval1  32836  ddeval0  32837  imambfm  32865  omssubadd  32903  carsgclctunlem3  32923  eulerpartlemf  32973  eulerpartlemgvv  32979  probun  33022  dstfrvunirn  33077  plymulx  33163  signslema  33177  signstfvn  33184  signsvtn0  33185  signstfvneq0  33187  signstres  33190  signstfveq0a  33191  breprexplemc  33248  logdivsqrle  33266  hgt750lemg  33270  tgoldbachgtda  33277  tgoldbachgt  33279  lpadmax  33298  lpadleft  33299  lpadright  33300  bnj529  33356  bnj548  33512  bnj570  33520  bnj852  33536  bnj929  33551  bnj1097  33596  bnj1118  33599  bnj1145  33608  funen1cnv  33695  spthcycl  33726  acycgr0v  33745  derangen  33769  subfacp1lem2b  33778  subfacp1lem4  33780  subfacp1lem5  33781  derangfmla  33787  ptpconn  33830  mppspstlem  34168  wsuclem  34403  colinearex  34648  btwnconn1lem11  34685  btwnconn1lem12  34686  fwddifnp1  34753  nn0prpwlem  34797  bj-snmoore  35587  bj-imdiridlem  35659  relowlpssretop  35838  fin2so  36068  matunitlindflem2  36078  ptrecube  36081  poimirlem8  36089  poimirlem13  36094  poimirlem15  36096  poimirlem24  36105  poimirlem25  36106  poimirlem26  36107  heicant  36116  mblfinlem2  36119  voliunnfl  36125  mbfresfi  36127  itg2addnclem  36132  itg2addnclem3  36134  itg2gt0cn  36136  ftc1cnnclem  36152  ftc1anclem5  36158  cover2  36176  indexdom  36196  sdclem1  36205  fdc  36207  equivbnd2  36254  heiborlem8  36280  heibor  36283  isdrngo2  36420  iscringd  36460  smprngopr  36514  prnc  36529  eqbrtr  36692  eqeltr  36694  islfld  37527  lkrshpor  37572  lfl1dim  37586  lfl1dim2N  37587  cmtcomlemN  37713  2lplnmN  38025  pmapjat1  38319  trlnid  38645  tendoex  39441  dia1dimid  39529  dibval2  39610  dihmeetlem2N  39765  dochlkr  39851  mapdcv  40126  hdmaplkr  40379  hdmapip0  40381  hlhillcs  40428  frlmvscadiccat  40684  mhphf  40774  dvdsexpnn  40829  nacsfix  41038  3rexfrabdioph  41123  4rexfrabdioph  41124  6rexfrabdioph  41125  7rexfrabdioph  41126  eldioph4b  41137  pellexlem2  41156  pellexlem5  41159  jm2.26lem3  41328  numinfctb  41433  ordne0gt0  41599  omge1  41634  omlim2  41636  omord2lim  41637  omord2i  41638  ntrclsfv1  42334  ntrneifv1  42358  ntrneifv2  42359  cvgdvgrat  42600  radcnvrat  42601  dvconstbi  42621  bccbc  42632  elpwgded  42853  elpwgdedVD  43206  sspwimpcf  43209  sspwimpcfVD  43210  sspwimpALT2  43217  ax6e2ndeqALT  43220  eliuniin  43316  eliuniin2  43337  qinioo  43780  dfxlim2v  44095  xlimliminflimsup  44110  cncfiooicclem1  44141  ibliooicc  44219  stoweidlem27  44275  stoweidlem28  44276  fourierdlem89  44443  fourierdlem91  44445  fourierdlem92  44446  smflimmpt  45058  odz2prm2pw  45762  perfectALTVlem2  45921  blen1b  46681  naryfvalelfv  46725  itscnhlc0yqe  46852  itsclquadb  46869  lubeldm2  46996  glbeldm2  46997  ipolub  47020  ipoglb  47023  functhinclem1  47068  thincciso  47076  prsthinc  47081  prstchom2ALT  47106  onetansqsecsq  47213  cotsqcscsq  47214  aacllem  47255
  Copyright terms: Public domain W3C validator