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

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
StepHypRef Expression
1 biimpa.1 . . 3 (𝜑 → (𝜓𝜒))
21biimprd 249 . 2 (𝜑 → (𝜒𝜓))
32imp 407 1 ((𝜑𝜒) → 𝜓)
Colors of variables: wff setvar class
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  1048  eqtr  2838  opabss  5121  axprlem4  5317  axprlem5  5318  euotd  5394  brcogw  5732  somin1  5986  xpdifid  6018  funfni  6450  fnco  6458  fnssres  6463  fn0  6472  fnimadisj  6473  fnimaeq0  6474  foco  6595  foimacnv  6625  fvelimab  6730  dffv2  6749  fvopab3ig  6757  dff3  6858  dffo4  6861  fpr2g  6965  f1eqcocnv  7048  isomin  7079  f1ocnv2d  7387  fnexALT  7641  xp1st  7710  xp2nd  7711  wfr3g  7942  wfrlem3  7945  wfrlem4  7947  iinon  7966  tfr3  8024  oawordri  8165  oaass  8176  omeulem1  8197  oeoa  8212  oeoe  8214  oeeulem  8216  ecelqsg  8341  elqsn0  8355  pwdom  8657  marypha1lem  8885  wofib  8997  cantnff  9125  cantnfp1  9132  cantnf  9144  cnfcomlem  9150  r1sscl  9202  rankval3b  9243  infxpidm2  9431  numdom  9452  onssnum  9454  acni  9459  acni2  9460  dfac5  9542  djulepw  9606  infunsdom1  9623  infunsdom  9624  cofsmo  9679  cfsmolem  9680  fin1ai  9703  fin2i  9705  isf34lem1  9782  fin67  9805  itunisuc  9829  axdc3lem4  9863  zornn0g  9915  ttukeylem6  9924  brdom3  9938  tsken  10164  tskcard  10191  r1tskina  10192  intgru  10224  prlem934  10443  ltexprlem7  10452  supaddc  11596  mul2lt0rlt0  12479  xrmaxeq  12560  xrmineq  12561  xmulneg1  12650  ixxun  12742  difelfzle  13008  ssfzoulel  13119  elfznelfzo  13130  ico01fl0  13177  btwnzge0  13186  ltdifltdiv  13192  ioopnfsup  13220  icopnfsup  13221  modifeq2int  13289  suppssfz  13350  expmordi  13519  faclbnd4lem4  13644  hasheni  13696  hashgt0  13737  hashge1  13738  hashprb  13746  lennncl  13872  wrdsymb0  13889  ccatsymb  13924  ccatlid  13928  ccatass  13930  ccatswrd  14018  swrdccat2  14019  ccatpfx  14051  swrdccatfn  14074  swrdccat  14085  revccat  14116  2cshw  14163  cnpart  14587  resqreu  14600  recval  14670  abs1m  14683  abslem2  14687  fzomaxdiflem  14690  sqreulem  14707  sqreu  14708  limsupgre  14826  rlimdiv  14990  fsumparts  15149  climcnds  15194  expcnv  15207  ntrivcvg  15241  mod2eq1n2dvds  15684  ndvdssub  15748  sadcaddlem  15794  rplpwr  15895  dvdssqlem  15898  algcvgblem  15909  eucalgcvga  15918  isprm2lem  16013  powm2modprm  16128  coprimeprodsq  16133  pythagtriplem11  16150  pythagtriplem13  16152  pcadd2  16214  4sqlem11  16279  vdwlem6  16310  vdwlem8  16312  vdwlem10  16314  ramval  16332  ramcl2  16340  ramlb  16343  ram0  16346  mreintcl  16854  mrcval  16869  mrccl  16870  mrcuni  16880  mrcun  16881  acsfiel  16913  rescabs  17091  funcres  17154  setcmon  17335  setcepi  17336  fullestrcsetc  17389  funcsetcestrclem8  17400  fullsetcestrc  17404  yonffthlem  17520  pleval2i  17562  pospo  17571  poslubdg  17747  acsdrsel  17765  acsdrscl  17768  acsficl  17769  psss  17812  grpidd  17869  ismndd  17921  gsumsgrpccat  17992  gsumccatOLD  17993  gsumwmhm  17998  mulgaddcom  18189  subgmulg  18231  resghm  18312  conjnsg  18332  f1otrspeq  18504  pmtrval  18508  pmtrrn  18514  pmtrfinv  18518  pmtrprfval  18544  psgnunilem1  18550  psgnunilem5  18551  psgnunilem4  18554  psgneldm2i  18562  lsmelvalix  18695  pj1ghm  18758  efgredlemc  18800  frgp0  18815  qusabl  18914  cycsubgcyg  18950  gsumval3  18956  gsumcllem  18957  ablfac1c  19122  pgpfac1lem5  19130  isringd  19264  lspsneq0b  19714  lmodindp1  19715  lmhmf1o  19747  lmhmpreima  19749  reslmhm  19753  pwssplit3  19762  lspsncmp  19817  lspsneq  19823  mpfind  20248  mhplss  20270  znf1o  20626  dsmmlss  20816  frlmlbs  20869  frlmup1  20870  mat1  20984  chfacfisf  21390  chfacfisfcpmat  21391  uniopn  21433  ntrval  21572  clsval  21573  neival  21638  neiptopreu  21669  lpval  21675  restdis  21714  lmbrf  21796  cnpnei  21800  1stcrest  21989  hauspwdom  22037  lfinpfin  22060  txcnpi  22144  ptrescn  22175  xkococnlem  22195  qtopeu  22252  kqreglem1  22277  ptuncnv  22343  filss  22389  fsubbas  22403  fbasrn  22420  cfinfil  22429  ufinffr  22465  elfm3  22486  rnelfmlem  22488  rnelfm  22489  flimclslem  22520  flfval  22526  isfcf  22570  cnextfvval  22601  cnextf  22602  cnextcn  22603  ustelimasn  22758  trust  22765  restutop  22773  ustuqtop2  22778  utop2nei  22786  ucncn  22821  trcfilu  22830  cnextucn  22839  met1stc  23058  metustexhalf  23093  cfilucfil  23096  psmetutop  23104  nmoix  23265  nmoeq0  23272  idnghm  23279  blcvx  23333  xrsxmet  23344  iccntr  23356  icccmp  23360  iihalf1  23462  iihalf2  23464  xrhmeo  23477  cnheibor  23486  ipcau2  23764  lmmbrf  23792  iscauf  23810  cmetcaulem  23818  bcthlem4  23857  cmetcusp  23884  rrxcph  23922  minveclem4  23962  evthicc2  23988  cniccbdd  23989  ovollb2  24017  ovolunlem1a  24024  ovolunlem1  24025  voliun  24082  icombl  24092  ioombl  24093  iccvolcl  24095  ioovolcl  24098  mbfss  24174  mbfposb  24181  itg2const2  24269  itg2splitlem  24276  itg2gt0  24288  iblss2  24333  itgioo  24343  dvaddf  24466  dvmulf  24467  dvcobr  24470  dvcof  24472  rolle  24514  dvlip  24517  c1lip1  24521  dvivthlem1  24532  lhop1lem  24537  dvfsumlem1  24550  ftc1lem4  24563  ftc1lem5  24564  ply1divmo  24656  coe1termlem  24775  plydiveu  24814  taylplem1  24878  pserulm  24937  abelth  24956  abscxp2  25203  abscxpbnd  25261  logbgt0b  25298  ang180lem2  25315  ang180lem3  25316  isosctrlem1  25323  angpieqvd  25336  atandmtan  25425  birthdaylem3  25458  wilthlem2  25573  wilthimp  25576  isppw  25618  isppw2  25619  dvdsflsumcom  25692  chteq0  25712  perfectlem2  25733  dchrval  25737  dchrinvcl  25756  dchrptlem1  25767  bposlem3  25789  lgslem4  25803  lgsmod  25826  lgsdilem  25827  lgsdir2lem2  25829  lgsdir2  25833  lgsne0  25838  lgsmulsqcoprm  25846  lgseisenlem1  25878  2lgsoddprm  25919  2sqlem4  25924  chpo1ubb  25984  dchrisumn0  26024  pntrsumbnd2  26070  ostthlem1  26130  ostth3  26141  idmot  26250  tgelrnln  26343  lmimid  26507  lmiisolem  26509  hypcgrlem1  26512  brcgr  26613  colinearalglem4  26622  colinearalg  26623  axlowdimlem14  26668  axcontlem4  26680  cplgrop  27146  lfgriswlk  27397  pthdlem1  27474  crctcshwlkn0  27526  elwspths2on  27666  clwlkclwwlklem2fv2  27701  frgrncvvdeqlem9  28013  nvss  28297  sspn  28440  nmoub3i  28477  nmblolbii  28503  blocnilem  28508  minvecolem4  28584  htthlem  28621  norm1  28953  norm1exi  28954  pjeq  29103  axpjpj  29124  normcan  29280  pjoi0  29421  nmopub2tALT  29613  nmfnleub2  29630  eighmorth  29668  nmbdoplbi  29728  nmcoplbi  29732  nmophmi  29735  nmbdfnlbi  29753  nmcfnlbi  29756  riesz3i  29766  cnlnadjlem7  29777  branmfn  29809  nmopleid  29843  hstle  29934  superpos  30058  cvexchlem  30072  foresf1o  30192  elabreximd  30197  unidifsnne  30223  f1o3d  30300  fmptco1f1o  30306  funcnvmpt  30340  fgreu  30345  suppovss  30354  resf1o  30392  fpwrelmap  30395  xrofsup  30418  eliccelico  30426  elicoelioo  30427  iocinif  30430  difioo  30431  eliccioo  30534  cshf1o  30563  gsummpt2co  30613  submomnd  30638  symgcom  30654  symgcom2  30655  odpmco  30657  pmtrcnel  30660  pmtridf1o  30663  cycpmco2lem6  30700  cycpmco2lem7  30701  cycpmco2  30702  cyc3co2  30709  cycpmconjv  30711  tocyccntz  30713  cyc3evpm  30719  cycpmconjslem2  30724  cycpmconjs  30725  archirngz  30745  ornglmullt  30807  orngrmullt  30808  lindssn  30866  linds2eq  30868  prmidl2  30877  qsidomlem1  30882  lbslsat  30913  lindsunlem  30919  lindsun  30920  dimkerim  30922  fedgmullem1  30924  fedgmullem2  30925  fedgmul  30926  madjusmdetlem2  30992  qtophaus  30999  locfinreflem  31003  unitdivcld  31043  tpr2rico  31054  ordtrestNEW  31063  lmxrge0  31094  elzrhunit  31119  qqhf  31126  indf1ofs  31184  gsumesum  31217  esumfsup  31228  esumcvg  31244  issgon  31281  sigainb  31294  insiga  31295  isrnmeas  31358  measvunilem  31370  volmeas  31389  ddeval1  31392  ddeval0  31393  imambfm  31419  omssubadd  31457  carsgclctunlem3  31477  eulerpartlemf  31527  eulerpartlemgvv  31533  probun  31576  dstfrvunirn  31631  plymulx  31717  signslema  31731  signstfvn  31738  signsvtn0  31739  signstfvneq0  31741  signstres  31744  signstfveq0a  31745  breprexplemc  31802  logdivsqrle  31820  hgt750lemg  31824  tgoldbachgtda  31831  tgoldbachgt  31833  lpadmax  31852  lpadleft  31853  lpadright  31854  bnj529  31911  bnj548  32068  bnj570  32076  bnj852  32092  bnj929  32107  bnj1097  32150  bnj1118  32153  bnj1145  32162  funen1cnv  32254  spthcycl  32273  acycgr0v  32292  derangen  32316  subfacp1lem2b  32325  subfacp1lem4  32327  subfacp1lem5  32328  derangfmla  32334  ptpconn  32377  mppspstlem  32715  wsuclem  33009  frr3g  33018  frrlem3  33022  fpr2  33037  nosupbnd2lem1  33112  nocvxmin  33145  colinearex  33418  btwnconn1lem11  33455  btwnconn1lem12  33456  fwddifnp1  33523  nn0prpwlem  33567  bj-snmoore  34299  relowlpssretop  34527  fin2so  34760  matunitlindflem2  34770  ptrecube  34773  poimirlem8  34781  poimirlem13  34786  poimirlem15  34788  poimirlem24  34797  poimirlem25  34798  poimirlem26  34799  heicant  34808  mblfinlem2  34811  voliunnfl  34817  mbfresfi  34819  itg2addnclem  34824  itg2addnclem3  34826  itg2gt0cn  34828  ftc1cnnclem  34846  ftc1anclem5  34852  cover2  34870  indexdom  34890  sdclem1  34899  fdc  34901  equivbnd2  34951  heiborlem8  34977  heibor  34980  isdrngo2  35117  iscringd  35157  smprngopr  35211  prnc  35226  eqeltr  35382  islfld  36078  lkrshpor  36123  lfl1dim  36137  lfl1dim2N  36138  cmtcomlemN  36264  2lplnmN  36575  pmapjat1  36869  trlnid  37195  tendoex  37991  dia1dimid  38079  dibval2  38160  dihmeetlem2N  38315  dochlkr  38401  mapdcv  38676  hdmaplkr  38929  hdmapip0  38931  hlhillcs  38974  frlmvscadiccat  39023  nacsfix  39187  3rexfrabdioph  39272  4rexfrabdioph  39273  6rexfrabdioph  39274  7rexfrabdioph  39275  eldioph4b  39286  pellexlem2  39305  pellexlem5  39308  jm2.26lem3  39476  numinfctb  39581  ntrclsfv1  40283  ntrneifv1  40307  ntrneifv2  40308  cvgdvgrat  40522  radcnvrat  40523  dvconstbi  40543  bccbc  40554  elpwgded  40775  elpwgdedVD  41128  sspwimpcf  41131  sspwimpcfVD  41132  sspwimpALT2  41139  ax6e2ndeqALT  41142  eliuniin  41242  eliuniin2  41263  qinioo  41687  dfxlim2v  42004  xlimliminflimsup  42019  cncfiooicclem1  42052  ibliooicc  42132  stoweidlem27  42189  stoweidlem28  42190  fourierdlem89  42357  fourierdlem91  42359  fourierdlem92  42360  smflimmpt  42961  odz2prm2pw  43602  perfectALTVlem2  43764  blen1b  44576  itscnhlc0yqe  44674  itsclquadb  44691  onetansqsecsq  44788  cotsqcscsq  44789  aacllem  44830
  Copyright terms: Public domain W3C validator