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

Theorem biimpa 502
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 444 1 ((𝜑𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  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 197  df-an 385
This theorem is referenced by:  simprbda  654  simplbda  655  pm5.1  938  bimsc1  1017  biimp3a  1581  equsex  2437  euor  2650  euan  2668  cgsexg  3378  cgsex2g  3379  cgsex4g  3380  ceqsex  3381  sbciegft  3607  sbeqalb  3629  syl5sseq  3794  elpwunsn  4368  ralxfr2d  5031  propeqop  5118  euotd  5123  relop  5428  elsnxp  5838  sspred  5849  fnbr  6154  f1o00  6332  foelrni  6406  dffv2  6433  iinpreima  6508  funressn  6589  fnex  6645  f1prex  6702  weniso  6767  riotaeqimp  6797  f1ocnv2d  7051  ofrval  7072  limsssuc  7215  resiexg  7267  eloprabi  7400  1stconst  7433  2ndconst  7434  frxp  7455  poxp  7457  smodm2  7621  smoiso  7628  tz7.44lem1  7670  oev2  7772  oesuclem  7774  oecl  7786  omordi  7815  omwordri  7821  omword2  7823  omordlim  7826  omlimcl  7827  omeulem2  7832  oeordi  7836  oewordri  7841  oelim2  7844  oeoa  7846  oeoe  7848  nnawordi  7870  nnaordex  7887  erth  7958  iiner  7986  pw2f1olem  8229  pw2f1o  8230  onomeneq  8315  onfin2  8317  unxpdomlem2  8330  isinf  8338  findcard2  8365  fipreima  8437  fipwss  8500  preleqALT  8685  cantnfp1lem3  8750  carden2b  8983  carddomi2  8986  infxpenlem  9026  acni2  9059  numacn  9062  alephfp  9121  pwsdompw  9218  ackbij2lem3  9255  cfeq0  9270  cfsuc  9271  cfsmolem  9284  domfin4  9325  axdc3lem2  9465  axdc3lem4  9467  alephreg  9596  fpwwe2  9657  winainflem  9707  r1limwun  9750  inar1  9789  grudomon  9831  nlt1pi  9920  indpi  9921  nqereu  9943  ltbtwnnq  9992  prlem934  10047  prlem936  10061  addgt0sr  10117  leltne  10319  ne0gt0  10334  mullt0  10739  msqgt0  10740  mulne0  10861  divne0  10889  div2neg  10940  ltmul12a  11071  recgt1i  11112  negfi  11163  nn2ge  11237  div4p1lem1div2  11479  nn0lt2  11632  peano5uzi  11658  eluzp1m1  11903  eluzaddi  11906  eluzsubi  11907  uz2m1nn  11956  nn01to3  11974  rpnnen1lem5  12011  rpnnen1lem5OLD  12017  rphalflt  12053  xrleltne  12171  max0sub  12220  xmulpnf1n  12301  xmulge0  12307  xadddi  12318  supxr  12336  supxr2  12337  ixxdisj  12383  ixxun  12384  ixxub  12389  ixxlb  12390  iccgelb  12423  icodisj  12490  difreicc  12497  iccf1o  12509  fzsuc2  12591  fzonmapblen  12708  elfznelfzo  12767  flge0nn0  12815  flge1nn  12816  2submod  12925  modfzo0difsn  12936  seqf1olem2  13035  expubnd  13115  sqlecan  13165  bernneq  13184  bernneq2  13185  expnbnd  13187  discr1  13194  facwordi  13270  faclbnd4lem4  13277  bcpasc  13302  hashgt0n0  13348  elprchashprn2  13376  hash1to3  13465  iswrdi  13495  ffz0iswrd  13518  ccatsymb  13554  ccatass  13560  swrdlend  13631  swrdfv2  13646  swrdspsleq  13649  swrdswrdlem  13659  swrdswrd  13660  swrdswrd0  13662  swrdccatin12lem2b  13686  revccat  13715  revrev  13716  repswccat  13732  2cshw  13759  cshwcsh2id  13774  revco  13780  cshco  13782  s2f1o  13861  s4f1o  13863  wrdlen2i  13887  wwlktovf  13900  ofccat  13909  trclub  13938  sqr0lem  14180  sqrlem2  14183  sqrlem7  14188  max0add  14249  recval  14261  nnabscl  14264  absmax  14268  sqreulem  14298  climi0  14442  lo1bdd2  14454  rlimresb  14495  lo1eq  14498  rlimeq  14499  isercolllem3  14596  climsup  14599  fsumsplit  14670  fsumcom2  14704  fsumcom2OLD  14705  explecnv  14796  fprodser  14878  fprodsplit  14895  fprodcom2  14913  fprodcom2OLD  14914  eftlub  15038  sin02gt0  15121  rpnnen2lem10  15151  dvdsleabs2  15236  odd2np1  15267  oexpneg  15271  sqoddm1div8z  15280  bitsf1  15370  sadcaddlem  15381  bitsuz  15398  rplpwr  15478  rppwr  15479  nn0seqcvgd  15485  lcmneg  15518  qredeq  15573  dvdsnprmd  15605  oddprmge3  15614  isprm7  15622  qgt0numnn  15661  phibndlem  15677  hashgcdeq  15696  reumodprminv  15711  coprimeprodsq2  15716  pythagtrip  15741  dvdsprmpweqle  15792  fldivp1  15803  unbenlem  15814  4sqlem9  15852  4sqlem15  15865  4sqlem16  15866  vdwlem6  15892  vdwlem10  15896  vdwlem11  15897  vdwlem13  15899  vdw  15900  prmgaplem7  15963  prmgaplem8  15964  cshwshashlem1  16004  mreuni  16462  cidpropd  16571  subsubc  16714  ffthiso  16790  fuciso  16836  setcmon  16938  setcepi  16939  catciso  16958  funcestrcsetclem7  16987  funcestrcsetclem8  16988  setc1strwun  16994  funcsetcestrclem7  17002  hofcl  17100  hofpropd  17108  yonedalem4c  17118  yonedainv  17122  issstrmgm  17453  imasmnd  17529  pwsco1mhm  17571  imasgrp  17732  subginv  17802  subgmulg  17809  eqger  17845  subgga  17933  orbstafun  17944  orbsta  17946  symggrp  18020  psgnsn  18140  dfod2  18181  gexval  18193  gex1  18206  sylow2blem1  18235  sylow3lem1  18242  pj1eu  18309  efgredlema  18353  frgp0  18373  frgpmhm  18378  odadd1  18451  0cyg  18494  gsumzres  18510  gsumzsplit  18527  gsummptfzcl  18568  dprd2dlem1  18640  dprd2da  18641  dmdprdsplit2  18645  dprdsplit  18647  pgpfaclem3  18682  ablfac2  18688  imasring  18819  rhmf1o  18934  kerf1hrm  18945  subrg1  18992  abvneg  19036  lmhmf1o  19248  lmhmima  19249  reslmhm2b  19256  pwssplit0  19260  pwssplit1  19261  lsmspsn  19286  lspdisj  19327  lidlmcl  19419  isnzr2hash  19466  fidomndrnglem  19508  mplsubglem  19636  mplmonmul  19666  mplbas2  19672  subrgascl  19700  subrgasclcl  19701  evlsval2  19722  mpfind  19738  lply1binomsc  19879  absabv  20005  f1lindf  20363  mat0dimscm  20477  scmataddcl  20524  scmatsubcl  20525  smatvscl  20532  mdetunilem8  20627  chfacfscmul0  20865  chfacfscmulfsupp  20866  chfacfscmulgsum  20867  chfacfpmmul0  20869  chfacfpmmulfsupp  20870  chfacfpmmulgsum  20871  cpmidpmatlem3  20879  chcoeffeqlem  20892  cayleyhamilton0  20896  cayleyhamiltonALT  20898  cayleyhamilton1  20899  elcls  21079  clsndisj  21081  isclo2  21094  neiuni  21128  neissex  21133  neiptopreu  21139  tgrest  21165  neitr  21186  tgcnp  21259  lmfpm  21301  lmcl  21303  lmss  21304  lmff  21307  ist1-2  21353  cnt1  21356  cmpsublem  21404  clsconn  21435  locfindis  21535  kgeni  21542  kgenidm  21552  txcnpi  21613  ptpjopn  21617  ptclsg  21620  txcmplem1  21646  qtoptop2  21704  qtoptopon  21709  r0sep  21753  ptunhmeo  21813  t0kq  21823  fsubbas  21872  neifil  21885  uffixsn  21930  ufildr  21936  rnelfm  21958  isfcls2  22018  uffclsflim  22036  alexsublem  22049  cnextfun  22069  cnextfvval  22070  cnextf  22071  cnextcn  22072  tmdcn2  22094  symgtgp  22106  tsmssplit  22156  ustuni  22231  trust  22234  utoptop  22239  restutop  22242  restutopopn  22243  ustuqtop1  22246  ustuqtop2  22247  ustuqtop3  22248  ustuqtop4  22249  utop2nei  22255  utop3cls  22256  ucncn  22290  trcfilu  22299  cfiluweak  22300  psmetdmdm  22311  xmeter  22439  prdsbl  22497  neibl  22507  methaus  22526  prdsxmslem2  22535  metustto  22559  metustexhalf  22562  metust  22564  cfilucfil  22565  psmetutop  22573  tngngp2  22657  tngngp  22659  tgqioo  22804  xrsxmet  22813  icccmplem1  22826  icccmplem2  22827  cnmpt2pc  22928  iihalf2  22933  icoopnst  22939  iocopnst  22940  xrhmeo  22946  lebnumlem1  22961  lebnumlem3  22963  pi1blem  23039  pi1grplem  23049  pi1xfrf  23053  pi1xfr  23055  pi1xfrcnvlem  23056  pi1cof  23059  pi1coghm  23061  cmetcaulem  23286  causs  23296  metcld  23304  lmcau  23311  rrxcph  23380  minveclem4  23403  ivthlem2  23421  ivthlem3  23422  ivthicc  23427  ovolshftlem1  23477  ovolicc1  23484  ovolicopnf  23492  volfiniun  23515  uniioombllem3  23553  dyaddisjlem  23563  vitalilem2  23577  itg1ge0  23652  mbfi1fseqlem3  23683  xrge0f  23697  itg2seq  23708  itg2monolem1  23716  itg2addlem  23724  itg2gt0  23726  iblcnlem  23754  itgss3  23780  itgsplit  23801  dvnff  23885  dvferm2  23949  dvlip2  23957  dveq0  23962  dvge0  23968  dvcnvre  23981  dvfsumle  23983  dvfsumabs  23985  dvfsumlem2  23989  ftc1lem2  23998  ftc1lem4  24001  ftc1lem5  24002  ftc1cn  24005  ftc2  24006  itgsubstlem  24010  coe1mul3  24058  ply1divex  24095  dgrlem  24184  dgrlb  24191  coemulhi  24209  dgrlt  24221  dgrmul  24225  plydivlem4  24250  fta1  24262  aaliou2b  24295  taylplem2  24317  dvtaylp  24323  ulmcau  24348  tanabsge  24457  sinq12gt0  24458  argimgt0  24557  cxplea  24641  cxple2  24642  cxpsqrt  24648  cxpaddlelem  24691  loglesqrt  24698  logrec  24700  ang180lem2  24739  lawcos  24745  asinlem3a  24796  asinlem3  24797  asinsin  24818  atanlogaddlem  24839  atanlogadd  24840  atanlogsub  24842  atantan  24849  atanbnd  24852  atantayl2  24864  efrlim  24895  wilthlem2  24994  basellem2  25007  sqfpc  25062  ppieq0  25101  sqff1o  25107  fsumdvdscom  25110  ppiub  25128  chpeq0  25132  chtleppi  25134  fsumvma  25137  fsumvma2  25138  mersenne  25151  dchrabs2  25186  dchr1re  25187  dchrpt  25191  lgsdilem  25248  lgsdinn0  25269  gausslemma2dlem0b  25281  gausslemma2dlem1a  25289  gausslemma2dlem5  25295  gausslemma2dlem6  25296  lgsquad3  25311  m1lgs  25312  2lgslem1a  25315  2lgslem1  25318  2lgslem3a1  25324  2lgslem3b1  25325  2lgslem3c1  25326  2lgslem3d1  25327  2sqlem6  25347  rpvmasumlem  25375  dchrisumlem3  25379  dchrisum0flblem1  25396  pntibndlem2a  25478  pntlem3  25497  padicabv  25518  ercgrg  25611  tglnunirn  25642  tglineeltr  25725  mirln2  25771  mirbtwnhl  25774  isperp2  25809  outpasch  25846  lnopp2hpgb  25854  ttgbtwnid  25963  axcontlem2  26044  axcontlem12  26054  upgredg  26231  fusgrfisstep  26420  nbupgrres  26464  usgrnbcnvfv  26465  nbusgredgeu  26466  nbcplgr  26540  cusgrexi  26549  structtocusgr  26552  cusgrsizeinds  26558  vtxdgoddnumeven  26659  uhgr0edg0rgr  26679  wlkl1loop  26744  upgriswlk  26747  usgr2pthlem  26869  cyclnspth  26906  wwlknvtx  26948  wspthnp  26954  elwwlks2ons3  27075  elwwlks2ons3OLD  27076  elwspths2on  27081  usgr2wspthons3  27086  clwlkclwwlklem2a4  27120  clwlkclwwlk2  27126  clwlkclwwlkfolem  27130  clwlkclwwlkf1  27133  clwwisshclwws  27138  loopclwwlkn1b  27171  clwwlkf1  27178  wwlksext2clwwlk  27187  clwwnisshclwwsn  27190  eleclclwwlknlem2  27192  clwlksfclwwlk2wrdOLD  27212  clwlksf1clwwlklem3OLD  27221  clwlksf1clwwlklemOLD  27222  1pthon2v  27305  upgr3v3e3cycl  27332  upgreupthi  27360  eupth2lemb  27389  frgrncvvdeqlem7  27459  frgrncvvdeqlem8  27460  frgrncvvdeqlem9  27461  clwwnonrepclwwnon  27502  numclwwlkovh  27534  numclwwlk2lem1  27537  numclwwlk2lem1OLD  27544  frgrreggt1  27561  frgrregord013  27563  cnnv  27841  nmounbseqi  27941  nmounbseqiALT  27942  nmlnogt0  27961  nmblolbii  27963  blocnilem  27968  ajmoi  28023  minvecolem4  28045  hhnv  28331  norm1  28415  hhssnv  28430  pjhtheu  28562  pjpreeq  28566  spanunsni  28747  fh1  28786  fh2  28787  cm2j  28788  chscllem4  28808  pjid  28863  adjmo  29000  eleigveccl  29127  eigvalcl  29129  eigvec1  29130  eighmre  29131  eighmorth  29132  nmop0h  29159  nmbdoplbi  29192  nmcoplbi  29196  nmophmi  29199  lncnopbd  29205  nmbdfnlbi  29217  nmcfnlbi  29220  cnlnadjeui  29245  branmfn  29273  rnbra  29275  nmopleid  29307  strlem5  29423  hstrlem5  29431  dmdbr3  29473  dmdbr4  29474  mdsl3  29484  hatomistici  29530  cvexchlem  29536  chirredlem1  29558  chirredlem2  29559  chirredi  29562  atcvat3i  29564  atcvat4i  29565  atabsi  29569  mdsymlem1  29571  mdsymlem3  29573  mdsymlem5  29575  dmdbr5ati  29590  cdj1i  29601  foresf1o  29650  rabfodom  29651  elabreximd  29655  elpreq  29667  f1o3d  29740  acunirnmpt2f  29770  disjdsct  29789  1stpreimas  29792  fcobij  29809  fpwrelmapffslem  29816  nn0sqeq1  29822  xrofsup  29842  eliccelico  29848  elicoelioo  29849  numdenneg  29872  fsumiunle  29884  dpadd3  29929  threehalves  29932  xrge0addgt0  30000  xrge0adddir  30001  xrge0npcan  30003  omndmul3  30022  submarchi  30049  archirng  30051  archirngz  30052  archiexdiv  30053  archiabllem1a  30054  1smat1  30179  madjusmdetlem2  30203  locfinreflem  30216  metideq  30245  unitdivcld  30256  cnre2csqlem  30265  ordtconnlem1  30279  fmcncfil  30286  lmxrge0  30307  pl1cn  30310  zrhunitpreima  30331  elzdif0  30333  qqhval2lem  30334  qqhf  30339  indf1ofs  30397  esumfsup  30441  esumpcvgval  30449  esum2dlem  30463  esum2d  30464  esumiun  30465  sigasspw  30488  issgon  30495  ispisys2  30525  meascnbl  30591  voliune  30601  volfiniune  30602  omssubaddlem  30670  carsggect  30689  carsgclctunlem2  30690  oddpwdc  30725  eulerpartlems  30731  eulerpartlemgvv  30747  ballotlemfrcn0  30900  sgncl  30909  sgnneg  30911  sgn3da  30912  sgnmul  30913  sgnsub  30915  gsumnunsn  30924  signsplypnf  30936  signsply0  30937  signslema  30948  signstfvneq0  30958  signsvfpn  30971  signsvfnn  30972  repr0  30998  reprlt  31006  reprgt  31008  reprinfz1  31009  chtvalz  31016  breprexplemc  31019  hgt750lemb  31043  hgt750leme  31045  bnj563  31120  bnj1001  31335  subfacp1lem5  31473  subfacp1lem6  31474  erdszelem9  31488  ptpconn  31522  resconn  31535  cvmlift3lem7  31614  msrrcl  31747  trpredrec  32043  scutbdaylt  32228  btwnintr  32432  btwnouttr  32437  cgrxfr  32468  btwnconn1lem12  32511  colinbtwnle  32531  lineelsb2  32561  nn0prpwlem  32623  neibastop3  32663  onintopssconn  32745  bj-restsnss  33342  bj-restsnss2  33343  taupilem1  33478  relowlssretop  33522  finxpsuclem  33545  unccur  33705  lindsenlbs  33717  matunitlindflem1  33718  matunitlindflem2  33719  poimirlem2  33724  poimirlem8  33730  poimirlem14  33736  poimirlem15  33737  poimirlem17  33739  poimirlem20  33742  poimirlem22  33744  poimirlem24  33746  poimirlem25  33747  poimirlem27  33749  poimirlem28  33750  poimirlem31  33753  heicant  33757  mblfinlem2  33760  itg2gt0cn  33778  itgaddnclem2  33782  ftc1cnnclem  33796  ftc1cnnc  33797  ftc1anclem2  33799  ftc1anclem5  33802  ftc1anclem7  33804  ftc1anc  33806  ftc2nc  33807  dvasin  33809  areacirclem5  33817  areacirc  33818  fdc  33854  incsequz  33857  blbnd  33899  prdstotbnd  33906  cnpwstotbnd  33909  ismtyres  33920  rngohomf  34078  rngohom1  34080  rngohomadd  34081  rngohommul  34082  idlss  34128  idl0cl  34130  idladdcl  34131  idllmulcl  34132  idlrmulcl  34133  maxidlnr  34154  maxidlmax  34155  smprngopr  34164  pridlc  34183  ac6s6f  34294  lshpnel2N  34775  islsati  34784  lkr0f  34884  lfl1dim  34911  lfl1dim2N  34912  omlfh1N  35048  leat  35083  atlatmstc  35109  cvlatexch3  35128  lnnat  35216  cvrat3  35231  cvrat4  35232  3dim3  35258  dalem4  35454  dalem39  35500  paddasslem12  35620  psubcliN  35727  pmapojoinN  35757  lhpm0atN  35818  lhprelat3N  35829  trlnid  35969  trlval3  35977  cdleme22b  36131  trljco  36530  diaglbN  36846  dibvalrel  36954  dicvalrelN  36976  diclspsn  36985  dih1dimatlem  37120  dihlatat  37128  lcfl6  37291  lcfl8  37293  lcfrvalsnN  37332  lcfrlem9  37341  mapdheq2  37520  hlhillcs  37752  hlhilhillem  37754  mzpindd  37811  lzunuz  37833  2rexfrabdioph  37862  irrapxlem3  37890  pellexlem2  37896  pellexlem5  37899  pell1234qrreccl  37920  pell14qrdich  37935  pell1qrge1  37936  elpell1qr2  37938  reglogltb  37957  reglogleb  37958  rmxycomplete  37984  2nn0ind  38012  congabseq  38043  acongrep  38049  acongeq  38052  jm2.22  38064  jm2.26lem3  38070  pw2f1ocnv  38106  limsuc2  38113  fnwe2lem3  38124  aomclem6  38131  kercvrlsm  38155  pwssplit4  38161  lpirlnr  38189  rfovcnvf1od  38800  dssmapnvod  38816  cvgdvgrat  39014  radcnvrat  39015  dvconstbi  39035  bccbc  39046  bi2imp  39190  ax6e2ndeqALT  39666  mulltgt0  39680  refsumcn  39688  cncmpmax  39690  mapdm0OLD  39882  unirnmapsn  39905  icoiccdif  40253  climinf  40341  climreeq  40348  climeldmeq  40400  coskpi2  40580  cosknegpi  40583  icccncfext  40603  dvmptfprodlem  40662  volioore  40710  stoweidlem27  40747  stoweidlem29  40749  stoweidlem31  40751  stoweidlem34  40754  stoweidlem48  40768  stoweidlem59  40779  fourierdlem109  40935  fourierswlem  40950  elaa2  40954  etransclem37  40991  hspmbllem2  41347  smflimmpt  41522  sigarcol  41559  reuan  41686  ndmaovg  41770  subsubelfzo0  41846  iccelpart  41879  fargshiftf1  41887  fargshiftfo  41888  pfxeq  41914  pfxccatin12lem1  41933  repswpfx  41946  fmtnoprmfac1lem  41986  fmtno4prmfac  41994  2pwp1prmfmtno  42014  sfprmdvdsmersenne  42030  lighneallem3  42034  proththd  42041  evenm1odd  42062  evenp1odd  42063  nnoALTV  42116  stgoldbwt  42174  sbgoldbst  42176  nnsum4primeseven  42198  nnsum4primesevenALTV  42199  bgoldbtbndlem2  42204  upgrwlkupwlk  42231  rnghmf1o  42413  rnghmsubcsetclem1  42485  zrinitorngc  42510  zrtermorngc  42511  rhmsubcsetclem1  42531  rhmsubcrngclem1  42537  funcringcsetcALTV2lem8  42553  funcringcsetclem8ALTV  42576  zrtermoringc  42580  ply1sclrmsm  42681  lincfsuppcl  42712  zofldiv2  42835  elbigolo1  42861  blennn0em1  42895  blennn0e2  42898  dig2nn0ld  42908  nn0sumshdiglem2  42926
  Copyright terms: Public domain W3C validator