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

Theorem biimpar 502
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 445 1 ((𝜑𝜒) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  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 197  df-an 386
This theorem is referenced by:  exbiri  652  bitr  745  oplem1  1007  eqtr  2640  opabss  4712  euotd  4973  brcogw  5288  somin1  5527  xpdifid  5560  funfni  5989  fnco  5997  fnssres  6002  fn0  6009  fnimadisj  6010  fnimaeq0  6011  foco  6123  foimacnv  6152  fvelimab  6251  dffv2  6269  fvopab3ig  6276  dff3  6370  dffo4  6373  fpr2g  6472  f1eqcocnv  6553  isomin  6584  f1ocnv2d  6883  fnexALT  7129  xp1st  7195  xp2nd  7196  wfr3g  7410  wfrlem3  7413  wfrlem4  7415  iinon  7434  tfr3  7492  oawordri  7627  oaass  7638  omeulem1  7659  oeoa  7674  oeoe  7676  oeeulem  7678  ecelqsg  7799  elqsn0  7813  pwdom  8109  marypha1lem  8336  wofib  8447  cantnff  8568  cantnfp1  8575  cantnf  8587  cnfcomlem  8593  r1sscl  8645  rankval3b  8686  infxpidm2  8837  numdom  8858  onssnum  8860  acni  8865  acni2  8866  dfac5  8948  cdalepw  9015  infunsdom1  9032  infunsdom  9033  cofsmo  9088  cfsmolem  9089  fin1ai  9112  fin2i  9114  isf34lem1  9191  fin67  9214  itunisuc  9238  axdc3lem4  9272  zornn0g  9324  ttukeylem6  9333  brdom3  9347  tsken  9573  tskcard  9600  r1tskina  9601  intgru  9633  prlem934  9852  ltexprlem7  9861  supaddc  10987  mul2lt0rlt0  11929  xrmaxeq  12007  xrmineq  12008  xmulneg1  12096  ixxun  12188  difelfzle  12448  ssfzoulel  12558  elfznelfzo  12569  ico01fl0  12615  btwnzge0  12624  ltdifltdiv  12630  ioopnfsup  12658  icopnfsup  12659  modifeq2int  12727  suppssfz  12789  faclbnd4lem4  13078  hasheni  13131  hashgt0  13172  hashge1  13173  hashprb  13180  lennncl  13320  wrdsymb0  13334  ccatsymb  13361  ccatlid  13364  ccatass  13366  swrdid  13422  ccatswrd  13450  swrdccat2  13452  swrdccat  13487  revccat  13509  cnpart  13974  resqreu  13987  recval  14056  abs1m  14069  abslem2  14073  fzomaxdiflem  14076  sqreulem  14093  sqreu  14094  limsupgre  14206  rlimdiv  14370  fsumparts  14532  climcnds  14577  expcnv  14590  ntrivcvg  14623  mod2eq1n2dvds  15065  ndvdssub  15127  sadcaddlem  15173  rplpwr  15270  dvdssqlem  15273  algcvgblem  15284  eucalgcvga  15293  powm2modprm  15502  coprimeprodsq  15507  pythagtriplem11  15524  pythagtriplem13  15526  pcadd2  15588  4sqlem11  15653  vdwlem6  15684  vdwlem8  15686  vdwlem10  15688  ramval  15706  ramcl2  15714  ramlb  15717  ram0  15720  mreintcl  16249  mrcval  16264  mrccl  16265  mrcuni  16275  mrcun  16276  acsfiel  16309  rescabs  16487  funcres  16550  setcmon  16731  setcepi  16732  fullestrcsetc  16785  funcsetcestrclem8  16796  fullsetcestrc  16800  yonffthlem  16916  pleval2i  16958  pospo  16967  poslubdg  17143  acsdrsel  17161  acsdrscl  17164  acsficl  17165  psss  17208  grpidd  17262  ismndd  17307  gsumccat  17372  gsumwmhm  17376  mulgaddcom  17558  subgmulg  17602  resghm  17670  conjnsg  17690  f1otrspeq  17861  pmtrval  17865  pmtrrn  17871  pmtrfinv  17875  pmtrprfval  17901  psgnunilem1  17907  psgnunilem5  17908  psgnunilem4  17911  psgneldm2i  17919  lsmelvalix  18050  pj1ghm  18110  efgredlemc  18152  frgp0  18167  qusabl  18262  cycsubgcyg  18296  gsumval3  18302  gsumcllem  18303  ablfac1c  18464  pgpfac1lem5  18472  isringd  18579  lspsneq0b  19007  lmodindp1  19008  lmhmf1o  19040  lmhmpreima  19042  reslmhm  19046  pwssplit3  19055  lspsncmp  19110  lspsneq  19116  mpfind  19530  znf1o  19894  dsmmlss  20082  frlmlbs  20130  frlmup1  20131  mat1  20247  chfacfisf  20653  chfacfisfcpmat  20654  uniopn  20696  ntrval  20834  clsval  20835  neival  20900  neiptopreu  20931  lpval  20937  restdis  20976  lmbrf  21058  cnpnei  21062  1stcrest  21250  hauspwdom  21298  lfinpfin  21321  txcnpi  21405  ptrescn  21436  xkococnlem  21456  qtopeu  21513  kqreglem1  21538  ptuncnv  21604  filss  21651  fsubbas  21665  fbasrn  21682  cfinfil  21691  ufinffr  21727  elfm3  21748  rnelfmlem  21750  rnelfm  21751  flimclslem  21782  flfval  21788  isfcf  21832  cnextfvval  21863  cnextf  21864  cnextcn  21865  ustelimasn  22020  trust  22027  restutop  22035  ustuqtop2  22040  utop2nei  22048  ucncn  22083  trcfilu  22092  cnextucn  22101  met1stc  22320  metustexhalf  22355  cfilucfil  22358  psmetutop  22366  nmoix  22527  nmoeq0  22534  idnghm  22541  blcvx  22595  xrsxmet  22606  iccntr  22618  icccmp  22622  iihalf1  22724  iihalf2  22726  xrhmeo  22739  cnheibor  22748  ipcau2  23027  lmmbrf  23054  iscauf  23072  cmetcaulem  23080  bcthlem4  23118  cmetcusp  23144  rrxcph  23174  minveclem4  23197  evthicc2  23223  cniccbdd  23224  ovollb2  23251  ovolunlem1a  23258  ovolunlem1  23259  voliun  23316  icombl  23326  ioombl  23327  iccvolcl  23329  ioovolcl  23332  mbfss  23407  mbfposb  23414  itg2const2  23502  itg2splitlem  23509  itg2gt0  23521  iblss2  23566  itgioo  23576  dvaddf  23699  dvmulf  23700  dvcobr  23703  dvcof  23705  rolle  23747  dvlip  23750  c1lip1  23754  dvivthlem1  23765  lhop1lem  23770  dvfsumlem1  23783  ftc1lem4  23796  ftc1lem5  23797  ply1divmo  23889  coe1termlem  24008  plydiveu  24047  taylplem1  24111  pserulm  24170  abelth  24189  abscxp2  24433  abscxpbnd  24488  ang180lem2  24534  ang180lem3  24535  isosctrlem1  24542  angpieqvd  24552  atandmtan  24641  birthdaylem3  24674  wilthlem2  24789  wilthimp  24792  isppw  24834  isppw2  24835  dvdsflsumcom  24908  chteq0  24928  perfectlem2  24949  dchrval  24953  dchrinvcl  24972  dchrptlem1  24983  bposlem3  25005  lgsmod  25042  lgsdilem  25043  lgsdir2lem2  25045  lgsdir2  25049  lgsne0  25054  lgsmulsqcoprm  25062  lgseisenlem1  25094  2lgsoddprm  25135  2sqlem4  25140  chpo1ubb  25164  dchrisumn0  25204  pntrsumbnd2  25250  ostthlem1  25310  ostth3  25321  idmot  25426  tgelrnln  25519  lmimid  25680  lmiisolem  25682  hypcgrlem1  25685  brcgr  25774  colinearalglem4  25783  colinearalg  25784  axlowdimlem14  25829  axcontlem4  25841  cplgrop  26327  lfgriswlk  26579  pthdlem1  26656  crctcshwlkn0  26707  wlknwwlksnsur  26770  elwspths2on  26847  clwlkclwwlklem2fv2  26891  clwwlksgt0  26899  frgrncvvdeqlem9  27164  nvss  27432  sspn  27575  nmoub3i  27612  nmblolbii  27638  blocnilem  27643  minvecolem4  27720  htthlem  27758  norm1  28090  norm1exi  28091  pjeq  28242  axpjpj  28263  normcan  28419  pjoi0  28560  nmopub2tALT  28752  nmfnleub2  28769  eighmorth  28807  nmbdoplbi  28867  nmcoplbi  28871  nmophmi  28874  nmbdfnlbi  28892  nmcfnlbi  28895  riesz3i  28905  cnlnadjlem7  28916  branmfn  28948  nmopleid  28982  hstle  29073  superpos  29197  cvexchlem  29211  foresf1o  29327  elabreximd  29332  f1o3d  29415  fmptco1f1o  29418  funcnvmptOLD  29452  funcnvmpt  29453  fgreu  29456  resf1o  29490  fpwrelmap  29493  xrofsup  29518  eliccelico  29524  elicoelioo  29525  iocinif  29528  difioo  29529  eliccioo  29624  submomnd  29695  archirngz  29728  gsummpt2co  29765  ornglmullt  29792  orngrmullt  29793  pmtridf1o  29841  madjusmdetlem2  29879  qtophaus  29888  locfinreflem  29892  unitdivcld  29932  tpr2rico  29943  ordtrestNEW  29952  lmxrge0  29983  elzrhunit  30008  qqhf  30015  indf1ofs  30073  gsumesum  30106  esumfsup  30117  esumcvg  30133  issgon  30171  sigainb  30184  insiga  30185  isrnmeas  30248  measvunilem  30260  volmeas  30279  ddeval1  30282  ddeval0  30283  imambfm  30309  omssubadd  30347  carsgclctunlem3  30367  eulerpartlemf  30417  eulerpartlemgvv  30423  probun  30466  dstfrvunirn  30521  plymulx  30610  signslema  30624  signstfvn  30631  signsvtn0  30632  signstfvneq0  30634  signstres  30637  signstfveq0a  30638  breprexplemc  30695  logdivsqrle  30713  hgt750lemg  30717  tgoldbachgtda  30724  tgoldbachgt  30726  bnj529  30796  bnj548  30952  bnj570  30960  bnj852  30976  bnj929  30991  bnj1097  31034  bnj1118  31037  bnj1145  31046  derangen  31139  subfacp1lem2b  31148  subfacp1lem4  31150  subfacp1lem5  31151  derangfmla  31157  ptpconn  31200  mppspstlem  31453  wsuclem  31757  wsuclemOLD  31758  frr3g  31763  frrlem3  31766  nosupbnd2lem1  31845  nocvxmin  31878  colinearex  32151  btwnconn1lem11  32188  btwnconn1lem12  32189  fwddifnp1  32256  gtinfOLD  32298  nn0prpwlem  32301  bj-snmoore  33052  relowlpssretop  33192  fin2so  33376  matunitlindflem2  33386  ptrecube  33389  poimirlem8  33397  poimirlem13  33402  poimirlem15  33404  poimirlem24  33413  poimirlem25  33414  poimirlem26  33415  heicant  33424  mblfinlem2  33427  voliunnfl  33433  mbfresfi  33436  itg2addnclem  33441  itg2addnclem3  33443  itg2gt0cn  33445  ftc1cnnclem  33463  ftc1anclem5  33469  cover2  33488  indexdom  33509  sdclem1  33519  fdc  33521  equivbnd2  33571  heiborlem8  33597  heibor  33600  isdrngo2  33737  iscringd  33777  smprngopr  33831  prnc  33846  islfld  34175  lkrshpor  34220  lfl1dim  34234  lfl1dim2N  34235  cmtcomlemN  34361  2lplnmN  34671  pmapjat1  34965  trlnid  35292  tendoex  36089  dia1dimid  36178  dibval2  36259  dihmeetlem2N  36414  dochlkr  36500  mapdcv  36775  hdmaplkr  37031  hdmapip0  37033  hlhillcs  37076  nacsfix  37101  3rexfrabdioph  37187  4rexfrabdioph  37188  6rexfrabdioph  37189  7rexfrabdioph  37190  eldioph4b  37201  pellexlem2  37220  pellexlem5  37223  expmordi  37338  jm2.26lem3  37394  numinfctb  37499  ntrclsfv1  38179  ntrneifv1  38203  ntrneifv2  38204  cvgdvgrat  38338  radcnvrat  38339  dvconstbi  38359  bccbc  38370  elpwgded  38606  elpwgdedVD  38979  sspwimpcf  38982  sspwimpcfVD  38983  sspwimpALT2  38990  ax6e2ndeqALT  38993  eliuniin  39105  eliuniin2  39129  qinioo  39571  cncfiooicclem1  39875  ibliooicc  39956  stoweidlem27  40013  stoweidlem28  40014  fourierdlem89  40181  fourierdlem91  40183  fourierdlem92  40184  smflimmpt  40785  ccatpfx  41180  odz2prm2pw  41246  perfectALTVlem2  41402  blen1b  42153  onetansqsecsq  42273  cotsqcscsq  42274  aacllem  42318
  Copyright terms: Public domain W3C validator