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

Theorem biimpa 500
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  652  simplbda  653  pm5.1  920  bimsc1  999  biimp3a  1472  equsex  2328  euor  2541  euan  2559  cgsexg  3269  cgsex2g  3270  cgsex4g  3271  ceqsex  3272  sbciegft  3499  sbeqalb  3521  syl5sseq  3686  elpwunsn  4256  ralxfr2d  4912  propeqop  4999  euotd  5004  relop  5305  elsnxp  5715  sspred  5726  fnbr  6031  f1o00  6209  foelrni  6283  dffv2  6310  iinpreima  6385  funressn  6466  fnex  6522  f1prex  6579  weniso  6644  riotaeqimp  6674  f1ocnv2d  6928  ofrval  6949  limsssuc  7092  resiexg  7144  eloprabi  7277  1stconst  7310  2ndconst  7311  frxp  7332  poxp  7334  smodm2  7497  smoiso  7504  tz7.44lem1  7546  oev2  7648  oesuclem  7650  oecl  7662  omordi  7691  omwordri  7697  omword2  7699  omordlim  7702  omlimcl  7703  omeulem2  7708  oeordi  7712  oewordri  7717  oelim2  7720  oeoa  7722  oeoe  7724  nnawordi  7746  nnaordex  7763  erth  7834  iiner  7862  pw2f1olem  8105  pw2f1o  8106  onomeneq  8191  onfin2  8193  unxpdomlem2  8206  isinf  8214  findcard2  8241  fipreima  8313  fipwss  8376  cantnfp1lem3  8615  carden2b  8831  carddomi2  8834  infxpenlem  8874  acni2  8907  numacn  8910  alephfp  8969  pwsdompw  9064  ackbij2lem3  9101  cfeq0  9116  cfsuc  9117  cfsmolem  9130  domfin4  9171  axdc3lem2  9311  axdc3lem4  9313  alephreg  9442  fpwwe2  9503  winainflem  9553  r1limwun  9596  inar1  9635  grudomon  9677  nlt1pi  9766  indpi  9767  nqereu  9789  ltbtwnnq  9838  prlem934  9893  prlem936  9907  addgt0sr  9963  leltne  10165  ne0gt0  10180  mullt0  10585  msqgt0  10586  mulne0  10707  divne0  10735  div2neg  10786  ltmul12a  10917  recgt1i  10958  negfi  11009  nn2ge  11083  div4p1lem1div2  11325  nn0lt2  11478  peano5uzi  11504  eluzp1m1  11749  eluzaddi  11752  eluzsubi  11753  uz2m1nn  11801  nn01to3  11819  rpnnen1lem5  11856  rpnnen1lem5OLD  11862  rphalflt  11898  xrleltne  12016  max0sub  12065  xmulpnf1n  12146  xmulge0  12152  xadddi  12163  supxr  12181  supxr2  12182  ixxdisj  12228  ixxun  12229  ixxub  12234  ixxlb  12235  iccgelb  12268  icodisj  12335  difreicc  12342  iccf1o  12354  fzsuc2  12436  fzonmapblen  12553  elfznelfzo  12613  flge0nn0  12661  flge1nn  12662  2submod  12771  modfzo0difsn  12782  seqf1olem2  12881  expubnd  12961  sqlecan  13011  bernneq  13030  bernneq2  13031  expnbnd  13033  discr1  13040  facwordi  13116  faclbnd4lem4  13123  bcpasc  13148  hashgt0n0  13194  elprchashprn2  13222  hash1to3  13311  iswrdi  13341  ffz0iswrd  13364  ccatsymb  13400  ccatass  13406  swrdlend  13477  swrdfv2  13492  swrdspsleq  13495  swrdswrdlem  13505  swrdswrd  13506  swrdswrd0  13508  swrdccatin12lem2b  13532  revccat  13561  revrev  13562  repswccat  13578  2cshw  13605  cshwcsh2id  13620  revco  13626  cshco  13628  s2f1o  13707  s4f1o  13709  wrdlen2i  13732  wwlktovf  13745  ofccat  13754  trclub  13783  sqr0lem  14025  sqrlem2  14028  sqrlem7  14033  max0add  14094  recval  14106  nnabscl  14109  absmax  14113  sqreulem  14143  climi0  14287  lo1bdd2  14299  rlimresb  14340  lo1eq  14343  rlimeq  14344  isercolllem3  14441  climsup  14444  fsumsplit  14515  fsumcom2  14549  fsumcom2OLD  14550  explecnv  14641  fprodser  14723  fprodsplit  14740  fprodcom2  14758  fprodcom2OLD  14759  eftlub  14883  sin02gt0  14966  rpnnen2lem10  14996  dvdsleabs2  15081  odd2np1  15112  oexpneg  15116  sqoddm1div8z  15125  bitsf1  15215  sadcaddlem  15226  bitsuz  15243  rplpwr  15323  rppwr  15324  nn0seqcvgd  15330  lcmneg  15363  qredeq  15418  dvdsnprmd  15450  oddprmge3  15459  isprm7  15467  qgt0numnn  15506  phibndlem  15522  hashgcdeq  15541  reumodprminv  15556  coprimeprodsq2  15561  pythagtrip  15586  dvdsprmpweqle  15637  fldivp1  15648  unbenlem  15659  4sqlem9  15697  4sqlem15  15710  4sqlem16  15711  vdwlem6  15737  vdwlem10  15741  vdwlem11  15742  vdwlem13  15744  vdw  15745  prmgaplem7  15808  prmgaplem8  15809  cshwshashlem1  15849  mreuni  16307  cidpropd  16417  subsubc  16560  ffthiso  16636  fuciso  16682  setcmon  16784  setcepi  16785  catciso  16804  funcestrcsetclem7  16833  funcestrcsetclem8  16834  setc1strwun  16840  funcsetcestrclem7  16848  hofcl  16946  hofpropd  16954  yonedalem4c  16964  yonedainv  16968  issstrmgm  17299  imasmnd  17375  pwsco1mhm  17417  imasgrp  17578  subginv  17648  subgmulg  17655  eqger  17691  subgga  17779  orbstafun  17790  orbsta  17792  symggrp  17866  psgnsn  17986  dfod2  18027  gexval  18039  gex1  18052  sylow2blem1  18081  sylow3lem1  18088  pj1eu  18155  efgredlema  18199  frgp0  18219  frgpmhm  18224  odadd1  18297  0cyg  18340  gsumzres  18356  gsumzsplit  18373  gsummptfzcl  18414  dprd2dlem1  18486  dprd2da  18487  dmdprdsplit2  18491  dprdsplit  18493  pgpfaclem3  18528  ablfac2  18534  imasring  18665  rhmf1o  18780  kerf1hrm  18791  subrg1  18838  abvneg  18882  lmhmf1o  19094  lmhmima  19095  reslmhm2b  19102  pwssplit0  19106  pwssplit1  19107  lsmspsn  19132  lspdisj  19173  lidlmcl  19265  isnzr2hash  19312  fidomndrnglem  19354  mplsubglem  19482  mplmonmul  19512  mplbas2  19518  subrgascl  19546  subrgasclcl  19547  evlsval2  19568  mpfind  19584  lply1binomsc  19725  absabv  19851  f1lindf  20209  mat0dimscm  20323  scmataddcl  20370  scmatsubcl  20371  smatvscl  20378  mdetunilem8  20473  chfacfscmul0  20711  chfacfscmulfsupp  20712  chfacfscmulgsum  20713  chfacfpmmul0  20715  chfacfpmmulfsupp  20716  chfacfpmmulgsum  20717  cpmidpmatlem3  20725  chcoeffeqlem  20738  cayleyhamilton0  20742  cayleyhamiltonALT  20744  cayleyhamilton1  20745  elcls  20925  clsndisj  20927  isclo2  20940  neiuni  20974  neissex  20979  neiptopreu  20985  tgrest  21011  neitr  21032  tgcnp  21105  lmfpm  21147  lmcl  21149  lmss  21150  lmff  21153  ist1-2  21199  cnt1  21202  cmpsublem  21250  clsconn  21281  locfindis  21381  kgeni  21388  kgenidm  21398  txcnpi  21459  ptpjopn  21463  ptclsg  21466  txcmplem1  21492  qtoptop2  21550  qtoptopon  21555  r0sep  21599  ptunhmeo  21659  t0kq  21669  fsubbas  21718  neifil  21731  uffixsn  21776  ufildr  21782  rnelfm  21804  isfcls2  21864  uffclsflim  21882  alexsublem  21895  cnextfun  21915  cnextfvval  21916  cnextf  21917  cnextcn  21918  tmdcn2  21940  symgtgp  21952  tsmssplit  22002  ustuni  22077  trust  22080  utoptop  22085  restutop  22088  restutopopn  22089  ustuqtop1  22092  ustuqtop2  22093  ustuqtop3  22094  ustuqtop4  22095  utop2nei  22101  utop3cls  22102  ucncn  22136  trcfilu  22145  cfiluweak  22146  psmetdmdm  22157  xmeter  22285  prdsbl  22343  neibl  22353  methaus  22372  prdsxmslem2  22381  metustto  22405  metustexhalf  22408  metust  22410  cfilucfil  22411  psmetutop  22419  tngngp2  22503  tngngp  22505  tgqioo  22650  xrsxmet  22659  icccmplem1  22672  icccmplem2  22673  cnmpt2pc  22774  iihalf2  22779  icoopnst  22785  iocopnst  22786  xrhmeo  22792  lebnumlem1  22807  lebnumlem3  22809  pi1blem  22885  pi1grplem  22895  pi1xfrf  22899  pi1xfr  22901  pi1xfrcnvlem  22902  pi1cof  22905  pi1coghm  22907  cmetcaulem  23132  causs  23142  metcld  23150  lmcau  23157  rrxcph  23226  minveclem4  23249  ivthlem2  23267  ivthlem3  23268  ivthicc  23273  ovolshftlem1  23323  ovolicc1  23330  ovolicopnf  23338  volfiniun  23361  uniioombllem3  23399  dyaddisjlem  23409  vitalilem2  23423  itg1ge0  23498  mbfi1fseqlem3  23529  xrge0f  23543  itg2seq  23554  itg2monolem1  23562  itg2addlem  23570  itg2gt0  23572  iblcnlem  23600  itgss3  23626  itgsplit  23647  dvnff  23731  dvferm2  23795  dvlip2  23803  dveq0  23808  dvge0  23814  dvcnvre  23827  dvfsumle  23829  dvfsumabs  23831  dvfsumlem2  23835  ftc1lem2  23844  ftc1lem4  23847  ftc1lem5  23848  ftc1cn  23851  ftc2  23852  itgsubstlem  23856  coe1mul3  23904  ply1divex  23941  dgrlem  24030  dgrlb  24037  coemulhi  24055  dgrlt  24067  dgrmul  24071  plydivlem4  24096  fta1  24108  aaliou2b  24141  taylplem2  24163  dvtaylp  24169  ulmcau  24194  tanabsge  24303  sinq12gt0  24304  argimgt0  24403  cxplea  24487  cxple2  24488  cxpsqrt  24494  cxpaddlelem  24537  loglesqrt  24544  logrec  24546  ang180lem2  24585  lawcos  24591  asinlem3a  24642  asinlem3  24643  asinsin  24664  atanlogaddlem  24685  atanlogadd  24686  atanlogsub  24688  atantan  24695  atanbnd  24698  atantayl2  24710  efrlim  24741  wilthlem2  24840  basellem2  24853  sqfpc  24908  ppieq0  24947  sqff1o  24953  fsumdvdscom  24956  ppiub  24974  chpeq0  24978  chtleppi  24980  fsumvma  24983  fsumvma2  24984  mersenne  24997  dchrabs2  25032  dchr1re  25033  dchrpt  25037  lgsdilem  25094  lgsdinn0  25115  gausslemma2dlem0b  25127  gausslemma2dlem1a  25135  gausslemma2dlem5  25141  gausslemma2dlem6  25142  lgsquad3  25157  m1lgs  25158  2lgslem1a  25161  2lgslem1  25164  2lgslem3a1  25170  2lgslem3b1  25171  2lgslem3c1  25172  2lgslem3d1  25173  2sqlem6  25193  rpvmasumlem  25221  dchrisumlem3  25225  dchrisum0flblem1  25242  pntibndlem2a  25324  pntlem3  25343  padicabv  25364  ercgrg  25457  tglnunirn  25488  tglineeltr  25571  mirln2  25617  mirbtwnhl  25620  isperp2  25655  outpasch  25692  lnopp2hpgb  25700  ttgbtwnid  25809  axcontlem2  25890  axcontlem12  25900  upgredg  26077  fusgrfisstep  26266  nbupgrres  26310  usgrnbcnvfv  26311  nbusgredgeu  26312  nbcplgr  26386  cusgrexi  26395  structtocusgr  26398  cusgrsizeinds  26404  vtxdgoddnumeven  26505  uhgr0edg0rgr  26525  wlkl1loop  26590  upgriswlk  26593  usgr2pthlem  26715  cyclnspth  26751  wwlknvtx  26793  wspthnp  26799  elwwlks2ons3  26920  elwwlks2ons3OLD  26921  elwspths2on  26926  usgr2wspthons3  26931  clwlkclwwlklem2a4  26963  clwlkclwwlk2  26969  clwwisshclwws  26972  loopclwwlkn1b  27005  clwwlkf1  27012  wwlksext2clwwlk  27021  clwwnisshclwwsn  27024  eleclclwwlknlem2  27026  clwlksfclwwlk2wrd  27045  clwlksf1clwwlklem3  27054  clwlksf1clwwlklem  27055  1pthon2v  27131  upgr3v3e3cycl  27158  upgreupthi  27186  eupth2lemb  27215  frgrncvvdeqlem7  27285  frgrncvvdeqlem8  27286  frgrncvvdeqlem9  27287  numclwwlkovh  27353  numclwwlk2lem1  27356  numclwwlk2lem1OLD  27363  frgrreggt1  27380  frgrregord013  27382  cnnv  27660  nmounbseqi  27760  nmounbseqiALT  27761  nmlnogt0  27780  nmblolbii  27782  blocnilem  27787  ajmoi  27842  minvecolem4  27864  hhnv  28150  norm1  28234  hhssnv  28249  pjhtheu  28381  pjpreeq  28385  spanunsni  28566  fh1  28605  fh2  28606  cm2j  28607  chscllem4  28627  pjid  28682  adjmo  28819  eleigveccl  28946  eigvalcl  28948  eigvec1  28949  eighmre  28950  eighmorth  28951  nmop0h  28978  nmbdoplbi  29011  nmcoplbi  29015  nmophmi  29018  lncnopbd  29024  nmbdfnlbi  29036  nmcfnlbi  29039  cnlnadjeui  29064  branmfn  29092  rnbra  29094  nmopleid  29126  strlem5  29242  hstrlem5  29250  dmdbr3  29292  dmdbr4  29293  mdsl3  29303  hatomistici  29349  cvexchlem  29355  chirredlem1  29377  chirredlem2  29378  chirredi  29381  atcvat3i  29383  atcvat4i  29384  atabsi  29388  mdsymlem1  29390  mdsymlem3  29392  mdsymlem5  29394  dmdbr5ati  29409  cdj1i  29420  foresf1o  29469  rabfodom  29470  elabreximd  29474  elpreq  29486  f1o3d  29559  acunirnmpt2f  29589  disjdsct  29608  1stpreimas  29611  fcobij  29628  fpwrelmapffslem  29635  nn0sqeq1  29641  xrofsup  29661  eliccelico  29667  elicoelioo  29668  numdenneg  29691  fsumiunle  29703  dpadd3  29748  threehalves  29751  xrge0addgt0  29819  xrge0adddir  29820  xrge0npcan  29822  omndmul3  29841  submarchi  29868  archirng  29870  archirngz  29871  archiexdiv  29872  archiabllem1a  29873  1smat1  29998  madjusmdetlem2  30022  locfinreflem  30035  metideq  30064  unitdivcld  30075  cnre2csqlem  30084  ordtconnlem1  30098  fmcncfil  30105  lmxrge0  30126  pl1cn  30129  zrhunitpreima  30150  elzdif0  30152  qqhval2lem  30153  qqhf  30158  indf1ofs  30216  esumfsup  30260  esumpcvgval  30268  esum2dlem  30282  esum2d  30283  esumiun  30284  sigasspw  30307  issgon  30314  ispisys2  30344  meascnbl  30410  voliune  30420  volfiniune  30421  omssubaddlem  30489  carsggect  30508  carsgclctunlem2  30509  oddpwdc  30544  eulerpartlems  30550  eulerpartlemgvv  30566  ballotlemfrcn0  30719  sgncl  30728  sgnneg  30730  sgn3da  30731  sgnmul  30732  sgnsub  30734  gsumnunsn  30743  signsplypnf  30755  signsply0  30756  signslema  30767  signstfvneq0  30777  signsvfpn  30790  signsvfnn  30791  repr0  30817  reprlt  30825  reprgt  30827  reprinfz1  30828  chtvalz  30835  breprexplemc  30838  hgt750lemb  30862  hgt750leme  30864  bnj563  30939  bnj1001  31154  subfacp1lem5  31292  subfacp1lem6  31293  erdszelem9  31307  ptpconn  31341  resconn  31354  cvmlift3lem7  31433  msrrcl  31566  trpredrec  31862  scutbdaylt  32047  btwnintr  32251  btwnouttr  32256  cgrxfr  32287  btwnconn1lem12  32330  colinbtwnle  32350  lineelsb2  32380  nn0prpwlem  32442  neibastop3  32482  onintopssconn  32564  bj-restsnss  33161  bj-restsnss2  33162  taupilem1  33297  relowlssretop  33341  finxpsuclem  33364  unccur  33522  lindsenlbs  33534  matunitlindflem1  33535  matunitlindflem2  33536  poimirlem2  33541  poimirlem8  33547  poimirlem14  33553  poimirlem15  33554  poimirlem17  33556  poimirlem20  33559  poimirlem22  33561  poimirlem24  33563  poimirlem25  33564  poimirlem27  33566  poimirlem28  33567  poimirlem31  33570  heicant  33574  mblfinlem2  33577  itg2gt0cn  33595  itgaddnclem2  33599  ftc1cnnclem  33613  ftc1cnnc  33614  ftc1anclem2  33616  ftc1anclem5  33619  ftc1anclem7  33621  ftc1anc  33623  ftc2nc  33624  dvasin  33626  areacirclem5  33634  areacirc  33635  fdc  33671  incsequz  33674  blbnd  33716  prdstotbnd  33723  cnpwstotbnd  33726  ismtyres  33737  rngohomf  33895  rngohom1  33897  rngohomadd  33898  rngohommul  33899  idlss  33945  idl0cl  33947  idladdcl  33948  idllmulcl  33949  idlrmulcl  33950  maxidlnr  33971  maxidlmax  33972  smprngopr  33981  pridlc  34000  ac6s6f  34111  lshpnel2N  34590  islsati  34599  lkr0f  34699  lfl1dim  34726  lfl1dim2N  34727  omlfh1N  34863  leat  34898  atlatmstc  34924  cvlatexch3  34943  lnnat  35031  cvrat3  35046  cvrat4  35047  3dim3  35073  dalem4  35269  dalem39  35315  paddasslem12  35435  psubcliN  35542  pmapojoinN  35572  lhpm0atN  35633  lhprelat3N  35644  trlnid  35784  trlval3  35792  cdleme22b  35946  trljco  36345  diaglbN  36661  dibvalrel  36769  dicvalrelN  36791  diclspsn  36800  dih1dimatlem  36935  dihlatat  36943  lcfl6  37106  lcfl8  37108  lcfrvalsnN  37147  lcfrlem9  37156  mapdheq2  37335  hlhillcs  37567  hlhilhillem  37569  mzpindd  37626  lzunuz  37648  2rexfrabdioph  37677  irrapxlem3  37705  pellexlem2  37711  pellexlem5  37714  pell1234qrreccl  37735  pell14qrdich  37750  pell1qrge1  37751  elpell1qr2  37753  reglogltb  37772  reglogleb  37773  rmxycomplete  37799  2nn0ind  37827  congabseq  37858  acongrep  37864  acongeq  37867  jm2.22  37879  jm2.26lem3  37885  pw2f1ocnv  37921  limsuc2  37928  fnwe2lem3  37939  aomclem6  37946  kercvrlsm  37970  pwssplit4  37976  lpirlnr  38004  rfovcnvf1od  38615  dssmapnvod  38631  cvgdvgrat  38829  radcnvrat  38830  dvconstbi  38850  bccbc  38861  bi2imp  39005  ax6e2ndeqALT  39481  mulltgt0  39495  refsumcn  39503  cncmpmax  39505  mapdm0OLD  39697  unirnmapsn  39720  icoiccdif  40068  climinf  40156  climreeq  40163  climeldmeq  40215  coskpi2  40395  cosknegpi  40398  icccncfext  40418  dvmptfprodlem  40477  volioore  40525  stoweidlem27  40562  stoweidlem29  40564  stoweidlem31  40566  stoweidlem34  40569  stoweidlem48  40583  stoweidlem59  40594  fourierdlem109  40750  fourierswlem  40765  elaa2  40769  etransclem37  40806  hspmbllem2  41162  smflimmpt  41337  sigarcol  41374  reuan  41501  ndmaovg  41585  subsubelfzo0  41661  iccelpart  41694  fargshiftf1  41702  fargshiftfo  41703  pfxeq  41729  pfxccatin12lem1  41748  repswpfx  41761  fmtnoprmfac1lem  41801  fmtno4prmfac  41809  2pwp1prmfmtno  41829  sfprmdvdsmersenne  41845  lighneallem3  41849  proththd  41856  evenm1odd  41877  evenp1odd  41878  nnoALTV  41931  stgoldbwt  41989  sbgoldbst  41991  nnsum4primeseven  42013  nnsum4primesevenALTV  42014  bgoldbtbndlem2  42019  upgrwlkupwlk  42046  rnghmf1o  42228  rnghmsubcsetclem1  42300  zrinitorngc  42325  zrtermorngc  42326  rhmsubcsetclem1  42346  rhmsubcrngclem1  42352  funcringcsetcALTV2lem8  42368  funcringcsetclem8ALTV  42391  zrtermoringc  42395  ply1sclrmsm  42496  lincfsuppcl  42527  zofldiv2  42650  elbigolo1  42676  blennn0em1  42710  blennn0e2  42713  dig2nn0ld  42723  nn0sumshdiglem2  42741
  Copyright terms: Public domain W3C validator