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

Theorem biimpa 501
Description: Importation inference from a logical equivalence. (Contributed by NM, 3-May-1994.)
Hypothesis
Ref Expression
biimpa.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
biimpa ((𝜑𝜓) → 𝜒)

Proof of Theorem biimpa
StepHypRef Expression
1 biimpa.1 . . 3 (𝜑 → (𝜓𝜒))
21biimpd 219 . 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:  simprbda  652  simplbda  653  pm5.1  901  bimsc1  979  biimp3a  1430  equsex  2290  euor  2510  euan  2528  cgsexg  3233  cgsex2g  3234  cgsex4g  3235  ceqsex  3236  sbciegft  3460  sbeqalb  3482  syl5sseq  3645  elpwunsn  4215  ralxfr2d  4873  propeqop  4960  euotd  4965  relop  5261  elsnxp  5665  sspred  5676  fnbr  5981  f1o00  6158  foelrni  6231  dffv2  6258  iinpreima  6331  funressn  6411  fnex  6466  f1prex  6524  weniso  6589  riotaeqimp  6619  f1ocnv2d  6871  ofrval  6892  limsssuc  7035  resiexg  7087  eloprabi  7217  1stconst  7250  2ndconst  7251  frxp  7272  poxp  7274  smodm2  7437  smoiso  7444  tz7.44lem1  7486  oev2  7588  oesuclem  7590  oecl  7602  omordi  7631  omwordri  7637  omword2  7639  omordlim  7642  omlimcl  7643  omeulem2  7648  oeordi  7652  oewordri  7657  oelim2  7660  oeoa  7662  oeoe  7664  nnawordi  7686  nnaordex  7703  erth  7776  iiner  7804  pw2f1olem  8049  pw2f1o  8050  onomeneq  8135  onfin2  8137  unxpdomlem2  8150  isinf  8158  findcard2  8185  fipreima  8257  fipwss  8320  cantnfp1lem3  8562  carden2b  8778  carddomi2  8781  infxpenlem  8821  acni2  8854  numacn  8857  alephfp  8916  pwsdompw  9011  ackbij2lem3  9048  cfeq0  9063  cfsuc  9064  cfsmolem  9077  domfin4  9118  axdc3lem2  9258  axdc3lem4  9260  alephreg  9389  fpwwe2  9450  winainflem  9500  r1limwun  9543  inar1  9582  grudomon  9624  nlt1pi  9713  indpi  9714  nqereu  9736  ltbtwnnq  9785  prlem934  9840  prlem936  9854  addgt0sr  9910  leltne  10112  ne0gt0  10127  mullt0  10532  msqgt0  10533  mulne0  10654  divne0  10682  div2neg  10733  ltmul12a  10864  recgt1i  10905  negfi  10956  nn2ge  11030  div4p1lem1div2  11272  nn0lt2  11425  peano5uzi  11451  eluzp1m1  11696  eluzaddi  11699  eluzsubi  11700  uz2m1nn  11748  nn01to3  11766  rpnnen1lem5  11803  rpnnen1lem5OLD  11809  rphalflt  11845  xrleltne  11963  max0sub  12012  xmulpnf1n  12093  xmulge0  12099  xadddi  12110  supxr  12128  supxr2  12129  ixxdisj  12175  ixxun  12176  ixxub  12181  ixxlb  12182  iccgelb  12215  icodisj  12282  difreicc  12289  iccf1o  12301  fzsuc2  12383  fzonmapblen  12497  elfznelfzo  12557  flge0nn0  12604  flge1nn  12605  2submod  12714  modfzo0difsn  12725  seqf1olem2  12824  expubnd  12904  sqlecan  12954  bernneq  12973  bernneq2  12974  expnbnd  12976  discr1  12983  facwordi  13059  faclbnd4lem4  13066  bcpasc  13091  hashgt0n0  13139  elprchashprn2  13167  hash1to3  13256  iswrdi  13292  ffz0iswrd  13315  ccatsymb  13349  ccatass  13354  swrdlend  13413  swrdfv2  13428  swrdspsleq  13431  swrdswrdlem  13441  swrdswrd  13442  swrdswrd0  13444  swrdccatin12lem2b  13467  revccat  13496  revrev  13497  repswccat  13513  2cshw  13540  cshwcsh2id  13555  revco  13561  cshco  13563  s2f1o  13642  s4f1o  13644  wrdlen2i  13667  wwlktovf  13680  ofccat  13689  trclub  13720  sqr0lem  13962  sqrlem2  13965  sqrlem7  13970  max0add  14031  recval  14043  nnabscl  14046  absmax  14050  sqreulem  14080  climi0  14224  lo1bdd2  14236  rlimresb  14277  lo1eq  14280  rlimeq  14281  isercolllem3  14378  climsup  14381  fsumsplit  14452  fsumcom2  14486  fsumcom2OLD  14487  explecnv  14578  fprodser  14660  fprodsplit  14677  fprodcom2  14695  fprodcom2OLD  14696  eftlub  14820  sin02gt0  14903  rpnnen2lem10  14933  dvdsleabs2  15015  mulmoddvds  15032  odd2np1  15046  oexpneg  15050  sqoddm1div8z  15059  bitsf1  15149  sadcaddlem  15160  bitsuz  15177  rplpwr  15257  rppwr  15258  nn0seqcvgd  15264  lcmneg  15297  qredeq  15352  dvdsnprmd  15384  oddprmge3  15393  isprm7  15401  qgt0numnn  15440  phibndlem  15456  hashgcdeq  15475  reumodprminv  15490  coprimeprodsq2  15495  pythagtrip  15520  dvdsprmpweqle  15571  fldivp1  15582  unbenlem  15593  4sqlem9  15631  4sqlem15  15644  4sqlem16  15645  vdwlem6  15671  vdwlem10  15675  vdwlem11  15676  vdwlem13  15678  vdw  15679  prmgaplem7  15742  prmgaplem8  15743  cshwshashlem1  15783  mreuni  16241  cidpropd  16351  subsubc  16494  ffthiso  16570  fuciso  16616  setcmon  16718  setcepi  16719  catciso  16738  funcestrcsetclem7  16767  funcestrcsetclem8  16768  setc1strwun  16774  funcsetcestrclem7  16782  hofcl  16880  hofpropd  16888  yonedalem4c  16898  yonedainv  16902  issstrmgm  17233  imasmnd  17309  pwsco1mhm  17351  imasgrp  17512  subginv  17582  subgmulg  17589  eqger  17625  subgga  17714  orbstafun  17725  orbsta  17727  symggrp  17801  psgnsn  17921  dfod2  17962  gexval  17974  gex1  17987  sylow2blem1  18016  sylow3lem1  18023  pj1eu  18090  efgredlema  18134  frgp0  18154  frgpmhm  18159  odadd1  18232  0cyg  18275  gsumzres  18291  gsumzsplit  18308  gsummptfzcl  18349  dprd2dlem1  18421  dprd2da  18422  dmdprdsplit2  18426  dprdsplit  18428  pgpfaclem3  18463  ablfac2  18469  imasring  18600  rhmf1o  18713  kerf1hrm  18724  subrg1  18771  abvneg  18815  lmhmf1o  19027  lmhmima  19028  reslmhm2b  19035  pwssplit0  19039  pwssplit1  19040  lsmspsn  19065  lspdisj  19106  lidlmcl  19198  isnzr2hash  19245  fidomndrnglem  19287  mplsubglem  19415  mplmonmul  19445  mplbas2  19451  subrgascl  19479  subrgasclcl  19480  evlsval2  19501  mpfind  19517  lply1binomsc  19658  absabv  19784  f1lindf  20142  mat0dimscm  20256  scmataddcl  20303  scmatsubcl  20304  smatvscl  20311  mdetunilem8  20406  chfacfscmul0  20644  chfacfscmulfsupp  20645  chfacfscmulgsum  20646  chfacfpmmul0  20648  chfacfpmmulfsupp  20649  chfacfpmmulgsum  20650  cpmidpmatlem3  20658  chcoeffeqlem  20671  cayleyhamilton0  20675  cayleyhamiltonALT  20677  cayleyhamilton1  20678  elcls  20858  clsndisj  20860  isclo2  20873  neiuni  20907  neissex  20912  neiptopreu  20918  tgrest  20944  neitr  20965  tgcnp  21038  lmfpm  21080  lmcl  21082  lmss  21083  lmff  21086  ist1-2  21132  cnt1  21135  cmpsublem  21183  clsconn  21214  locfindis  21314  kgeni  21321  kgenidm  21331  txcnpi  21392  ptpjopn  21396  ptclsg  21399  txcmplem1  21425  qtoptop2  21483  qtoptopon  21488  r0sep  21532  ptunhmeo  21592  t0kq  21602  fsubbas  21652  neifil  21665  uffixsn  21710  ufildr  21716  rnelfm  21738  isfcls2  21798  uffclsflim  21816  alexsublem  21829  cnextfun  21849  cnextfvval  21850  cnextf  21851  cnextcn  21852  tmdcn2  21874  symgtgp  21886  tsmssplit  21936  ustuni  22011  trust  22014  utoptop  22019  restutop  22022  restutopopn  22023  ustuqtop1  22026  ustuqtop2  22027  ustuqtop3  22028  ustuqtop4  22029  utop2nei  22035  utop3cls  22036  ucncn  22070  trcfilu  22079  cfiluweak  22080  psmetdmdm  22091  xmeter  22219  prdsbl  22277  neibl  22287  methaus  22306  prdsxmslem2  22315  metustto  22339  metustexhalf  22342  metust  22344  cfilucfil  22345  psmetutop  22353  tngngp2  22437  tngngp  22439  tgqioo  22584  xrsxmet  22593  icccmplem1  22606  icccmplem2  22607  cnmpt2pc  22708  iihalf2  22713  icoopnst  22719  iocopnst  22720  xrhmeo  22726  lebnumlem1  22741  lebnumlem3  22743  pi1blem  22820  pi1grplem  22830  pi1xfrf  22834  pi1xfr  22836  pi1xfrcnvlem  22837  pi1cof  22840  pi1coghm  22842  cmetcaulem  23067  causs  23077  metcld  23085  lmcau  23092  rrxcph  23161  minveclem4  23184  ivthlem2  23202  ivthlem3  23203  ivthicc  23208  ovolshftlem1  23258  ovolicc1  23265  ovolicopnf  23273  volfiniun  23296  uniioombllem3  23334  dyaddisjlem  23344  vitalilem2  23359  itg1ge0  23434  mbfi1fseqlem3  23465  xrge0f  23479  itg2seq  23490  itg2monolem1  23498  itg2addlem  23506  itg2gt0  23508  iblcnlem  23536  itgss3  23562  itgsplit  23583  dvnff  23667  dvferm2  23731  dvlip2  23739  dveq0  23744  dvge0  23750  dvcnvre  23763  dvfsumle  23765  dvfsumabs  23767  dvfsumlem2  23771  ftc1lem2  23780  ftc1lem4  23783  ftc1lem5  23784  ftc1cn  23787  ftc2  23788  itgsubstlem  23792  coe1mul3  23840  ply1divex  23877  dgrlem  23966  dgrlb  23973  coemulhi  23991  dgrlt  24003  dgrmul  24007  plydivlem4  24032  fta1  24044  aaliou2b  24077  taylplem2  24099  dvtaylp  24105  ulmcau  24130  tanabsge  24239  sinq12gt0  24240  argimgt0  24339  cxplea  24423  cxple2  24424  cxpsqrt  24430  cxpaddlelem  24473  loglesqrt  24480  logrec  24482  ang180lem2  24521  lawcos  24527  asinlem3a  24578  asinlem3  24579  asinsin  24600  atanlogaddlem  24621  atanlogadd  24622  atanlogsub  24624  atantan  24631  atanbnd  24634  atantayl2  24646  efrlim  24677  wilthlem2  24776  basellem2  24789  sqfpc  24844  ppieq0  24883  sqff1o  24889  fsumdvdscom  24892  ppiub  24910  chpeq0  24914  chtleppi  24916  fsumvma  24919  fsumvma2  24920  mersenne  24933  dchrabs2  24968  dchr1re  24969  dchrpt  24973  lgsdilem  25030  lgsdinn0  25051  gausslemma2dlem0b  25063  gausslemma2dlem1a  25071  gausslemma2dlem5  25077  gausslemma2dlem6  25078  lgsquad3  25093  m1lgs  25094  2lgslem1a  25097  2lgslem1  25100  2lgslem3a1  25106  2lgslem3b1  25107  2lgslem3c1  25108  2lgslem3d1  25109  2sqlem6  25129  rpvmasumlem  25157  dchrisumlem3  25161  dchrisum0flblem1  25178  pntibndlem2a  25260  pntlem3  25279  padicabv  25300  ercgrg  25393  tglnunirn  25424  tglineeltr  25507  mirln2  25553  mirbtwnhl  25556  isperp2  25591  outpasch  25628  lnopp2hpgb  25636  ttgbtwnid  25745  axcontlem2  25826  axcontlem12  25836  upgredg  26013  fusgrfisstep  26202  nbupgrres  26247  usgrnbcnvfv  26248  nbusgredgeu  26249  nbcplgr  26311  cusgrexi  26320  cusgrsizeinds  26329  vtxdgoddnumeven  26430  uhgr0edg0rgr  26450  wlkl1loop  26515  upgriswlk  26518  usgr2pthlem  26640  cyclnspth  26676  wspthnp  26718  elwwlks2ons3  26829  elwspths2on  26834  usgr2wspthons3  26838  clwlkclwwlklem2a4  26879  clwlkclwwlk2  26885  clwwlksn1loop  26889  clwwlksf1  26897  clwwisshclwws  26908  eleclclwwlksnlem2  26919  clwlksfclwwlk2wrd  26938  clwlksf1clwwlklem3  26947  clwlksf1clwwlklem  26948  1pthon2v  26993  upgr3v3e3cycl  27020  upgreupthi  27048  eupth2lemb  27077  frgrncvvdeqlem7  27149  frgrncvvdeqlem8  27150  frgrncvvdeqlem9  27151  frgrwopreglem4  27157  numclwwlkovf2ex  27191  numclwwlk2lem1  27206  frgrreggt1  27221  frgrregord013  27223  cnnv  27502  nmounbseqi  27602  nmounbseqiALT  27603  nmlnogt0  27622  nmblolbii  27624  blocnilem  27629  ajmoi  27684  minvecolem4  27706  hhnv  27992  norm1  28076  hhssnv  28091  pjhtheu  28223  pjpreeq  28227  spanunsni  28408  fh1  28447  fh2  28448  cm2j  28449  chscllem4  28469  pjid  28524  adjmo  28661  eleigveccl  28788  eigvalcl  28790  eigvec1  28791  eighmre  28792  eighmorth  28793  nmop0h  28820  nmbdoplbi  28853  nmcoplbi  28857  nmophmi  28860  lncnopbd  28866  nmbdfnlbi  28878  nmcfnlbi  28881  cnlnadjeui  28906  branmfn  28934  rnbra  28936  nmopleid  28968  strlem5  29084  hstrlem5  29092  dmdbr3  29134  dmdbr4  29135  mdsl3  29145  hatomistici  29191  cvexchlem  29197  chirredlem1  29219  chirredlem2  29220  chirredi  29223  atcvat3i  29225  atcvat4i  29226  atabsi  29230  mdsymlem1  29232  mdsymlem3  29234  mdsymlem5  29236  dmdbr5ati  29251  cdj1i  29262  foresf1o  29315  rabfodom  29316  elabreximd  29320  elpreq  29332  f1o3d  29404  acunirnmpt2f  29434  disjdsct  29454  1stpreimas  29457  fcobij  29474  fpwrelmapffslem  29481  nn0sqeq1  29487  xrofsup  29507  eliccelico  29513  elicoelioo  29514  numdenneg  29537  fsumiunle  29549  dpadd3  29594  threehalves  29597  xrge0addgt0  29665  xrge0adddir  29666  xrge0npcan  29668  omndmul3  29687  submarchi  29714  archirng  29716  archirngz  29717  archiexdiv  29718  archiabllem1a  29719  1smat1  29844  madjusmdetlem2  29868  locfinreflem  29881  metideq  29910  unitdivcld  29921  cnre2csqlem  29930  ordtconnlem1  29944  fmcncfil  29951  lmxrge0  29972  pl1cn  29975  zrhunitpreima  29996  elzdif0  29998  qqhval2lem  29999  qqhf  30004  indf1ofs  30062  esumfsup  30106  esumpcvgval  30114  esum2dlem  30128  esum2d  30129  esumiun  30130  sigasspw  30153  issgon  30160  ispisys2  30190  meascnbl  30256  voliune  30266  volfiniune  30267  omssubaddlem  30335  carsggect  30354  carsgclctunlem2  30355  oddpwdc  30390  eulerpartlems  30396  eulerpartlemgvv  30412  ballotlemfrcn0  30565  sgncl  30574  sgnneg  30576  sgn3da  30577  sgnmul  30578  sgnsub  30580  gsumnunsn  30589  signsplypnf  30601  signsply0  30602  signslema  30613  signstfvneq0  30623  signsvfpn  30636  signsvfnn  30637  repr0  30663  reprlt  30671  reprgt  30673  reprinfz1  30674  chtvalz  30681  breprexplemc  30684  hgt750lemb  30708  hgt750leme  30710  bnj563  30787  bnj1001  31002  subfacp1lem5  31140  subfacp1lem6  31141  erdszelem9  31155  ptpconn  31189  resconn  31202  cvmlift3lem7  31281  msrrcl  31414  trpredrec  31712  scutbdaylt  31896  btwnintr  32101  btwnouttr  32106  cgrxfr  32137  btwnconn1lem12  32180  colinbtwnle  32200  lineelsb2  32230  nn0prpwlem  32292  neibastop3  32332  onintopssconn  32414  bj-restsnss  33011  bj-restsnss2  33012  taupilem1  33138  relowlssretop  33182  finxpsuclem  33205  unccur  33363  lindsenlbs  33375  matunitlindflem1  33376  matunitlindflem2  33377  poimirlem2  33382  poimirlem8  33388  poimirlem14  33394  poimirlem15  33395  poimirlem17  33397  poimirlem20  33400  poimirlem22  33402  poimirlem24  33404  poimirlem25  33405  poimirlem27  33407  poimirlem28  33408  poimirlem31  33411  heicant  33415  mblfinlem2  33418  itg2gt0cn  33436  itgaddnclem2  33440  ftc1cnnclem  33454  ftc1cnnc  33455  ftc1anclem2  33457  ftc1anclem5  33460  ftc1anclem7  33462  ftc1anc  33464  ftc2nc  33465  dvasin  33467  areacirclem5  33475  areacirc  33476  fdc  33512  incsequz  33515  blbnd  33557  prdstotbnd  33564  cnpwstotbnd  33567  ismtyres  33578  rngohomf  33736  rngohom1  33738  rngohomadd  33739  rngohommul  33740  idlss  33786  idl0cl  33788  idladdcl  33789  idllmulcl  33790  idlrmulcl  33791  maxidlnr  33812  maxidlmax  33813  smprngopr  33822  pridlc  33841  ac6s6f  33952  lshpnel2N  34091  islsati  34100  lkr0f  34200  lfl1dim  34227  lfl1dim2N  34228  omlfh1N  34364  leat  34399  atlatmstc  34425  cvlatexch3  34444  lnnat  34532  cvrat3  34547  cvrat4  34548  3dim3  34574  dalem4  34770  dalem39  34816  paddasslem12  34936  psubcliN  35043  pmapojoinN  35073  lhpm0atN  35134  lhprelat3N  35145  trlnid  35285  trlval3  35293  cdleme22b  35448  trljco  35847  diaglbN  36163  dibvalrel  36271  dicvalrelN  36293  diclspsn  36302  dih1dimatlem  36437  dihlatat  36445  lcfl6  36608  lcfl8  36610  lcfrvalsnN  36649  lcfrlem9  36658  mapdheq2  36837  hlhillcs  37069  hlhilhillem  37071  mzpindd  37128  lzunuz  37150  2rexfrabdioph  37179  irrapxlem3  37207  pellexlem2  37213  pellexlem5  37216  pell1234qrreccl  37237  pell14qrdich  37252  pell1qrge1  37253  elpell1qr2  37255  reglogltb  37274  reglogleb  37275  rmxycomplete  37301  2nn0ind  37329  congabseq  37360  acongrep  37366  acongeq  37369  jm2.22  37381  jm2.26lem3  37387  pw2f1ocnv  37423  limsuc2  37430  fnwe2lem3  37441  aomclem6  37448  kercvrlsm  37472  pwssplit4  37478  lpirlnr  37506  rfovcnvf1od  38118  dssmapnvod  38134  cvgdvgrat  38332  radcnvrat  38333  dvconstbi  38353  bccbc  38364  bi2imp  38508  ax6e2ndeqALT  38987  mulltgt0  39001  refsumcn  39009  cncmpmax  39011  mapdm0OLD  39199  unirnmapsn  39222  icoiccdif  39553  climinf  39638  climreeq  39645  climeldmeq  39697  coskpi2  39840  cosknegpi  39843  icccncfext  39863  dvmptfprodlem  39922  volioore  39970  stoweidlem27  40007  stoweidlem29  40009  stoweidlem31  40011  stoweidlem34  40014  stoweidlem48  40028  stoweidlem59  40039  fourierdlem109  40195  fourierswlem  40210  elaa2  40214  etransclem37  40251  hspmbllem2  40604  smflimmpt  40779  sigarcol  40816  reuan  40943  ndmaovg  41027  subsubelfzo0  41099  iccelpart  41133  fargshiftf1  41141  fargshiftfo  41142  pfxeq  41169  pfxccatin12lem1  41188  repswpfx  41201  fmtno4prmfac  41249  2pwp1prmfmtno  41269  sfprmdvdsmersenne  41285  lighneallem3  41289  proththd  41296  evenm1odd  41317  evenp1odd  41318  nnoALTV  41371  stgoldbwt  41429  sbgoldbst  41431  nnsum4primeseven  41453  nnsum4primesevenALTV  41454  bgoldbtbndlem2  41459  upgrwlkupwlk  41486  rnghmf1o  41668  rnghmsubcsetclem1  41740  zrinitorngc  41765  zrtermorngc  41766  rhmsubcsetclem1  41786  rhmsubcrngclem1  41792  funcringcsetcALTV2lem8  41808  funcringcsetclem8ALTV  41831  zrtermoringc  41835  ply1sclrmsm  41936  lincfsuppcl  41967  zofldiv2  42090  elbigolo1  42116  blennn0em1  42150  blennn0e2  42153  dig2nn0ld  42163  nn0sumshdiglem2  42181
  Copyright terms: Public domain W3C validator