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

Theorem biimpar 463
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 393 1 ((𝜑𝜒) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382
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 383
This theorem is referenced by:  bitr  806  exbiri  811  oplem1  1043  eqtr  2790  opabss  4848  euotd  5106  brcogw  5429  somin1  5670  xpdifid  5703  funfni  6131  fnco  6139  fnssres  6144  fn0  6151  fnimadisj  6152  fnimaeq0  6153  foco  6266  foimacnv  6295  fvelimab  6395  dffv2  6413  fvopab3ig  6420  dff3  6515  dffo4  6518  fpr2g  6619  f1eqcocnv  6699  isomin  6730  f1ocnv2d  7033  fnexALT  7279  xp1st  7347  xp2nd  7348  wfr3g  7565  wfrlem3  7568  wfrlem4  7570  wfrlem4OLD  7571  iinon  7590  tfr3  7648  oawordri  7784  oaass  7795  omeulem1  7816  oeoa  7831  oeoe  7833  oeeulem  7835  ecelqsg  7954  elqsn0  7968  pwdom  8268  marypha1lem  8495  wofib  8606  cantnff  8735  cantnfp1  8742  cantnf  8754  cnfcomlem  8760  r1sscl  8812  rankval3b  8853  infxpidm2  9040  numdom  9061  onssnum  9063  acni  9068  acni2  9069  dfac5  9151  cdalepw  9220  infunsdom1  9237  infunsdom  9238  cofsmo  9293  cfsmolem  9294  fin1ai  9317  fin2i  9319  isf34lem1  9396  fin67  9419  itunisuc  9443  axdc3lem4  9477  zornn0g  9529  ttukeylem6  9538  brdom3  9552  tsken  9778  tskcard  9805  r1tskina  9806  intgru  9838  prlem934  10057  ltexprlem7  10066  supaddc  11192  mul2lt0rlt0  12135  xrmaxeq  12215  xrmineq  12216  xmulneg1  12304  ixxun  12396  difelfzle  12660  ssfzoulel  12770  elfznelfzo  12781  ico01fl0  12828  btwnzge0  12837  ltdifltdiv  12843  ioopnfsup  12871  icopnfsup  12872  modifeq2int  12940  suppssfz  13001  faclbnd4lem4  13287  hasheni  13340  hashgt0  13379  hashge1  13380  hashprb  13387  lennncl  13521  wrdsymb0  13535  ccatsymb  13564  ccatlid  13568  ccatass  13570  swrdid  13637  ccatswrd  13665  swrdccat2  13667  swrdccat  13702  revccat  13724  cnpart  14188  resqreu  14201  recval  14270  abs1m  14283  abslem2  14287  fzomaxdiflem  14290  sqreulem  14307  sqreu  14308  limsupgre  14420  rlimdiv  14584  fsumparts  14745  climcnds  14790  expcnv  14803  ntrivcvg  14836  mod2eq1n2dvds  15279  ndvdssub  15341  sadcaddlem  15387  rplpwr  15484  dvdssqlem  15487  algcvgblem  15498  eucalgcvga  15507  isprm2lem  15601  powm2modprm  15715  coprimeprodsq  15720  pythagtriplem11  15737  pythagtriplem13  15739  pcadd2  15801  4sqlem11  15866  vdwlem6  15897  vdwlem8  15899  vdwlem10  15901  ramval  15919  ramcl2  15927  ramlb  15930  ram0  15933  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  17772  subgmulg  17816  resghm  17884  conjnsg  17904  f1otrspeq  18074  pmtrval  18078  pmtrrn  18084  pmtrfinv  18088  pmtrprfval  18114  psgnunilem1  18120  psgnunilem5  18121  psgnunilem4  18124  psgneldm2i  18132  lsmelvalix  18263  pj1ghm  18323  efgredlemc  18365  frgp0  18380  qusabl  18475  cycsubgcyg  18509  gsumval3  18515  gsumcllem  18516  ablfac1c  18678  pgpfac1lem5  18686  isringd  18793  lspsneq0b  19226  lmodindp1  19227  lmhmf1o  19259  lmhmpreima  19261  reslmhm  19265  pwssplit3  19274  lspsncmp  19329  lspsneq  19335  mpfind  19751  znf1o  20115  dsmmlss  20305  frlmlbs  20353  frlmup1  20354  mat1  20471  chfacfisf  20879  chfacfisfcpmat  20880  uniopn  20922  ntrval  21061  clsval  21062  neival  21127  neiptopreu  21158  lpval  21164  restdis  21203  lmbrf  21285  cnpnei  21289  1stcrest  21477  hauspwdom  21525  lfinpfin  21548  txcnpi  21632  ptrescn  21663  xkococnlem  21683  qtopeu  21740  kqreglem1  21765  ptuncnv  21831  filss  21877  fsubbas  21891  fbasrn  21908  cfinfil  21917  ufinffr  21953  elfm3  21974  rnelfmlem  21976  rnelfm  21977  flimclslem  22008  flfval  22014  isfcf  22058  cnextfvval  22089  cnextf  22090  cnextcn  22091  ustelimasn  22246  trust  22253  restutop  22261  ustuqtop2  22266  utop2nei  22274  ucncn  22309  trcfilu  22318  cnextucn  22327  met1stc  22546  metustexhalf  22581  cfilucfil  22584  psmetutop  22592  nmoix  22753  nmoeq0  22760  idnghm  22767  blcvx  22821  xrsxmet  22832  iccntr  22844  icccmp  22848  iihalf1  22950  iihalf2  22952  xrhmeo  22965  cnheibor  22974  ipcau2  23252  lmmbrf  23279  iscauf  23297  cmetcaulem  23305  bcthlem4  23343  cmetcusp  23369  rrxcph  23399  minveclem4  23422  evthicc2  23448  cniccbdd  23449  ovollb2  23477  ovolunlem1a  23484  ovolunlem1  23485  voliun  23542  icombl  23552  ioombl  23553  iccvolcl  23555  ioovolcl  23558  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  24660  abscxpbnd  24715  ang180lem2  24761  ang180lem3  24762  isosctrlem1  24769  angpieqvd  24779  atandmtan  24868  birthdaylem3  24901  wilthlem2  25016  wilthimp  25019  isppw  25061  isppw2  25062  dvdsflsumcom  25135  chteq0  25155  perfectlem2  25176  dchrval  25180  dchrinvcl  25199  dchrptlem1  25210  bposlem3  25232  lgslem4  25246  lgsmod  25269  lgsdilem  25270  lgsdir2lem2  25272  lgsdir2  25276  lgsne0  25281  lgsmulsqcoprm  25289  lgseisenlem1  25321  2lgsoddprm  25362  2sqlem4  25367  chpo1ubb  25391  dchrisumn0  25431  pntrsumbnd2  25477  ostthlem1  25537  ostth3  25548  idmot  25653  tgelrnln  25746  lmimid  25907  lmiisolem  25909  hypcgrlem1  25912  brcgr  26001  colinearalglem4  26010  colinearalg  26011  axlowdimlem14  26056  axcontlem4  26068  cplgrop  26568  lfgriswlk  26820  pthdlem1  26897  crctcshwlkn0  26949  wlknwwlksnsurOLD  27024  elwspths2on  27108  clwwlkgt0  27136  clwlkclwwlklem2fv2  27146  frgrncvvdeqlem9  27489  nvss  27788  sspn  27931  nmoub3i  27968  nmblolbii  27994  blocnilem  27999  minvecolem4  28076  htthlem  28114  norm1  28446  norm1exi  28447  pjeq  28598  axpjpj  28619  normcan  28775  pjoi0  28916  nmopub2tALT  29108  nmfnleub2  29125  eighmorth  29163  nmbdoplbi  29223  nmcoplbi  29227  nmophmi  29230  nmbdfnlbi  29248  nmcfnlbi  29251  riesz3i  29261  cnlnadjlem7  29272  branmfn  29304  nmopleid  29338  hstle  29429  superpos  29553  cvexchlem  29567  foresf1o  29681  elabreximd  29686  f1o3d  29771  fmptco1f1o  29774  funcnvmptOLD  29807  funcnvmpt  29808  fgreu  29811  resf1o  29845  fpwrelmap  29848  xrofsup  29873  eliccelico  29879  elicoelioo  29880  iocinif  29883  difioo  29884  eliccioo  29979  submomnd  30050  archirngz  30083  gsummpt2co  30120  ornglmullt  30147  orngrmullt  30148  pmtridf1o  30196  madjusmdetlem2  30234  qtophaus  30243  locfinreflem  30247  unitdivcld  30287  tpr2rico  30298  ordtrestNEW  30307  lmxrge0  30338  elzrhunit  30363  qqhf  30370  indf1ofs  30428  gsumesum  30461  esumfsup  30472  esumcvg  30488  issgon  30526  sigainb  30539  insiga  30540  isrnmeas  30603  measvunilem  30615  volmeas  30634  ddeval1  30637  ddeval0  30638  imambfm  30664  omssubadd  30702  carsgclctunlem3  30722  eulerpartlemf  30772  eulerpartlemgvv  30778  probun  30821  dstfrvunirn  30876  plymulx  30965  signslema  30979  signstfvn  30986  signsvtn0  30987  signstfvneq0  30989  signstres  30992  signstfveq0a  30993  breprexplemc  31050  logdivsqrle  31068  hgt750lemg  31072  tgoldbachgtda  31079  tgoldbachgt  31081  bnj529  31149  bnj548  31305  bnj570  31313  bnj852  31329  bnj929  31344  bnj1097  31387  bnj1118  31390  bnj1145  31399  derangen  31492  subfacp1lem2b  31501  subfacp1lem4  31503  subfacp1lem5  31504  derangfmla  31510  ptpconn  31553  mppspstlem  31806  wsuclem  32107  frr3g  32116  frrlem3  32119  nosupbnd2lem1  32198  nocvxmin  32231  colinearex  32504  btwnconn1lem11  32541  btwnconn1lem12  32542  fwddifnp1  32609  gtinfOLD  32651  nn0prpwlem  32654  bj-snmoore  33400  relowlpssretop  33549  fin2so  33729  matunitlindflem2  33739  ptrecube  33742  poimirlem8  33750  poimirlem13  33755  poimirlem15  33757  poimirlem24  33766  poimirlem25  33767  poimirlem26  33768  heicant  33777  mblfinlem2  33780  voliunnfl  33786  mbfresfi  33788  itg2addnclem  33793  itg2addnclem3  33795  itg2gt0cn  33797  ftc1cnnclem  33815  ftc1anclem5  33821  cover2  33840  indexdom  33861  sdclem1  33871  fdc  33873  equivbnd2  33923  heiborlem8  33949  heibor  33952  isdrngo2  34089  iscringd  34129  smprngopr  34183  prnc  34198  eqeltr  34346  islfld  34871  lkrshpor  34916  lfl1dim  34930  lfl1dim2N  34931  cmtcomlemN  35057  2lplnmN  35367  pmapjat1  35661  trlnid  35988  tendoex  36784  dia1dimid  36873  dibval2  36954  dihmeetlem2N  37109  dochlkr  37195  mapdcv  37470  hdmaplkr  37723  hdmapip0  37725  hlhillcs  37768  nacsfix  37801  3rexfrabdioph  37887  4rexfrabdioph  37888  6rexfrabdioph  37889  7rexfrabdioph  37890  eldioph4b  37901  pellexlem2  37920  pellexlem5  37923  expmordi  38038  jm2.26lem3  38094  numinfctb  38199  ntrclsfv1  38879  ntrneifv1  38903  ntrneifv2  38904  cvgdvgrat  39038  radcnvrat  39039  dvconstbi  39059  bccbc  39070  elpwgded  39305  elpwgdedVD  39675  sspwimpcf  39678  sspwimpcfVD  39679  sspwimpALT2  39686  ax6e2ndeqALT  39689  eliuniin  39800  eliuniin2  39824  qinioo  40280  dfxlim2v  40591  cncfiooicclem1  40624  ibliooicc  40704  stoweidlem27  40761  stoweidlem28  40762  fourierdlem89  40929  fourierdlem91  40931  fourierdlem92  40932  smflimmpt  41536  ccatpfx  41937  odz2prm2pw  42003  perfectALTVlem2  42159  blen1b  42910  onetansqsecsq  43033  cotsqcscsq  43034  aacllem  43078
  Copyright terms: Public domain W3C validator