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

Theorem biimpar 465
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 239 . 2 (𝜑 → (𝜒𝜓))
32imp 395 1 ((𝜑𝜒) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  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 198  df-an 385
This theorem is referenced by:  bitr  830  exbiri  836  oplem1  1072  eqtr  2832  opabss  4915  euotd  5175  brcogw  5499  somin1  5747  xpdifid  5780  funfni  6205  fnco  6213  fnssres  6218  fn0  6225  fnimadisj  6226  fnimaeq0  6227  foco  6344  foimacnv  6373  fvelimab  6477  dffv2  6495  fvopab3ig  6502  dff3  6597  dffo4  6600  fpr2g  6703  f1eqcocnv  6783  isomin  6814  f1ocnv2d  7119  fnexALT  7365  xp1st  7433  xp2nd  7434  wfr3g  7651  wfrlem3  7654  wfrlem4  7656  wfrlem4OLD  7657  iinon  7676  tfr3  7734  oawordri  7870  oaass  7881  omeulem1  7902  oeoa  7917  oeoe  7919  oeeulem  7921  ecelqsg  8040  elqsn0  8054  pwdom  8354  marypha1lem  8581  wofib  8692  cantnff  8821  cantnfp1  8828  cantnf  8840  cnfcomlem  8846  r1sscl  8898  rankval3b  8939  infxpidm2  9126  numdom  9147  onssnum  9149  acni  9154  acni2  9155  dfac5  9237  cdalepw  9306  infunsdom1  9323  infunsdom  9324  cofsmo  9379  cfsmolem  9380  fin1ai  9403  fin2i  9405  isf34lem1  9482  fin67  9505  itunisuc  9529  axdc3lem4  9563  zornn0g  9615  ttukeylem6  9624  brdom3  9638  tsken  9864  tskcard  9891  r1tskina  9892  intgru  9924  prlem934  10143  ltexprlem7  10152  supaddc  11278  mul2lt0rlt0  12149  xrmaxeq  12231  xrmineq  12232  xmulneg1  12320  ixxun  12412  difelfzle  12679  ssfzoulel  12789  elfznelfzo  12800  ico01fl0  12847  btwnzge0  12856  ltdifltdiv  12862  ioopnfsup  12890  icopnfsup  12891  modifeq2int  12959  suppssfz  13020  faclbnd4lem4  13306  hasheni  13359  hashgt0  13398  hashge1  13399  hashprb  13405  lennncl  13539  wrdsymb0  13553  ccatsymb  13582  ccatlid  13586  ccatass  13588  swrdid  13655  ccatswrd  13683  swrdccat2  13685  swrdccat  13720  revccat  13742  cnpart  14206  resqreu  14219  recval  14288  abs1m  14301  abslem2  14305  fzomaxdiflem  14308  sqreulem  14325  sqreu  14326  limsupgre  14438  rlimdiv  14602  fsumparts  14763  climcnds  14808  expcnv  14821  ntrivcvg  14853  mod2eq1n2dvds  15294  ndvdssub  15355  sadcaddlem  15401  rplpwr  15498  dvdssqlem  15501  algcvgblem  15512  eucalgcvga  15521  isprm2lem  15615  powm2modprm  15728  coprimeprodsq  15733  pythagtriplem11  15750  pythagtriplem13  15752  pcadd2  15814  4sqlem11  15879  vdwlem6  15910  vdwlem8  15912  vdwlem10  15914  ramval  15932  ramcl2  15940  ramlb  15943  ram0  15946  mreintcl  16463  mrcval  16478  mrccl  16479  mrcuni  16489  mrcun  16490  acsfiel  16522  rescabs  16700  funcres  16763  setcmon  16944  setcepi  16945  fullestrcsetc  16999  funcsetcestrclem8  17010  fullsetcestrc  17014  yonffthlem  17130  pleval2i  17172  pospo  17181  poslubdg  17357  acsdrsel  17375  acsdrscl  17378  acsficl  17379  psss  17422  grpidd  17476  ismndd  17521  gsumccat  17586  gsumwmhm  17590  mulgaddcom  17771  subgmulg  17813  resghm  17881  conjnsg  17901  f1otrspeq  18071  pmtrval  18075  pmtrrn  18081  pmtrfinv  18085  pmtrprfval  18111  psgnunilem1  18117  psgnunilem5  18118  psgnunilem4  18121  psgneldm2i  18129  lsmelvalix  18260  pj1ghm  18320  efgredlemc  18362  frgp0  18377  qusabl  18472  cycsubgcyg  18506  gsumval3  18512  gsumcllem  18513  ablfac1c  18675  pgpfac1lem5  18683  isringd  18790  lspsneq0b  19223  lmodindp1  19224  lmhmf1o  19256  lmhmpreima  19258  reslmhm  19262  pwssplit3  19271  lspsncmp  19326  lspsneq  19332  mpfind  19747  znf1o  20110  dsmmlss  20302  frlmlbs  20350  frlmup1  20351  mat1  20468  chfacfisf  20876  chfacfisfcpmat  20877  uniopn  20919  ntrval  21058  clsval  21059  neival  21124  neiptopreu  21155  lpval  21161  restdis  21200  lmbrf  21282  cnpnei  21286  1stcrest  21474  hauspwdom  21522  lfinpfin  21545  txcnpi  21629  ptrescn  21660  xkococnlem  21680  qtopeu  21737  kqreglem1  21762  ptuncnv  21828  filss  21874  fsubbas  21888  fbasrn  21905  cfinfil  21914  ufinffr  21950  elfm3  21971  rnelfmlem  21973  rnelfm  21974  flimclslem  22005  flfval  22011  isfcf  22055  cnextfvval  22086  cnextf  22087  cnextcn  22088  ustelimasn  22243  trust  22250  restutop  22258  ustuqtop2  22263  utop2nei  22271  ucncn  22306  trcfilu  22315  cnextucn  22324  met1stc  22543  metustexhalf  22578  cfilucfil  22581  psmetutop  22589  nmoix  22750  nmoeq0  22757  idnghm  22764  blcvx  22818  xrsxmet  22829  iccntr  22841  icccmp  22845  iihalf1  22947  iihalf2  22949  xrhmeo  22962  cnheibor  22971  ipcau2  23249  lmmbrf  23277  iscauf  23295  cmetcaulem  23303  bcthlem4  23341  cmetcusp  23367  rrxcph  23398  minveclem4  23421  evthicc2  23447  cniccbdd  23448  ovollb2  23476  ovolunlem1a  23483  ovolunlem1  23484  voliun  23541  icombl  23551  ioombl  23552  iccvolcl  23554  ioovolcl  23557  mbfss  23633  mbfposb  23640  itg2const2  23728  itg2splitlem  23735  itg2gt0  23747  iblss2  23792  itgioo  23802  dvaddf  23925  dvmulf  23926  dvcobr  23929  dvcof  23931  rolle  23973  dvlip  23976  c1lip1  23980  dvivthlem1  23991  lhop1lem  23996  dvfsumlem1  24009  ftc1lem4  24022  ftc1lem5  24023  ply1divmo  24115  coe1termlem  24234  plydiveu  24273  taylplem1  24337  pserulm  24396  abelth  24415  abscxp2  24659  abscxpbnd  24714  ang180lem2  24760  ang180lem3  24761  isosctrlem1  24768  angpieqvd  24778  atandmtan  24867  birthdaylem3  24900  wilthlem2  25015  wilthimp  25018  isppw  25060  isppw2  25061  dvdsflsumcom  25134  chteq0  25154  perfectlem2  25175  dchrval  25179  dchrinvcl  25198  dchrptlem1  25209  bposlem3  25231  lgslem4  25245  lgsmod  25268  lgsdilem  25269  lgsdir2lem2  25271  lgsdir2  25275  lgsne0  25280  lgsmulsqcoprm  25288  lgseisenlem1  25320  2lgsoddprm  25361  2sqlem4  25366  chpo1ubb  25390  dchrisumn0  25430  pntrsumbnd2  25476  ostthlem1  25536  ostth3  25547  idmot  25652  tgelrnln  25745  lmimid  25906  lmiisolem  25908  hypcgrlem1  25911  brcgr  26000  colinearalglem4  26009  colinearalg  26010  axlowdimlem14  26055  axcontlem4  26067  cplgrop  26567  lfgriswlk  26819  pthdlem1  26896  crctcshwlkn0  26948  wlknwwlksnsurOLD  27023  elwspths2on  27107  clwwlkgt0  27135  clwlkclwwlklem2fv2  27145  frgrncvvdeqlem9  27488  nvss  27782  sspn  27925  nmoub3i  27962  nmblolbii  27988  blocnilem  27993  minvecolem4  28070  htthlem  28108  norm1  28440  norm1exi  28441  pjeq  28592  axpjpj  28613  normcan  28769  pjoi0  28910  nmopub2tALT  29102  nmfnleub2  29119  eighmorth  29157  nmbdoplbi  29217  nmcoplbi  29221  nmophmi  29224  nmbdfnlbi  29242  nmcfnlbi  29245  riesz3i  29255  cnlnadjlem7  29266  branmfn  29298  nmopleid  29332  hstle  29423  superpos  29547  cvexchlem  29561  foresf1o  29674  elabreximd  29679  f1o3d  29764  fmptco1f1o  29767  funcnvmptOLD  29800  funcnvmpt  29801  fgreu  29804  resf1o  29838  fpwrelmap  29841  xrofsup  29866  eliccelico  29872  elicoelioo  29873  iocinif  29876  difioo  29877  eliccioo  29970  submomnd  30041  archirngz  30074  gsummpt2co  30111  ornglmullt  30138  orngrmullt  30139  pmtridf1o  30187  madjusmdetlem2  30225  qtophaus  30234  locfinreflem  30238  unitdivcld  30278  tpr2rico  30289  ordtrestNEW  30298  lmxrge0  30329  elzrhunit  30354  qqhf  30361  indf1ofs  30419  gsumesum  30452  esumfsup  30463  esumcvg  30479  issgon  30517  sigainb  30530  insiga  30531  isrnmeas  30594  measvunilem  30606  volmeas  30625  ddeval1  30628  ddeval0  30629  imambfm  30655  omssubadd  30693  carsgclctunlem3  30713  eulerpartlemf  30763  eulerpartlemgvv  30769  probun  30812  dstfrvunirn  30867  plymulx  30956  signslema  30970  signstfvn  30977  signsvtn0  30978  signstfvneq0  30980  signstres  30983  signstfveq0a  30984  breprexplemc  31041  logdivsqrle  31059  hgt750lemg  31063  tgoldbachgtda  31070  tgoldbachgt  31072  bnj529  31139  bnj548  31295  bnj570  31303  bnj852  31319  bnj929  31334  bnj1097  31377  bnj1118  31380  bnj1145  31389  derangen  31482  subfacp1lem2b  31491  subfacp1lem4  31493  subfacp1lem5  31494  derangfmla  31500  ptpconn  31543  mppspstlem  31796  wsuclem  32096  frr3g  32105  frrlem3  32108  nosupbnd2lem1  32187  nocvxmin  32220  colinearex  32493  btwnconn1lem11  32530  btwnconn1lem12  32531  fwddifnp1  32598  gtinfOLD  32640  nn0prpwlem  32643  bj-snmoore  33381  relowlpssretop  33530  fin2so  33711  matunitlindflem2  33721  ptrecube  33724  poimirlem8  33732  poimirlem13  33737  poimirlem15  33739  poimirlem24  33748  poimirlem25  33749  poimirlem26  33750  heicant  33759  mblfinlem2  33762  voliunnfl  33768  mbfresfi  33770  itg2addnclem  33775  itg2addnclem3  33777  itg2gt0cn  33779  ftc1cnnclem  33797  ftc1anclem5  33803  cover2  33822  indexdom  33843  sdclem1  33852  fdc  33854  equivbnd2  33904  heiborlem8  33930  heibor  33933  isdrngo2  34070  iscringd  34110  smprngopr  34164  prnc  34179  eqeltr  34324  islfld  34844  lkrshpor  34889  lfl1dim  34903  lfl1dim2N  34904  cmtcomlemN  35030  2lplnmN  35341  pmapjat1  35635  trlnid  35961  tendoex  36757  dia1dimid  36845  dibval2  36926  dihmeetlem2N  37081  dochlkr  37167  mapdcv  37442  hdmaplkr  37695  hdmapip0  37697  hlhillcs  37740  nacsfix  37778  3rexfrabdioph  37864  4rexfrabdioph  37865  6rexfrabdioph  37866  7rexfrabdioph  37867  eldioph4b  37878  pellexlem2  37897  pellexlem5  37900  expmordi  38014  jm2.26lem3  38070  numinfctb  38175  ntrclsfv1  38854  ntrneifv1  38878  ntrneifv2  38879  cvgdvgrat  39013  radcnvrat  39014  dvconstbi  39034  bccbc  39045  elpwgded  39279  elpwgdedVD  39648  sspwimpcf  39651  sspwimpcfVD  39652  sspwimpALT2  39659  ax6e2ndeqALT  39662  eliuniin  39773  eliuniin2  39796  qinioo  40243  dfxlim2v  40554  cncfiooicclem1  40587  ibliooicc  40667  stoweidlem27  40724  stoweidlem28  40725  fourierdlem89  40892  fourierdlem91  40894  fourierdlem92  40895  smflimmpt  41499  ccatpfx  41985  odz2prm2pw  42051  perfectALTVlem2  42207  blen1b  42951  onetansqsecsq  43074  cotsqcscsq  43075  aacllem  43119
  Copyright terms: Public domain W3C validator