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 237 . 2 (𝜑 → (𝜒𝜓))
32imp 444 1 ((𝜑𝜒) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  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 196  df-an 385
This theorem is referenced by:  exbiri  650  bitr  741  oplem1  999  eqtr  2629  opabss  4646  euotd  4900  brcogw  5212  somin1  5448  xpdifid  5481  funfni  5905  fnco  5913  fnssres  5918  fn0  5924  fnimadisj  5925  fnimaeq0  5926  foco  6038  foimacnv  6067  fvelimab  6163  dffv2  6181  fvopab3ig  6188  dff3  6280  dffo4  6283  fpr2g  6380  f1eqcocnv  6456  isomin  6487  f1ocnv2d  6784  fnexALT  7025  xp1st  7089  xp2nd  7090  wfr3g  7300  wfrlem3  7303  wfrlem4  7305  iinon  7324  tfr3  7382  oawordri  7517  oaass  7528  omeulem1  7549  oeoa  7564  oeoe  7566  oeeulem  7568  ecelqsg  7689  elqsn0  7703  pwdom  7997  marypha1lem  8222  wofib  8333  cantnff  8454  cantnfp1  8461  cantnf  8473  cnfcomlem  8479  r1sscl  8531  rankval3b  8572  infxpidm2  8723  numdom  8744  onssnum  8746  acni  8751  acni2  8752  dfac5  8834  cdalepw  8901  infunsdom1  8918  infunsdom  8919  cofsmo  8974  cfsmolem  8975  fin1ai  8998  fin2i  9000  isf34lem1  9077  fin67  9100  itunisuc  9124  axdc3lem4  9158  zornn0g  9210  ttukeylem6  9219  brdom3  9231  tsken  9455  tskcard  9482  r1tskina  9483  intgru  9515  prlem934  9734  ltexprlem7  9743  supaddc  10867  mul2lt0rlt0  11808  xrmaxeq  11884  xrmineq  11885  xmulneg1  11971  ixxun  12062  difelfzle  12321  ssfzoulel  12428  elfznelfzo  12439  ico01fl0  12482  btwnzge0  12491  ltdifltdiv  12497  ioopnfsup  12525  icopnfsup  12526  modifeq2int  12594  suppssfz  12656  faclbnd4lem4  12945  hasheni  12998  hashgt0  13038  hashge1  13039  hashprb  13046  lennncl  13180  wrdsymb0  13194  ccatsymb  13219  ccatlid  13222  ccatass  13224  swrdid  13280  ccatswrd  13308  swrdccat2  13310  swrdccat  13344  revccat  13366  cnpart  13828  resqreu  13841  recval  13910  abs1m  13923  abslem2  13927  fzomaxdiflem  13930  sqreulem  13947  sqreu  13948  limsupgre  14060  rlimdiv  14224  fsumparts  14379  climcnds  14422  expcnv  14435  ntrivcvg  14468  mod2eq1n2dvds  14909  ndvdssub  14971  sadcaddlem  15017  rplpwr  15114  dvdssqlem  15117  algcvgblem  15128  eucalgcvga  15137  powm2modprm  15346  coprimeprodsq  15351  pythagtriplem11  15368  pythagtriplem13  15370  pcadd2  15432  4sqlem11  15497  vdwlem6  15528  vdwlem8  15530  vdwlem10  15532  ramval  15550  ramcl2  15558  ramlb  15561  ram0  15564  mreintcl  16078  mrcval  16093  mrccl  16094  mrcuni  16104  mrcun  16105  acsfiel  16138  rescabs  16316  funcres  16379  setcmon  16560  setcepi  16561  fullestrcsetc  16614  funcsetcestrclem8  16625  fullsetcestrc  16629  yonffthlem  16745  pleval2i  16787  pospo  16796  poslubdg  16972  acsdrsel  16990  acsdrscl  16993  acsficl  16994  psss  17037  grpidd  17091  ismndd  17136  gsumccat  17201  gsumwmhm  17205  mulgaddcom  17387  subgmulg  17431  resghm  17499  conjnsg  17519  f1otrspeq  17690  pmtrval  17694  pmtrrn  17700  pmtrfinv  17704  pmtrprfval  17730  psgnunilem1  17736  psgnunilem5  17737  psgnunilem4  17740  psgneldm2i  17748  lsmelvalix  17879  pj1ghm  17939  efgredlemc  17981  frgp0  17996  qusabl  18091  cycsubgcyg  18125  gsumval3  18131  gsumcllem  18132  ablfac1c  18293  pgpfac1lem5  18301  isringd  18408  lspsneq0b  18834  lmodindp1  18835  lmhmf1o  18867  lmhmpreima  18869  reslmhm  18873  pwssplit3  18882  lspsncmp  18937  lspsneq  18943  mpfind  19357  znf1o  19719  dsmmlss  19907  frlmlbs  19955  frlmup1  19956  mat1  20072  chfacfisf  20478  chfacfisfcpmat  20479  uniopn  20527  ntrval  20650  clsval  20651  neival  20716  neiptopreu  20747  lpval  20753  restdis  20792  lmbrf  20874  cnpnei  20878  1stcrest  21066  hauspwdom  21114  lfinpfin  21137  txcnpi  21221  ptrescn  21252  xkococnlem  21272  qtopeu  21329  kqreglem1  21354  ptuncnv  21420  filss  21467  fsubbas  21481  fbasrn  21498  cfinfil  21507  ufinffr  21543  elfm3  21564  rnelfmlem  21566  rnelfm  21567  flimclslem  21598  flfval  21604  isfcf  21648  cnextfvval  21679  cnextf  21680  cnextcn  21681  ustelimasn  21836  trust  21843  restutop  21851  ustuqtop2  21856  utop2nei  21864  ucncn  21899  trcfilu  21908  cnextucn  21917  met1stc  22136  metustexhalf  22171  cfilucfil  22174  psmetutop  22182  nmoix  22343  nmoeq0  22350  idnghm  22357  blcvx  22409  xrsxmet  22420  iccntr  22432  icccmp  22436  iihalf1  22538  iihalf2  22540  xrhmeo  22553  cnheibor  22562  ipcau2  22841  lmmbrf  22868  iscauf  22886  cmetcaulem  22894  bcthlem4  22932  cmetcusp  22958  rrxcph  22988  minveclem4  23011  evthicc2  23036  cniccbdd  23037  ovollb2  23064  ovolunlem1a  23071  ovolunlem1  23072  voliun  23129  icombl  23139  ioombl  23140  iccvolcl  23142  ioovolcl  23144  mbfss  23219  mbfposb  23226  itg2const2  23314  itg2splitlem  23321  itg2gt0  23333  iblss2  23378  itgioo  23388  dvaddf  23511  dvmulf  23512  dvcobr  23515  dvcof  23517  rolle  23557  dvlip  23560  c1lip1  23564  dvivthlem1  23575  lhop1lem  23580  dvfsumlem1  23593  ftc1lem4  23606  ftc1lem5  23607  ply1divmo  23699  coe1termlem  23818  plydiveu  23857  taylplem1  23921  pserulm  23980  abelth  23999  abscxp2  24239  abscxpbnd  24294  ang180lem2  24340  ang180lem3  24341  isosctrlem1  24348  angpieqvd  24358  atandmtan  24447  birthdaylem3  24480  wilthlem2  24595  wilthimp  24598  isppw  24640  isppw2  24641  dvdsflsumcom  24714  chteq0  24734  perfectlem2  24755  dchrval  24759  dchrinvcl  24778  dchrptlem1  24789  bposlem3  24811  lgsmod  24848  lgsdilem  24849  lgsdir2lem2  24851  lgsdir2  24855  lgsne0  24860  lgsmulsqcoprm  24868  lgseisenlem1  24900  2lgsoddprm  24941  2sqlem4  24946  chpo1ubb  24970  dchrisumn0  25010  pntrsumbnd2  25056  ostthlem1  25116  ostth3  25127  idmot  25232  tgelrnln  25325  lmimid  25486  lmiisolem  25488  hypcgrlem1  25491  brcgr  25580  colinearalglem4  25589  colinearalg  25590  axlowdimlem14  25635  axcontlem4  25647  uvtxnbgravtx  26023  wlknwwlknsur  26240  clwlkisclwwlklem2fv2  26311  frghash2spot  26590  nvss  26832  sspn  26975  nmoub3i  27012  nmblolbii  27038  blocnilem  27043  minvecolem4  27120  htthlem  27158  norm1  27490  norm1exi  27491  pjeq  27642  axpjpj  27663  normcan  27819  pjoi0  27960  nmopub2tALT  28152  nmfnleub2  28169  eighmorth  28207  nmbdoplbi  28267  nmcoplbi  28271  nmophmi  28274  nmbdfnlbi  28292  nmcfnlbi  28295  riesz3i  28305  cnlnadjlem7  28316  branmfn  28348  nmopleid  28382  hstle  28473  superpos  28597  cvexchlem  28611  foresf1o  28727  elabreximd  28732  f1o3d  28813  funcnvmptOLD  28850  funcnvmpt  28851  fgreu  28854  resf1o  28893  fpwrelmap  28896  xrofsup  28923  eliccelico  28929  elicoelioo  28930  iocinif  28933  difioo  28934  eliccioo  28970  submomnd  29041  archirngz  29074  gsummpt2co  29111  ornglmullt  29138  orngrmullt  29139  madjusmdetlem2  29222  qtophaus  29231  locfinreflem  29235  crefi  29242  unitdivcld  29275  tpr2rico  29286  ordtrestNEW  29295  lmxrge0  29326  elzrhunit  29351  qqhf  29358  indf1ofs  29415  gsumesum  29448  esumfsup  29459  esumcvg  29475  issgon  29513  sigainb  29526  insiga  29527  isrnmeas  29590  measvunilem  29602  volmeas  29621  ddeval1  29624  ddeval0  29625  imambfm  29651  omssubadd  29689  carsgclctunlem3  29709  eulerpartlemf  29759  eulerpartlemgvv  29765  probun  29808  dstfrvunirn  29863  plymulx  29951  signslema  29965  signstfvn  29972  signsvtn0  29973  signstfvneq0  29975  signstres  29978  signstfveq0a  29979  bnj529  30065  bnj548  30221  bnj570  30229  bnj852  30245  bnj929  30260  bnj1097  30303  bnj1118  30306  bnj1145  30315  derangen  30408  subfacp1lem2b  30417  subfacp1lem4  30419  subfacp1lem5  30420  derangfmla  30426  ptpcon  30469  mppspstlem  30722  wsuclem  31017  wsuclemOLD  31018  frr3g  31023  frrlem3  31026  nocvxmin  31090  nobndlem6  31096  nobndup  31099  nobnddown  31100  colinearex  31337  btwnconn1lem11  31374  btwnconn1lem12  31375  fwddifnp1  31442  gtinfOLD  31484  nn0prpwlem  31487  bj-elpw3  32237  relowlpssretop  32388  fin2so  32566  matunitlindflem2  32576  ptrecube  32579  poimirlem8  32587  poimirlem13  32592  poimirlem15  32594  poimirlem24  32603  poimirlem25  32604  poimirlem26  32605  heicant  32614  mblfinlem2  32617  voliunnfl  32623  mbfresfi  32626  itg2addnclem  32631  itg2addnclem3  32633  itg2gt0cn  32635  ftc1cnnclem  32653  ftc1anclem5  32659  cover2  32678  indexdom  32699  sdclem1  32709  fdc  32711  equivbnd2  32761  heiborlem8  32787  heibor  32790  isdrngo2  32927  iscringd  32967  smprngopr  33021  prnc  33036  islfld  33367  lkrshpor  33412  lfl1dim  33426  lfl1dim2N  33427  cmtcomlemN  33553  2lplnmN  33863  pmapjat1  34157  trlnid  34484  tendoex  35281  dia1dimid  35370  dibval2  35451  dihmeetlem2N  35606  dochlkr  35692  mapdcv  35967  hdmaplkr  36223  hdmapip0  36225  hlhillcs  36268  nacsfix  36293  3rexfrabdioph  36379  4rexfrabdioph  36380  6rexfrabdioph  36381  7rexfrabdioph  36382  eldioph4b  36393  pellexlem2  36412  pellexlem5  36415  expmordi  36530  jm2.26lem3  36586  numinfctb  36692  ntrclsfv1  37373  ntrneifv1  37397  ntrneifv2  37398  cvgdvgrat  37534  radcnvrat  37535  dvconstbi  37555  bccbc  37566  elpwgded  37801  elpwgdedVD  38175  sspwimpcf  38178  sspwimpcfVD  38179  sspwimpALT2  38186  ax6e2ndeqALT  38189  qinioo  38609  cncfiooicclem1  38779  ibliooicc  38863  stoweidlem27  38920  stoweidlem28  38921  fourierdlem89  39088  fourierdlem91  39090  fourierdlem92  39091  odz2prm2pw  40013  perfectALTVlem2  40165  ccatpfx  40272  cplgrop  40659  lfgriswlk  40897  pthdlem1  40972  crctcsh1wlkn0  41024  wlknwwlksnsur  41087  elwspths2on  41163  clwlkclwwlklem2fv2  41205  clwwlksgt0  41213  frgrhash2wsp  41497  blen1b  42180  onetansqsecsq  42301  cotsqcscsq  42302  aacllem  42356
  Copyright terms: Public domain W3C validator