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

Theorem biimpa 470
Description: Inference from a logical equivalence. (Contributed by NM, 3-May-1994.)
Hypothesis
Ref Expression
biimpa.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
biimpa  |-  ( (
ph  /\  ps )  ->  ch )

Proof of Theorem biimpa
StepHypRef Expression
1 biimpa.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21biimpd 198 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
32imp 418 1  |-  ( (
ph  /\  ps )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  simprbda  606  simplbda  607  pm5.1  830  bimsc1  904  biimp3a  1281  euor  2170  euan  2200  cgsexg  2819  cgsex2g  2820  cgsex4g  2821  ceqsex  2822  sbciegft  3021  sbeqalb  3043  syl5sseq  3226  euotd  4267  ralxfr2d  4550  elpwunsn  4568  limsssuc  4641  relop  4834  resiexg  4997  fnbr  5346  f1o00  5508  dffv2  5592  iinpreima  5655  funressn  5706  fnex  5741  weniso  5852  f1ocnv2d  6068  ofrval  6088  eloprabi  6186  1stconst  6207  2ndconst  6208  frxp  6225  poxp  6227  riotasvdOLD  6348  smodm2  6372  smoiso  6379  tz7.44lem1  6418  oev2  6522  oesuclem  6524  oecl  6536  omordi  6564  omwordri  6570  omword2  6572  omordlim  6575  omlimcl  6576  omeulem2  6581  oeordi  6585  oewordri  6590  oelim2  6593  oeoa  6595  oeoe  6597  nnawordi  6619  nnaordex  6636  erth  6704  iiner  6731  pw2f1olem  6966  pw2f1o  6967  onomeneq  7050  onfin2  7052  unxpdomlem2  7068  isinf  7076  findcard2  7098  fipreima  7161  fipwss  7182  cantnfp1lem3  7382  carden2b  7600  carddomi2  7603  infxpenlem  7641  acni2  7673  numacn  7676  alephfp  7735  pwsdompw  7830  ackbij2lem3  7867  cfeq0  7882  cfsuc  7883  cfsmolem  7896  domfin4  7937  axdc3lem2  8077  axdc3lem4  8079  alephreg  8204  fpwwe2  8265  winainflem  8315  r1limwun  8358  inar1  8397  grudomon  8439  nlt1pi  8530  indpi  8531  nqereu  8553  ltbtwnnq  8602  prlem934  8657  prlem936  8671  addgt0sr  8726  leltne  8911  ne0gt0  8925  mullt0  9293  msqgt0  9294  mulne0  9410  divne0  9436  div2neg  9483  ltmul12a  9612  recgt1i  9653  nn2ge  9771  peano5uzi  10100  eluzp1m1  10251  eluzaddi  10254  eluzsubi  10255  uz2m1nn  10292  rpnnen1lem5  10346  rphalflt  10380  xrleltne  10479  max0sub  10523  xmulpnf1n  10598  xmulge0  10604  xadddi  10615  supxr  10631  supxr2  10632  ixxdisj  10671  ixxun  10672  ixxub  10677  ixxlb  10678  icodisj  10761  difreicc  10767  iccf1o  10778  fzsuc2  10842  flge0nn0  10948  flge1nn  10949  seqf1olem2  11086  expubnd  11162  sqlecan  11209  bernneq  11227  bernneq2  11228  expnbnd  11230  discr1  11237  facwordi  11302  faclbnd4lem4  11309  bcpasc  11333  iswrdi  11417  ccatass  11436  revccat  11484  revrev  11485  revco  11489  sqr0lem  11726  sqrlem2  11729  sqrlem7  11734  max0add  11795  recval  11806  nnabscl  11809  absmax  11813  sqreulem  11843  climi0  11986  lo1bdd2  11998  rlimresb  12039  lo1eq  12042  rlimeq  12043  isercolllem3  12140  climsup  12143  fsumsplit  12212  fsumcom2  12237  explecnv  12323  eftlub  12389  sin02gt0  12472  rpnnen2lem10  12502  odd2np1  12587  oexpneg  12590  bitsf1  12637  sadcaddlem  12648  bitsuz  12665  rplpwr  12735  rppwr  12736  nn0seqcvgd  12740  qredeq  12785  qgt0numnn  12822  phibndlem  12838  coprimeprodsq2  12863  pythagtrip  12887  fldivp1  12945  unbenlem  12955  4sqlem9  12993  4sqlem15  13006  4sqlem16  13007  vdwlem6  13033  vdwlem10  13037  vdwlem11  13038  vdwlem13  13040  vdw  13041  mreuni  13502  cidpropd  13613  subsubc  13727  ffthiso  13803  fuciso  13849  setcmon  13919  setcepi  13920  catciso  13939  hofcl  14033  hofpropd  14041  yonedalem4c  14051  yonedainv  14055  ipoval  14257  imasmnd  14410  pwsco1mhm  14446  imasgrp  14611  subginv  14628  subgmulg  14635  eqger  14667  subgga  14754  orbstafun  14765  orbsta  14767  symggrp  14780  dfod2  14877  gexval  14889  gex1  14902  sylow2blem1  14931  sylow3lem1  14938  pj1eu  15005  efgredlema  15049  frgp0  15069  frgpmhm  15074  odadd1  15140  0cyg  15179  gsumzres  15194  gsumzsplit  15206  dprd2dlem1  15276  dprd2da  15277  dmdprdsplit2  15281  dprdsplit  15283  pgpfaclem3  15318  ablfac2  15324  imasrng  15402  subrg1  15555  abvneg  15599  lmhmf1o  15803  lmhmima  15804  reslmhm2b  15811  lsmspsn  15837  lspdisj  15878  lidlmcl  15969  fidomndrnglem  16047  mplsubglem  16179  mplmonmul  16208  mplbas2  16212  subrgascl  16239  subrgasclcl  16240  absabv  16429  elcls  16810  clsndisj  16812  isclo2  16825  neiuni  16859  neissex  16864  tgrest  16890  tgcnp  16983  lmfpm  17023  lmcl  17025  lmss  17026  lmff  17029  ist1-2  17075  cnt1  17078  cmpsublem  17126  clscon  17156  kgeni  17232  kgenidm  17242  txcnpi  17302  ptpjopn  17306  ptclsg  17309  txcmplem1  17335  qtoptop2  17390  qtoptopon  17395  r0sep  17439  ptunhmeo  17499  t0kq  17509  fsubbas  17562  neifil  17575  uffixsn  17620  ufildr  17626  rnelfm  17648  isfcls2  17708  uffclsflim  17726  alexsublem  17738  tmdcn2  17772  symgtgp  17784  tsmssplit  17834  xmeter  17979  prdsbl  18037  neibl  18047  methaus  18066  prdsxmslem2  18075  tngngp2  18168  tngngp  18170  tgqioo  18306  xrsxmet  18315  icccmplem1  18327  icccmplem2  18328  cnmpt2pc  18426  iihalf2  18431  icoopnst  18437  iocopnst  18438  xrhmeo  18444  lebnumlem1  18459  lebnumlem3  18461  pi1blem  18537  pi1grplem  18547  pi1xfrf  18551  pi1xfr  18553  pi1xfrcnvlem  18554  pi1cof  18557  pi1coghm  18559  cmetcaulem  18714  causs  18724  metcld  18731  lmcau  18738  minveclem4  18796  ivthlem2  18812  ivthlem3  18813  ivthicc  18818  ovolshftlem1  18868  ovolicc1  18875  ovolicopnf  18883  volfiniun  18904  uniioombllem3  18940  dyaddisjlem  18950  vitalilem2  18964  itg1ge0  19041  mbfi1fseqlem3  19072  xrge0f  19086  itg2seq  19097  itg2monolem1  19105  itg2addlem  19113  itg2gt0  19115  iblcnlem  19143  itgss3  19169  itgsplit  19190  dvnff  19272  dvferm2  19334  dvlip2  19342  dveq0  19347  dvge0  19353  dvcnvre  19366  dvfsumle  19368  dvfsumabs  19370  dvfsumlem2  19374  ftc1lem2  19383  ftc1lem4  19386  ftc1lem5  19387  ftc1cn  19390  ftc2  19391  itgsubstlem  19395  evlsval2  19404  mpfind  19428  coe1mul3  19485  ply1divex  19522  dgrlem  19611  dgrlb  19618  coemulhi  19635  dgrlt  19647  dgrmul  19651  plydivlem4  19676  fta1  19688  aaliou2b  19721  taylplem2  19743  dvtaylp  19749  ulmcau  19772  tanabsge  19874  sinq12gt0  19875  argimgt0  19966  cxplea  20043  cxple2  20044  cxpsqr  20050  cxpaddlelem  20091  loglesqr  20098  ang180lem2  20108  lawcos  20114  logrec  20117  asinlem3a  20166  asinlem3  20167  asinsin  20188  atanlogaddlem  20209  atanlogadd  20210  atanlogsub  20212  atantan  20219  atanbnd  20222  atantayl2  20234  efrlim  20264  wilthlem2  20307  basellem2  20319  sqfpc  20375  ppieq0  20414  sqff1o  20420  fsumdvdscom  20425  ppiub  20443  chpeq0  20447  chtleppi  20449  fsumvma  20452  fsumvma2  20453  mersenne  20466  dchrabs2  20501  dchr1re  20502  dchrpt  20506  lgsdilem  20561  lgsdinn0  20579  lgsquad3  20600  m1lgs  20601  2sqlem6  20608  rpvmasumlem  20636  dchrisumlem3  20640  dchrisum0flblem1  20657  pntibndlem2a  20739  pntlem3  20758  padicabv  20779  vcoprnelem  21134  cnnv  21245  nmounbseqi  21355  nmounbseqiOLD  21356  nmlnogt0  21375  nmblolbii  21377  blocnilem  21382  ajmoi  21437  minvecolem4  21459  hhnv  21744  norm1  21828  hhssnv  21841  pjhtheu  21973  pjpreeq  21977  spanunsni  22158  fh1  22197  fh2  22198  cm2j  22199  chscllem4  22219  pjid  22274  adjmo  22412  eleigveccl  22539  eigvalcl  22541  eigvec1  22542  eighmre  22543  eighmorth  22544  nmop0h  22571  nmbdoplbi  22604  nmcoplbi  22608  nmophmi  22611  lncnopbd  22617  nmbdfnlbi  22629  nmcfnlbi  22632  cnlnadjeui  22657  branmfn  22685  rnbra  22687  nmopleid  22719  strlem5  22835  hstrlem5  22843  dmdbr3  22885  dmdbr4  22886  mdsl3  22896  hatomistici  22942  cvexchlem  22948  chirredlem1  22970  chirredlem2  22971  chirredi  22974  atcvat3i  22976  atcvat4i  22977  atabsi  22981  mdsymlem1  22983  mdsymlem3  22985  mdsymlem5  22987  dmdbr5ati  23002  cdj1i  23013  f1o3d  23037  elpreq  23188  xrofsup  23255  iccgelb  23266  eliccelico  23270  elicoelioo  23271  unitdivcld  23285  xrge0addgt0  23331  xrge0adddir  23332  xrge0npcan  23333  baselsiga  23476  sigasspw  23477  issgon  23484  meascnbl  23546  indf1ofs  23609  probun  23622  subfacp1lem5  23715  subfacp1lem6  23716  erdszelem9  23730  ptpcon  23764  rescon  23777  cvmlift3lem7  23856  eupap1  23900  sspred  24174  trpredrec  24241  axcontlem2  24593  axcontlem12  24603  btwnintr  24642  btwnouttr  24647  cgrxfr  24678  btwnconn1lem12  24721  colinbtwnle  24741  lineelsb2  24771  onintopsscon  24879  areacirclem6  24930  areacirc  24931  mapmapmap  25148  repcpwti  25161  cbicp  25166  valcurfn1  25204  prsubrtr  25399  basexre  25522  limptlimpr2lem2  25575  mslb1  25607  supnuf  25629  ehm  25791  dehm  25792  cehm  25793  idsubfun  25858  domcatfun  25925  codcatfun  25934  pdiveql  26168  nn0prpwlem  26238  locfindis  26305  neibastop3  26311  fdc  26455  incsequz  26458  blbnd  26511  prdstotbnd  26518  cnpwstotbnd  26521  ismtyres  26532  rngohomf  26597  rngohom1  26599  rngohomadd  26600  rngohommul  26601  idlss  26641  idl0cl  26643  idladdcl  26644  idllmulcl  26645  idlrmulcl  26646  maxidlnr  26667  maxidlmax  26668  smprngopr  26677  pridlc  26696  ceqsex3OLD  26726  mzpindd  26824  lzunuz  26847  2rexfrabdioph  26877  irrapxlem3  26909  pellexlem2  26915  pellexlem5  26918  pell1234qrreccl  26939  pell14qrdich  26954  pell1qrge1  26955  elpell1qr2  26957  reglogltb  26976  reglogleb  26977  rmxycomplete  27002  2nn0ind  27030  congabseq  27061  acongrep  27067  acongeq  27070  dvdsleabs2  27077  jm2.22  27088  jm2.26lem3  27094  pw2f1ocnv  27130  limsuc2  27137  fnwe2lem3  27149  aomclem6  27156  kercvrlsm  27181  pwssplit0  27187  pwssplit1  27188  pwssplit4  27191  frlmbas  27223  elfilspd  27255  f1lindf  27292  lpirlnr  27321  hashgcdeq  27517  dvconstbi  27551  mulltgt0  27693  refsumcn  27701  cncmpmax  27703  climinf  27732  climreeq  27739  stoweidlem27  27776  stoweidlem29  27778  stoweidlem31  27780  stoweidlem34  27783  stoweidlem48  27797  stoweidlem59  27808  sigarcol  27854  reuan  27958  ndmaovg  28044  elprchashprn2  28088  s2f1o  28091  s4f1o  28093  usgra1  28119  nbgraop  28140  nbcusgra  28159  biimpa21  28335  a9e2ndeqALT  28708  bnj563  28772  bnj1001  28990  lshpnel2N  29175  islsati  29184  lkr0f  29284  lfl1dim  29311  lfl1dim2N  29312  omlfh1N  29448  leat  29483  atlatmstc  29509  cvlatexch3  29528  lnnat  29616  cvrat3  29631  cvrat4  29632  3dim3  29658  dalem4  29854  dalem39  29900  paddasslem12  30020  psubcliN  30127  pmapojoinN  30157  lhpm0atN  30218  lhprelat3N  30229  trlnid  30368  trlval3  30376  cdleme22b  30530  trljco  30929  diaglbN  31245  dibvalrel  31353  dicvalrelN  31375  diclspsn  31384  dih1dimatlem  31519  dihlatat  31527  lcfl6  31690  lcfl8  31692  lcfrvalsnN  31731  lcfrlem9  31740  mapdheq2  31919  hlhillcs  32151  hlhilhillem  32153
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator