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

Theorem biimpar 501
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 238 . 2 (𝜑 → (𝜒𝜓))
32imp 444 1 ((𝜑𝜒) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383
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 385
This theorem is referenced by:  exbiri  651  bitr  745  oplem1  1027  eqtr  2670  opabss  4747  euotd  5004  brcogw  5323  somin1  5564  xpdifid  5597  funfni  6029  fnco  6037  fnssres  6042  fn0  6049  fnimadisj  6050  fnimaeq0  6051  foco  6163  foimacnv  6192  fvelimab  6292  dffv2  6310  fvopab3ig  6317  dff3  6412  dffo4  6415  fpr2g  6516  f1eqcocnv  6596  isomin  6627  f1ocnv2d  6928  fnexALT  7174  xp1st  7242  xp2nd  7243  wfr3g  7458  wfrlem3  7461  wfrlem4  7463  iinon  7482  tfr3  7540  oawordri  7675  oaass  7686  omeulem1  7707  oeoa  7722  oeoe  7724  oeeulem  7726  ecelqsg  7845  elqsn0  7859  pwdom  8153  marypha1lem  8380  wofib  8491  cantnff  8609  cantnfp1  8616  cantnf  8628  cnfcomlem  8634  r1sscl  8686  rankval3b  8727  infxpidm2  8878  numdom  8899  onssnum  8901  acni  8906  acni2  8907  dfac5  8989  cdalepw  9056  infunsdom1  9073  infunsdom  9074  cofsmo  9129  cfsmolem  9130  fin1ai  9153  fin2i  9155  isf34lem1  9232  fin67  9255  itunisuc  9279  axdc3lem4  9313  zornn0g  9365  ttukeylem6  9374  brdom3  9388  tsken  9614  tskcard  9641  r1tskina  9642  intgru  9674  prlem934  9893  ltexprlem7  9902  supaddc  11028  mul2lt0rlt0  11970  xrmaxeq  12048  xrmineq  12049  xmulneg1  12137  ixxun  12229  difelfzle  12491  ssfzoulel  12602  elfznelfzo  12613  ico01fl0  12660  btwnzge0  12669  ltdifltdiv  12675  ioopnfsup  12703  icopnfsup  12704  modifeq2int  12772  suppssfz  12834  faclbnd4lem4  13123  hasheni  13176  hashgt0  13215  hashge1  13216  hashprb  13223  lennncl  13357  wrdsymb0  13371  ccatsymb  13400  ccatlid  13404  ccatass  13406  swrdid  13474  ccatswrd  13502  swrdccat2  13504  swrdccat  13539  revccat  13561  cnpart  14024  resqreu  14037  recval  14106  abs1m  14119  abslem2  14123  fzomaxdiflem  14126  sqreulem  14143  sqreu  14144  limsupgre  14256  rlimdiv  14420  fsumparts  14582  climcnds  14627  expcnv  14640  ntrivcvg  14673  mod2eq1n2dvds  15118  ndvdssub  15180  sadcaddlem  15226  rplpwr  15323  dvdssqlem  15326  algcvgblem  15337  eucalgcvga  15346  isprm2lem  15441  powm2modprm  15555  coprimeprodsq  15560  pythagtriplem11  15577  pythagtriplem13  15579  pcadd2  15641  4sqlem11  15706  vdwlem6  15737  vdwlem8  15739  vdwlem10  15741  ramval  15759  ramcl2  15767  ramlb  15770  ram0  15773  mreintcl  16302  mrcval  16317  mrccl  16318  mrcuni  16328  mrcun  16329  acsfiel  16362  rescabs  16540  funcres  16603  setcmon  16784  setcepi  16785  fullestrcsetc  16838  funcsetcestrclem8  16849  fullsetcestrc  16853  yonffthlem  16969  pleval2i  17011  pospo  17020  poslubdg  17196  acsdrsel  17214  acsdrscl  17217  acsficl  17218  psss  17261  grpidd  17315  ismndd  17360  gsumccat  17425  gsumwmhm  17429  mulgaddcom  17611  subgmulg  17655  resghm  17723  conjnsg  17743  f1otrspeq  17913  pmtrval  17917  pmtrrn  17923  pmtrfinv  17927  pmtrprfval  17953  psgnunilem1  17959  psgnunilem5  17960  psgnunilem4  17963  psgneldm2i  17971  lsmelvalix  18102  pj1ghm  18162  efgredlemc  18204  frgp0  18219  qusabl  18314  cycsubgcyg  18348  gsumval3  18354  gsumcllem  18355  ablfac1c  18516  pgpfac1lem5  18524  isringd  18631  lspsneq0b  19061  lmodindp1  19062  lmhmf1o  19094  lmhmpreima  19096  reslmhm  19100  pwssplit3  19109  lspsncmp  19164  lspsneq  19170  mpfind  19584  znf1o  19948  dsmmlss  20136  frlmlbs  20184  frlmup1  20185  mat1  20301  chfacfisf  20707  chfacfisfcpmat  20708  uniopn  20750  ntrval  20888  clsval  20889  neival  20954  neiptopreu  20985  lpval  20991  restdis  21030  lmbrf  21112  cnpnei  21116  1stcrest  21304  hauspwdom  21352  lfinpfin  21375  txcnpi  21459  ptrescn  21490  xkococnlem  21510  qtopeu  21567  kqreglem1  21592  ptuncnv  21658  filss  21704  fsubbas  21718  fbasrn  21735  cfinfil  21744  ufinffr  21780  elfm3  21801  rnelfmlem  21803  rnelfm  21804  flimclslem  21835  flfval  21841  isfcf  21885  cnextfvval  21916  cnextf  21917  cnextcn  21918  ustelimasn  22073  trust  22080  restutop  22088  ustuqtop2  22093  utop2nei  22101  ucncn  22136  trcfilu  22145  cnextucn  22154  met1stc  22373  metustexhalf  22408  cfilucfil  22411  psmetutop  22419  nmoix  22580  nmoeq0  22587  idnghm  22594  blcvx  22648  xrsxmet  22659  iccntr  22671  icccmp  22675  iihalf1  22777  iihalf2  22779  xrhmeo  22792  cnheibor  22801  ipcau2  23079  lmmbrf  23106  iscauf  23124  cmetcaulem  23132  bcthlem4  23170  cmetcusp  23196  rrxcph  23226  minveclem4  23249  evthicc2  23275  cniccbdd  23276  ovollb2  23303  ovolunlem1a  23310  ovolunlem1  23311  voliun  23368  icombl  23378  ioombl  23379  iccvolcl  23381  ioovolcl  23384  mbfss  23458  mbfposb  23465  itg2const2  23553  itg2splitlem  23560  itg2gt0  23572  iblss2  23617  itgioo  23627  dvaddf  23750  dvmulf  23751  dvcobr  23754  dvcof  23756  rolle  23798  dvlip  23801  c1lip1  23805  dvivthlem1  23816  lhop1lem  23821  dvfsumlem1  23834  ftc1lem4  23847  ftc1lem5  23848  ply1divmo  23940  coe1termlem  24059  plydiveu  24098  taylplem1  24162  pserulm  24221  abelth  24240  abscxp2  24484  abscxpbnd  24539  ang180lem2  24585  ang180lem3  24586  isosctrlem1  24593  angpieqvd  24603  atandmtan  24692  birthdaylem3  24725  wilthlem2  24840  wilthimp  24843  isppw  24885  isppw2  24886  dvdsflsumcom  24959  chteq0  24979  perfectlem2  25000  dchrval  25004  dchrinvcl  25023  dchrptlem1  25034  bposlem3  25056  lgslem4  25070  lgsmod  25093  lgsdilem  25094  lgsdir2lem2  25096  lgsdir2  25100  lgsne0  25105  lgsmulsqcoprm  25113  lgseisenlem1  25145  2lgsoddprm  25186  2sqlem4  25191  chpo1ubb  25215  dchrisumn0  25255  pntrsumbnd2  25301  ostthlem1  25361  ostth3  25372  idmot  25477  tgelrnln  25570  lmimid  25731  lmiisolem  25733  hypcgrlem1  25736  brcgr  25825  colinearalglem4  25834  colinearalg  25835  axlowdimlem14  25880  axcontlem4  25892  cplgrop  26389  lfgriswlk  26641  pthdlem1  26718  crctcshwlkn0  26769  wlknwwlksnsur  26844  elwspths2on  26926  clwwlkgt0  26954  clwlkclwwlklem2fv2  26962  frgrncvvdeqlem9  27287  nvss  27576  sspn  27719  nmoub3i  27756  nmblolbii  27782  blocnilem  27787  minvecolem4  27864  htthlem  27902  norm1  28234  norm1exi  28235  pjeq  28386  axpjpj  28407  normcan  28563  pjoi0  28704  nmopub2tALT  28896  nmfnleub2  28913  eighmorth  28951  nmbdoplbi  29011  nmcoplbi  29015  nmophmi  29018  nmbdfnlbi  29036  nmcfnlbi  29039  riesz3i  29049  cnlnadjlem7  29060  branmfn  29092  nmopleid  29126  hstle  29217  superpos  29341  cvexchlem  29355  foresf1o  29469  elabreximd  29474  f1o3d  29559  fmptco1f1o  29562  funcnvmptOLD  29595  funcnvmpt  29596  fgreu  29599  resf1o  29633  fpwrelmap  29636  xrofsup  29661  eliccelico  29667  elicoelioo  29668  iocinif  29671  difioo  29672  eliccioo  29767  submomnd  29838  archirngz  29871  gsummpt2co  29908  ornglmullt  29935  orngrmullt  29936  pmtridf1o  29984  madjusmdetlem2  30022  qtophaus  30031  locfinreflem  30035  unitdivcld  30075  tpr2rico  30086  ordtrestNEW  30095  lmxrge0  30126  elzrhunit  30151  qqhf  30158  indf1ofs  30216  gsumesum  30249  esumfsup  30260  esumcvg  30276  issgon  30314  sigainb  30327  insiga  30328  isrnmeas  30391  measvunilem  30403  volmeas  30422  ddeval1  30425  ddeval0  30426  imambfm  30452  omssubadd  30490  carsgclctunlem3  30510  eulerpartlemf  30560  eulerpartlemgvv  30566  probun  30609  dstfrvunirn  30664  plymulx  30753  signslema  30767  signstfvn  30774  signsvtn0  30775  signstfvneq0  30777  signstres  30780  signstfveq0a  30781  breprexplemc  30838  logdivsqrle  30856  hgt750lemg  30860  tgoldbachgtda  30867  tgoldbachgt  30869  bnj529  30937  bnj548  31093  bnj570  31101  bnj852  31117  bnj929  31132  bnj1097  31175  bnj1118  31178  bnj1145  31187  derangen  31280  subfacp1lem2b  31289  subfacp1lem4  31291  subfacp1lem5  31292  derangfmla  31298  ptpconn  31341  mppspstlem  31594  wsuclem  31895  frr3g  31904  frrlem3  31907  nosupbnd2lem1  31986  nocvxmin  32019  colinearex  32292  btwnconn1lem11  32329  btwnconn1lem12  32330  fwddifnp1  32397  gtinfOLD  32439  nn0prpwlem  32442  bj-snmoore  33193  relowlpssretop  33342  fin2so  33526  matunitlindflem2  33536  ptrecube  33539  poimirlem8  33547  poimirlem13  33552  poimirlem15  33554  poimirlem24  33563  poimirlem25  33564  poimirlem26  33565  heicant  33574  mblfinlem2  33577  voliunnfl  33583  mbfresfi  33586  itg2addnclem  33591  itg2addnclem3  33593  itg2gt0cn  33595  ftc1cnnclem  33613  ftc1anclem5  33619  cover2  33638  indexdom  33659  sdclem1  33669  fdc  33671  equivbnd2  33721  heiborlem8  33747  heibor  33750  isdrngo2  33887  iscringd  33927  smprngopr  33981  prnc  33996  eqeltr  34144  islfld  34667  lkrshpor  34712  lfl1dim  34726  lfl1dim2N  34727  cmtcomlemN  34853  2lplnmN  35163  pmapjat1  35457  trlnid  35784  tendoex  36580  dia1dimid  36669  dibval2  36750  dihmeetlem2N  36905  dochlkr  36991  mapdcv  37266  hdmaplkr  37522  hdmapip0  37524  hlhillcs  37567  nacsfix  37592  3rexfrabdioph  37678  4rexfrabdioph  37679  6rexfrabdioph  37680  7rexfrabdioph  37681  eldioph4b  37692  pellexlem2  37711  pellexlem5  37714  expmordi  37829  jm2.26lem3  37885  numinfctb  37990  ntrclsfv1  38670  ntrneifv1  38694  ntrneifv2  38695  cvgdvgrat  38829  radcnvrat  38830  dvconstbi  38850  bccbc  38861  elpwgded  39097  elpwgdedVD  39467  sspwimpcf  39470  sspwimpcfVD  39471  sspwimpALT2  39478  ax6e2ndeqALT  39481  eliuniin  39593  eliuniin2  39617  qinioo  40080  dfxlim2v  40391  cncfiooicclem1  40424  ibliooicc  40505  stoweidlem27  40562  stoweidlem28  40563  fourierdlem89  40730  fourierdlem91  40732  fourierdlem92  40733  smflimmpt  41337  ccatpfx  41734  odz2prm2pw  41800  perfectALTVlem2  41956  blen1b  42707  onetansqsecsq  42830  cotsqcscsq  42831  aacllem  42875
  Copyright terms: Public domain W3C validator