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

Theorem biimpa 464
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 220 . 2 (𝜑 → (𝜓𝜒))
32imp 395 1 ((𝜑𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  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 198  df-an 385
This theorem is referenced by:  simprbda  488  simplbda  489  pm5.1  845  bimsc1  861  biimp3a  1586  equsex  2459  euor  2675  euan  2694  cgsexg  3432  cgsex2g  3433  cgsex4g  3434  ceqsex  3435  sbciegft  3664  sbeqalb  3686  syl5sseq  3850  elpwunsn  4417  ralxfr2d  5079  propeqop  5162  euotd  5168  relop  5474  elsnxp  5891  sspred  5901  fnbr  6204  f1o00  6387  foelrni  6465  dffv2  6492  iinpreima  6567  funressn  6650  fnex  6706  f1prex  6763  weniso  6828  riotaeqimp  6858  f1ocnv2d  7116  ofrval  7137  limsssuc  7280  resiexg  7332  eloprabi  7465  1stconst  7499  2ndconst  7500  frxp  7521  poxp  7523  smodm2  7688  smoiso  7695  tz7.44lem1  7737  oev2  7840  oesuclem  7842  oecl  7854  omordi  7883  omwordri  7889  omword2  7891  omordlim  7894  omlimcl  7895  omeulem2  7900  oeordi  7904  oewordri  7909  oelim2  7912  oeoa  7914  oeoe  7916  nnawordi  7938  nnaordex  7955  erth  8026  iiner  8054  pw2f1olem  8303  pw2f1o  8304  onomeneq  8389  onfin2  8391  unxpdomlem2  8404  isinf  8412  findcard2  8439  fipreima  8511  fipwss  8574  preleqALT  8759  cantnfp1lem3  8824  carden2b  9076  carddomi2  9079  infxpenlem  9119  acni2  9152  numacn  9155  alephfp  9214  pwsdompw  9311  ackbij2lem3  9348  cfeq0  9363  cfsuc  9364  cfsmolem  9377  domfin4  9418  axdc3lem2  9558  axdc3lem4  9560  alephreg  9689  fpwwe2  9750  winainflem  9800  r1limwun  9843  inar1  9882  grudomon  9924  nlt1pi  10013  indpi  10014  nqereu  10036  ltbtwnnq  10085  prlem934  10140  prlem936  10154  addgt0sr  10210  leltne  10412  ne0gt0  10427  mullt0  10832  msqgt0  10833  mulne0  10954  divne0  10982  div2neg  11033  ltmul12a  11164  recgt1i  11205  negfi  11256  nn2ge  11331  div4p1lem1div2  11554  nn0lt2  11706  peano5uzi  11732  eluzp1m1  11928  eluzaddi  11931  eluzsubi  11932  uz2m1nn  11982  nn01to3  12000  rpnnen1lem5  12037  rphalflt  12074  xrleltne  12194  max0sub  12245  xmulpnf1n  12326  xmulge0  12332  xadddi  12343  supxr  12361  supxr2  12362  ixxdisj  12408  ixxun  12409  ixxub  12414  ixxlb  12415  iccgelb  12448  icodisj  12518  difreicc  12527  iccf1o  12539  fzsuc2  12621  fzonmapblen  12738  elfznelfzo  12797  flge0nn0  12845  flge1nn  12846  2submod  12955  modfzo0difsn  12966  seqf1olem2  13064  expubnd  13144  sqlecan  13194  bernneq  13213  bernneq2  13214  expnbnd  13216  discr1  13223  facwordi  13296  faclbnd4lem4  13303  bcpasc  13328  hashgt0n0  13374  elprchashprn2  13401  hash1to3  13490  iswrdi  13520  ffz0iswrd  13543  ccatsymb  13579  ccatass  13585  swrdlend  13655  swrdfv2  13670  swrdspsleq  13673  swrdswrdlem  13683  swrdswrd  13684  swrdswrd0  13686  swrdccatin12lem2b  13710  revccat  13739  revrev  13740  repswccat  13756  2cshw  13783  cshwcsh2id  13798  revco  13804  cshco  13806  s2f1o  13885  s4f1o  13887  wrdlen2i  13911  wwlktovf  13924  ofccat  13933  trclub  13962  sqr0lem  14204  sqrlem2  14207  sqrlem7  14212  max0add  14273  recval  14285  nnabscl  14288  absmax  14292  sqreulem  14322  climi0  14466  lo1bdd2  14478  rlimresb  14519  lo1eq  14522  rlimeq  14523  isercolllem3  14620  climsup  14623  fsumsplit  14694  fsumcom2  14728  explecnv  14819  fprodser  14900  fprodsplit  14917  fprodcom2  14935  eftlub  15059  sin02gt0  15142  rpnnen2lem10  15172  dvdsleabs2  15257  odd2np1  15285  oexpneg  15289  sqoddm1div8z  15298  bitsf1  15387  sadcaddlem  15398  bitsuz  15415  rplpwr  15495  rppwr  15496  nn0seqcvgd  15502  lcmneg  15535  qredeq  15589  dvdsnprmd  15621  oddprmge3  15630  isprm7  15637  qgt0numnn  15676  phibndlem  15692  hashgcdeq  15711  reumodprminv  15726  coprimeprodsq2  15731  pythagtrip  15756  dvdsprmpweqle  15807  fldivp1  15818  unbenlem  15829  4sqlem9  15867  4sqlem15  15880  4sqlem16  15881  vdwlem6  15907  vdwlem10  15911  vdwlem11  15912  vdwlem13  15914  vdw  15915  prmgaplem7  15978  prmgaplem8  15979  cshwshashlem1  16014  mreuni  16465  cidpropd  16574  subsubc  16717  ffthiso  16793  fuciso  16839  setcmon  16941  setcepi  16942  catciso  16961  funcestrcsetclem7  16991  funcestrcsetclem8  16992  setc1strwun  16998  funcsetcestrclem7  17006  hofcl  17104  hofpropd  17112  yonedalem4c  17122  yonedainv  17126  issstrmgm  17457  imasmnd  17533  pwsco1mhm  17575  imasgrp  17736  subginv  17803  subgmulg  17810  eqger  17846  subgga  17934  orbstafun  17945  orbsta  17947  symggrp  18021  psgnsn  18141  dfod2  18182  gexval  18194  gex1  18207  sylow2blem1  18236  sylow3lem1  18243  pj1eu  18310  efgredlema  18354  frgp0  18374  frgpmhm  18379  odadd1  18452  0cyg  18495  gsumzres  18511  gsumzsplit  18528  gsummptfzcl  18569  dprd2dlem1  18642  dprd2da  18643  dmdprdsplit2  18647  dprdsplit  18649  pgpfaclem3  18684  ablfac2  18690  imasring  18821  rhmf1o  18936  kerf1hrm  18947  subrg1  18994  abvneg  19038  lmhmf1o  19253  lmhmima  19254  reslmhm2b  19261  pwssplit0  19265  pwssplit1  19266  lsmspsn  19291  lspdisj  19332  lidlmcl  19426  isnzr2hash  19473  fidomndrnglem  19515  mplsubglem  19643  mplmonmul  19673  mplbas2  19679  subrgascl  19706  subrgasclcl  19707  evlsval2  19728  mpfind  19744  lply1binomsc  19885  absabv  20011  f1lindf  20371  mat0dimscm  20486  scmataddcl  20533  scmatsubcl  20534  smatvscl  20541  mdetunilem8  20636  chfacfscmul0  20876  chfacfscmulfsupp  20877  chfacfscmulgsum  20878  chfacfpmmul0  20880  chfacfpmmulfsupp  20881  chfacfpmmulgsum  20882  cpmidpmatlem3  20890  chcoeffeqlem  20903  cayleyhamilton0  20907  cayleyhamiltonALT  20909  cayleyhamilton1  20910  elcls  21091  clsndisj  21093  isclo2  21106  neiuni  21140  neissex  21145  neiptopreu  21151  tgrest  21177  neitr  21198  tgcnp  21271  lmfpm  21313  lmcl  21315  lmss  21316  lmff  21319  ist1-2  21365  cnt1  21368  cmpsublem  21416  clsconn  21447  locfindis  21547  kgeni  21554  kgenidm  21564  txcnpi  21625  ptpjopn  21629  ptclsg  21632  txcmplem1  21658  qtoptop2  21716  qtoptopon  21721  r0sep  21765  ptunhmeo  21825  t0kq  21835  fsubbas  21884  neifil  21897  uffixsn  21942  ufildr  21948  rnelfm  21970  isfcls2  22030  uffclsflim  22048  alexsublem  22061  cnextfun  22081  cnextfvval  22082  cnextf  22083  cnextcn  22084  tmdcn2  22106  symgtgp  22118  tsmssplit  22168  ustuni  22243  trust  22246  utoptop  22251  restutop  22254  restutopopn  22255  ustuqtop1  22258  ustuqtop2  22259  ustuqtop3  22260  ustuqtop4  22261  utop2nei  22267  utop3cls  22268  ucncn  22302  trcfilu  22311  cfiluweak  22312  psmetdmdm  22323  xmeter  22451  prdsbl  22509  neibl  22519  methaus  22538  prdsxmslem2  22547  metustto  22571  metustexhalf  22574  metust  22576  cfilucfil  22577  psmetutop  22585  tngngp2  22669  tngngp  22671  tgqioo  22816  xrsxmet  22825  icccmplem1  22838  icccmplem2  22839  cnmpt2pc  22940  iihalf2  22945  icoopnst  22951  iocopnst  22952  xrhmeo  22958  lebnumlem1  22973  lebnumlem3  22975  pi1blem  23051  pi1grplem  23061  pi1xfrf  23065  pi1xfr  23067  pi1xfrcnvlem  23068  pi1cof  23071  pi1coghm  23073  cmetcaulem  23298  causs  23308  metcld  23316  lmcau  23323  rrxcph  23392  minveclem4  23415  ivthlem2  23433  ivthlem3  23434  ivthicc  23439  ovolshftlem1  23490  ovolicc1  23497  ovolicopnf  23505  volfiniun  23528  uniioombllem3  23566  dyaddisjlem  23576  vitalilem2  23590  itg1ge0  23667  mbfi1fseqlem3  23698  xrge0f  23712  itg2seq  23723  itg2monolem1  23731  itg2addlem  23739  itg2gt0  23741  iblcnlem  23769  itgss3  23795  itgsplit  23816  dvnff  23900  dvferm2  23964  dvlip2  23972  dveq0  23977  dvge0  23983  dvcnvre  23996  dvfsumle  23998  dvfsumabs  24000  dvfsumlem2  24004  ftc1lem2  24013  ftc1lem4  24016  ftc1lem5  24017  ftc1cn  24020  ftc2  24021  itgsubstlem  24025  coe1mul3  24073  ply1divex  24110  dgrlem  24199  dgrlb  24206  coemulhi  24224  dgrlt  24236  dgrmul  24240  plydivlem4  24265  fta1  24277  aaliou2b  24310  taylplem2  24332  dvtaylp  24338  ulmcau  24363  tanabsge  24473  sinq12gt0  24474  argimgt0  24572  cxplea  24656  cxple2  24657  cxpsqrt  24663  cxpaddlelem  24706  loglesqrt  24713  logrec  24715  ang180lem2  24754  lawcos  24760  asinlem3a  24811  asinlem3  24812  asinsin  24833  atanlogaddlem  24854  atanlogadd  24855  atanlogsub  24857  atantan  24864  atanbnd  24867  atantayl2  24879  efrlim  24910  wilthlem2  25009  basellem2  25022  sqfpc  25077  ppieq0  25116  sqff1o  25122  fsumdvdscom  25125  ppiub  25143  chpeq0  25147  chtleppi  25149  fsumvma  25152  fsumvma2  25153  mersenne  25166  dchrabs2  25201  dchr1re  25202  dchrpt  25206  lgsdilem  25263  lgsdinn0  25284  gausslemma2dlem0b  25296  gausslemma2dlem1a  25304  gausslemma2dlem5  25310  gausslemma2dlem6  25311  lgsquad3  25326  m1lgs  25327  2lgslem1a  25330  2lgslem1  25333  2lgslem3a1  25339  2lgslem3b1  25340  2lgslem3c1  25341  2lgslem3d1  25342  2sqlem6  25362  rpvmasumlem  25390  dchrisumlem3  25394  dchrisum0flblem1  25411  pntibndlem2a  25493  pntlem3  25512  padicabv  25533  ercgrg  25626  tglnunirn  25657  tglineeltr  25740  mirln2  25786  mirbtwnhl  25789  isperp2  25824  outpasch  25861  lnopp2hpgb  25869  ttgbtwnid  25978  axcontlem2  26059  axcontlem12  26069  upgredg  26247  fusgrfisstep  26437  nbupgrres  26481  usgrnbcnvfv  26482  nbusgredgeu  26483  nbcplgr  26558  cusgrexi  26567  structtocusgr  26570  cusgrsizeinds  26576  vtxdgoddnumeven  26677  uhgr0edg0rgr  26697  wlkl1loop  26762  upgriswlk  26765  usgr2pthlem  26887  cyclnspth  26924  wwlknvtx  26966  wspthnp  26972  elwwlks2ons3  27095  elwwlks2ons3OLD  27096  elwspths2on  27101  usgr2wspthons3  27106  clwlkclwwlklem2a4  27140  clwlkclwwlk2  27146  clwlkclwwlkfolem  27150  clwlkclwwlkf1  27153  clwwisshclwws  27158  loopclwwlkn1b  27191  clwwlkf1  27198  wwlksext2clwwlk  27207  clwwnisshclwwsn  27210  eleclclwwlknlem2  27212  clwlksfclwwlk2wrdOLD  27232  clwlksf1clwwlklem3OLD  27241  clwlksf1clwwlklemOLD  27242  1pthon2v  27326  upgr3v3e3cycl  27353  upgreupthi  27381  eupth2lemb  27410  frgrncvvdeqlem7  27480  frgrncvvdeqlem8  27481  frgrncvvdeqlem9  27482  clwwnonrepclwwnon  27522  numclwwlkovh  27553  numclwwlk2lem1  27556  numclwwlk2lem1OLD  27563  frgrreggt1  27581  frgrregord013  27583  cnnv  27860  nmounbseqi  27960  nmounbseqiALT  27961  nmlnogt0  27980  nmblolbii  27982  blocnilem  27987  ajmoi  28042  minvecolem4  28064  hhnv  28350  norm1  28434  hhssnv  28449  pjhtheu  28581  pjpreeq  28585  spanunsni  28766  fh1  28805  fh2  28806  cm2j  28807  chscllem4  28827  pjid  28882  adjmo  29019  eleigveccl  29146  eigvalcl  29148  eigvec1  29149  eighmre  29150  eighmorth  29151  nmop0h  29178  nmbdoplbi  29211  nmcoplbi  29215  nmophmi  29218  lncnopbd  29224  nmbdfnlbi  29236  nmcfnlbi  29239  cnlnadjeui  29264  branmfn  29292  rnbra  29294  nmopleid  29326  strlem5  29442  hstrlem5  29450  dmdbr3  29492  dmdbr4  29493  mdsl3  29503  hatomistici  29549  cvexchlem  29555  chirredlem1  29577  chirredlem2  29578  chirredi  29581  atcvat3i  29583  atcvat4i  29584  atabsi  29588  mdsymlem1  29590  mdsymlem3  29592  mdsymlem5  29594  dmdbr5ati  29609  cdj1i  29620  foresf1o  29668  rabfodom  29669  elabreximd  29673  elpreq  29685  f1o3d  29758  acunirnmpt2f  29788  disjdsct  29807  1stpreimas  29810  fcobij  29827  fpwrelmapffslem  29834  nn0sqeq1  29840  xrofsup  29860  eliccelico  29866  elicoelioo  29867  numdenneg  29890  fsumiunle  29902  dpadd3  29945  threehalves  29948  xrge0addgt0  30016  xrge0adddir  30017  xrge0npcan  30019  omndmul3  30038  submarchi  30065  archirng  30067  archirngz  30068  archiexdiv  30069  archiabllem1a  30070  1smat1  30195  madjusmdetlem2  30219  locfinreflem  30232  metideq  30261  unitdivcld  30272  cnre2csqlem  30281  ordtconnlem1  30295  fmcncfil  30302  lmxrge0  30323  pl1cn  30326  zrhunitpreima  30347  elzdif0  30349  qqhval2lem  30350  qqhf  30355  indf1ofs  30413  esumfsup  30457  esumpcvgval  30465  esum2dlem  30479  esum2d  30480  esumiun  30481  sigasspw  30504  issgon  30511  ispisys2  30541  meascnbl  30607  voliune  30617  volfiniune  30618  omssubaddlem  30686  carsggect  30705  carsgclctunlem2  30706  oddpwdc  30741  eulerpartlems  30747  eulerpartlemgvv  30763  ballotlemfrcn0  30916  sgncl  30925  sgnneg  30927  sgn3da  30928  sgnmul  30929  sgnsub  30931  gsumnunsn  30940  signsplypnf  30952  signsply0  30953  signslema  30964  signstfvneq0  30974  signsvfpn  30987  signsvfnn  30988  repr0  31014  reprlt  31022  reprgt  31024  reprinfz1  31025  chtvalz  31032  breprexplemc  31035  hgt750lemb  31059  hgt750leme  31061  bnj563  31136  bnj1001  31351  subfacp1lem5  31489  subfacp1lem6  31490  erdszelem9  31504  ptpconn  31538  resconn  31551  cvmlift3lem7  31630  msrrcl  31763  trpredrec  32058  scutbdaylt  32243  btwnintr  32447  btwnouttr  32452  cgrxfr  32483  btwnconn1lem12  32526  colinbtwnle  32546  lineelsb2  32576  nn0prpwlem  32638  neibastop3  32678  onintopssconn  32756  bj-restsnss  33347  bj-restsnss2  33348  taupilem1  33484  relowlssretop  33527  finxpsuclem  33550  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  33777  itgaddnclem2  33781  ftc1cnnclem  33795  ftc1cnnc  33796  ftc1anclem2  33798  ftc1anclem5  33801  ftc1anclem7  33803  ftc1anc  33805  ftc2nc  33806  dvasin  33808  areacirclem5  33816  areacirc  33817  fdc  33852  incsequz  33855  blbnd  33897  prdstotbnd  33904  cnpwstotbnd  33907  ismtyres  33918  rngohomf  34076  rngohom1  34078  rngohomadd  34079  rngohommul  34080  idlss  34126  idl0cl  34128  idladdcl  34129  idllmulcl  34130  idlrmulcl  34131  maxidlnr  34152  maxidlmax  34153  smprngopr  34162  pridlc  34181  ac6s6f  34291  lshpnel2N  34765  islsati  34774  lkr0f  34874  lfl1dim  34901  lfl1dim2N  34902  omlfh1N  35038  leat  35073  atlatmstc  35099  cvlatexch3  35118  lnnat  35207  cvrat3  35222  cvrat4  35223  3dim3  35249  dalem4  35445  dalem39  35491  paddasslem12  35611  psubcliN  35718  pmapojoinN  35748  lhpm0atN  35809  lhprelat3N  35820  trlnid  35960  trlval3  35968  cdleme22b  36122  trljco  36521  diaglbN  36836  dibvalrel  36944  dicvalrelN  36966  diclspsn  36975  dih1dimatlem  37110  dihlatat  37118  lcfl6  37281  lcfl8  37283  lcfrvalsnN  37322  lcfrlem9  37331  mapdheq2  37510  hlhillcs  37739  hlhilhillem  37741  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  37983  2nn0ind  38011  congabseq  38042  acongrep  38048  acongeq  38051  jm2.22  38063  jm2.26lem3  38069  pw2f1ocnv  38105  limsuc2  38112  fnwe2lem3  38123  aomclem6  38130  kercvrlsm  38154  pwssplit4  38160  lpirlnr  38188  rfovcnvf1od  38798  dssmapnvod  38814  cvgdvgrat  39012  radcnvrat  39013  dvconstbi  39033  bccbc  39044  bi2imp  39186  ax6e2ndeqALT  39661  mulltgt0  39675  refsumcn  39683  cncmpmax  39685  mapdm0OLD  39872  unirnmapsn  39893  icoiccdif  40231  climinf  40318  climreeq  40325  climeldmeq  40377  coskpi2  40557  cosknegpi  40560  icccncfext  40580  dvmptfprodlem  40639  volioore  40686  stoweidlem27  40723  stoweidlem29  40725  stoweidlem31  40727  stoweidlem34  40730  stoweidlem48  40744  stoweidlem59  40755  fourierdlem109  40911  fourierswlem  40926  elaa2  40930  etransclem37  40967  hspmbllem2  41323  smflimmpt  41498  sigarcol  41535  reuan  41692  ndmaovg  41773  afv2orxorb  41817  subsubelfzo0  41911  iccelpart  41944  fargshiftf1  41952  fargshiftfo  41953  pfxeq  41979  pfxccatin12lem1  41998  repswpfx  42011  fmtnoprmfac1lem  42051  fmtno4prmfac  42059  2pwp1prmfmtno  42079  sfprmdvdsmersenne  42095  lighneallem3  42099  proththd  42106  evenm1odd  42127  evenp1odd  42128  nnoALTV  42181  stgoldbwt  42239  sbgoldbst  42241  nnsum4primeseven  42263  nnsum4primesevenALTV  42264  bgoldbtbndlem2  42269  upgrwlkupwlk  42289  rnghmf1o  42471  rnghmsubcsetclem1  42543  zrinitorngc  42568  zrtermorngc  42569  rhmsubcsetclem1  42589  rhmsubcrngclem1  42595  funcringcsetcALTV2lem8  42611  funcringcsetclem8ALTV  42634  zrtermoringc  42638  ply1sclrmsm  42739  lincfsuppcl  42770  zofldiv2  42893  elbigolo1  42919  blennn0em1  42953  blennn0e2  42956  dig2nn0ld  42966  nn0sumshdiglem2  42984
  Copyright terms: Public domain W3C validator