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  2172  euan  2202  cgsexg  2821  cgsex2g  2822  cgsex4g  2823  ceqsex  2824  sbciegft  3023  sbeqalb  3045  syl5sseq  3228  euotd  4269  ralxfr2d  4552  elpwunsn  4570  limsssuc  4643  relop  4836  resiexg  4999  fnbr  5348  f1o00  5510  dffv2  5594  iinpreima  5657  funressn  5708  fnex  5743  weniso  5854  f1ocnv2d  6070  ofrval  6090  eloprabi  6188  1stconst  6209  2ndconst  6210  frxp  6227  poxp  6229  riotasvdOLD  6350  smodm2  6374  smoiso  6381  tz7.44lem1  6420  oev2  6524  oesuclem  6526  oecl  6538  omordi  6566  omwordri  6572  omword2  6574  omordlim  6577  omlimcl  6578  omeulem2  6583  oeordi  6587  oewordri  6592  oelim2  6595  oeoa  6597  oeoe  6599  nnawordi  6621  nnaordex  6638  erth  6706  iiner  6733  pw2f1olem  6968  pw2f1o  6969  onomeneq  7052  onfin2  7054  unxpdomlem2  7070  isinf  7078  findcard2  7100  fipreima  7163  fipwss  7184  cantnfp1lem3  7384  carden2b  7602  carddomi2  7605  infxpenlem  7643  acni2  7675  numacn  7678  alephfp  7737  pwsdompw  7832  ackbij2lem3  7869  cfeq0  7884  cfsuc  7885  cfsmolem  7898  domfin4  7939  axdc3lem2  8079  axdc3lem4  8081  alephreg  8206  fpwwe2  8267  winainflem  8317  r1limwun  8360  inar1  8399  grudomon  8441  nlt1pi  8532  indpi  8533  nqereu  8555  ltbtwnnq  8604  prlem934  8659  prlem936  8673  addgt0sr  8728  leltne  8913  ne0gt0  8927  mullt0  9295  msqgt0  9296  mulne0  9412  divne0  9438  div2neg  9485  ltmul12a  9614  recgt1i  9655  nn2ge  9773  peano5uzi  10102  eluzp1m1  10253  eluzaddi  10256  eluzsubi  10257  uz2m1nn  10294  rpnnen1lem5  10348  rphalflt  10382  xrleltne  10481  max0sub  10525  xmulpnf1n  10600  xmulge0  10606  xadddi  10617  supxr  10633  supxr2  10634  ixxdisj  10673  ixxun  10674  ixxub  10679  ixxlb  10680  icodisj  10763  difreicc  10769  iccf1o  10780  fzsuc2  10844  flge0nn0  10950  flge1nn  10951  seqf1olem2  11088  expubnd  11164  sqlecan  11211  bernneq  11229  bernneq2  11230  expnbnd  11232  discr1  11239  facwordi  11304  faclbnd4lem4  11311  bcpasc  11335  iswrdi  11419  ccatass  11438  revccat  11486  revrev  11487  revco  11491  sqr0lem  11728  sqrlem2  11731  sqrlem7  11736  max0add  11797  recval  11808  nnabscl  11811  absmax  11815  sqreulem  11845  climi0  11988  lo1bdd2  12000  rlimresb  12041  lo1eq  12044  rlimeq  12045  isercolllem3  12142  climsup  12145  fsumsplit  12214  fsumcom2  12239  explecnv  12325  eftlub  12391  sin02gt0  12474  rpnnen2lem10  12504  odd2np1  12589  oexpneg  12592  bitsf1  12639  sadcaddlem  12650  bitsuz  12667  rplpwr  12737  rppwr  12738  nn0seqcvgd  12742  qredeq  12787  qgt0numnn  12824  phibndlem  12840  coprimeprodsq2  12865  pythagtrip  12889  fldivp1  12947  unbenlem  12957  4sqlem9  12995  4sqlem15  13008  4sqlem16  13009  vdwlem6  13035  vdwlem10  13039  vdwlem11  13040  vdwlem13  13042  vdw  13043  mreuni  13504  cidpropd  13615  subsubc  13729  ffthiso  13805  fuciso  13851  setcmon  13921  setcepi  13922  catciso  13941  hofcl  14035  hofpropd  14043  yonedalem4c  14053  yonedainv  14057  ipoval  14259  imasmnd  14412  pwsco1mhm  14448  imasgrp  14613  subginv  14630  subgmulg  14637  eqger  14669  subgga  14756  orbstafun  14767  orbsta  14769  symggrp  14782  dfod2  14879  gexval  14891  gex1  14904  sylow2blem1  14933  sylow3lem1  14940  pj1eu  15007  efgredlema  15051  frgp0  15071  frgpmhm  15076  odadd1  15142  0cyg  15181  gsumzres  15196  gsumzsplit  15208  dprd2dlem1  15278  dprd2da  15279  dmdprdsplit2  15283  dprdsplit  15285  pgpfaclem3  15320  ablfac2  15326  imasrng  15404  subrg1  15557  abvneg  15601  lmhmf1o  15805  lmhmima  15806  reslmhm2b  15813  lsmspsn  15839  lspdisj  15880  lidlmcl  15971  fidomndrnglem  16049  mplsubglem  16181  mplmonmul  16210  mplbas2  16214  subrgascl  16241  subrgasclcl  16242  absabv  16431  elcls  16812  clsndisj  16814  isclo2  16827  neiuni  16861  neissex  16866  tgrest  16892  tgcnp  16985  lmfpm  17025  lmcl  17027  lmss  17028  lmff  17031  ist1-2  17077  cnt1  17080  cmpsublem  17128  clscon  17158  kgeni  17234  kgenidm  17244  txcnpi  17304  ptpjopn  17308  ptclsg  17311  txcmplem1  17337  qtoptop2  17392  qtoptopon  17397  r0sep  17441  ptunhmeo  17501  t0kq  17511  fsubbas  17564  neifil  17577  uffixsn  17622  ufildr  17628  rnelfm  17650  isfcls2  17710  uffclsflim  17728  alexsublem  17740  tmdcn2  17774  symgtgp  17786  tsmssplit  17836  xmeter  17981  prdsbl  18039  neibl  18049  methaus  18068  prdsxmslem2  18077  tngngp2  18170  tngngp  18172  tgqioo  18308  xrsxmet  18317  icccmplem1  18329  icccmplem2  18330  cnmpt2pc  18428  iihalf2  18433  icoopnst  18439  iocopnst  18440  xrhmeo  18446  lebnumlem1  18461  lebnumlem3  18463  pi1blem  18539  pi1grplem  18549  pi1xfrf  18553  pi1xfr  18555  pi1xfrcnvlem  18556  pi1cof  18559  pi1coghm  18561  cmetcaulem  18716  causs  18726  metcld  18733  lmcau  18740  minveclem4  18798  ivthlem2  18814  ivthlem3  18815  ivthicc  18820  ovolshftlem1  18870  ovolicc1  18877  ovolicopnf  18885  volfiniun  18906  uniioombllem3  18942  dyaddisjlem  18952  vitalilem2  18966  itg1ge0  19043  mbfi1fseqlem3  19074  xrge0f  19088  itg2seq  19099  itg2monolem1  19107  itg2addlem  19115  itg2gt0  19117  iblcnlem  19145  itgss3  19171  itgsplit  19192  dvnff  19274  dvferm2  19336  dvlip2  19344  dveq0  19349  dvge0  19355  dvcnvre  19368  dvfsumle  19370  dvfsumabs  19372  dvfsumlem2  19376  ftc1lem2  19385  ftc1lem4  19388  ftc1lem5  19389  ftc1cn  19392  ftc2  19393  itgsubstlem  19397  evlsval2  19406  mpfind  19430  coe1mul3  19487  ply1divex  19524  dgrlem  19613  dgrlb  19620  coemulhi  19637  dgrlt  19649  dgrmul  19653  plydivlem4  19678  fta1  19690  aaliou2b  19723  taylplem2  19745  dvtaylp  19751  ulmcau  19774  tanabsge  19876  sinq12gt0  19877  argimgt0  19968  cxplea  20045  cxple2  20046  cxpsqr  20052  cxpaddlelem  20093  loglesqr  20100  ang180lem2  20110  lawcos  20116  logrec  20119  asinlem3a  20168  asinlem3  20169  asinsin  20190  atanlogaddlem  20211  atanlogadd  20212  atanlogsub  20214  atantan  20221  atanbnd  20224  atantayl2  20236  efrlim  20266  wilthlem2  20309  basellem2  20321  sqfpc  20377  ppieq0  20416  sqff1o  20422  fsumdvdscom  20427  ppiub  20445  chpeq0  20449  chtleppi  20451  fsumvma  20454  fsumvma2  20455  mersenne  20468  dchrabs2  20503  dchr1re  20504  dchrpt  20508  lgsdilem  20563  lgsdinn0  20581  lgsquad3  20602  m1lgs  20603  2sqlem6  20610  rpvmasumlem  20638  dchrisumlem3  20642  dchrisum0flblem1  20659  pntibndlem2a  20741  pntlem3  20760  padicabv  20781  vcoprnelem  21136  cnnv  21247  nmounbseqi  21357  nmounbseqiOLD  21358  nmlnogt0  21377  nmblolbii  21379  blocnilem  21384  ajmoi  21439  minvecolem4  21461  hhnv  21746  norm1  21830  hhssnv  21843  pjhtheu  21975  pjpreeq  21979  spanunsni  22160  fh1  22199  fh2  22200  cm2j  22201  chscllem4  22221  pjid  22276  adjmo  22414  eleigveccl  22541  eigvalcl  22543  eigvec1  22544  eighmre  22545  eighmorth  22546  nmop0h  22573  nmbdoplbi  22606  nmcoplbi  22610  nmophmi  22613  lncnopbd  22619  nmbdfnlbi  22631  nmcfnlbi  22634  cnlnadjeui  22659  branmfn  22687  rnbra  22689  nmopleid  22721  strlem5  22837  hstrlem5  22845  dmdbr3  22887  dmdbr4  22888  mdsl3  22898  hatomistici  22944  cvexchlem  22950  chirredlem1  22972  chirredlem2  22973  chirredi  22976  atcvat3i  22978  atcvat4i  22979  atabsi  22983  mdsymlem1  22985  mdsymlem3  22987  mdsymlem5  22989  dmdbr5ati  23004  cdj1i  23015  f1o3d  23039  elpreq  23190  xrofsup  23257  iccgelb  23268  eliccelico  23272  elicoelioo  23273  unitdivcld  23287  xrge0addgt0  23333  xrge0adddir  23334  xrge0npcan  23335  baselsiga  23478  sigasspw  23479  issgon  23486  meascnbl  23548  indf1ofs  23611  probun  23624  subfacp1lem5  23717  subfacp1lem6  23718  erdszelem9  23732  ptpcon  23766  rescon  23779  cvmlift3lem7  23858  eupap1  23902  sspred  24176  trpredrec  24243  axcontlem2  24595  axcontlem12  24605  btwnintr  24644  btwnouttr  24649  cgrxfr  24680  btwnconn1lem12  24723  colinbtwnle  24743  lineelsb2  24773  onintopsscon  24881  areacirclem6  24941  areacirc  24942  mapmapmap  25159  repcpwti  25172  cbicp  25177  valcurfn1  25215  prsubrtr  25410  basexre  25533  limptlimpr2lem2  25586  mslb1  25618  supnuf  25640  ehm  25802  dehm  25803  cehm  25804  idsubfun  25869  domcatfun  25936  codcatfun  25945  pdiveql  26179  nn0prpwlem  26249  locfindis  26316  neibastop3  26322  fdc  26466  incsequz  26469  blbnd  26522  prdstotbnd  26529  cnpwstotbnd  26532  ismtyres  26543  rngohomf  26608  rngohom1  26610  rngohomadd  26611  rngohommul  26612  idlss  26652  idl0cl  26654  idladdcl  26655  idllmulcl  26656  idlrmulcl  26657  maxidlnr  26678  maxidlmax  26679  smprngopr  26688  pridlc  26707  ceqsex3OLD  26737  mzpindd  26835  lzunuz  26858  2rexfrabdioph  26888  irrapxlem3  26920  pellexlem2  26926  pellexlem5  26929  pell1234qrreccl  26950  pell14qrdich  26965  pell1qrge1  26966  elpell1qr2  26968  reglogltb  26987  reglogleb  26988  rmxycomplete  27013  2nn0ind  27041  congabseq  27072  acongrep  27078  acongeq  27081  dvdsleabs2  27088  jm2.22  27099  jm2.26lem3  27105  pw2f1ocnv  27141  limsuc2  27148  fnwe2lem3  27160  aomclem6  27167  kercvrlsm  27192  pwssplit0  27198  pwssplit1  27199  pwssplit4  27202  frlmbas  27234  elfilspd  27266  f1lindf  27303  lpirlnr  27332  hashgcdeq  27528  dvconstbi  27562  mulltgt0  27704  refsumcn  27712  cncmpmax  27714  climinf  27743  climreeq  27750  stoweidlem27  27787  stoweidlem29  27789  stoweidlem31  27791  stoweidlem34  27794  stoweidlem48  27808  stoweidlem59  27819  sigarcol  27865  reuan  27969  ndmaovg  28055  elprchashprn2  28099  s2f1o  28102  s4f1o  28104  usgra1  28130  nbgraop  28151  nbcusgra  28170  bi2imp  28303  biimpa21  28391  a9e2ndeqALT  28781  bnj563  28845  bnj1001  29063  lshpnel2N  29248  islsati  29257  lkr0f  29357  lfl1dim  29384  lfl1dim2N  29385  omlfh1N  29521  leat  29556  atlatmstc  29582  cvlatexch3  29601  lnnat  29689  cvrat3  29704  cvrat4  29705  3dim3  29731  dalem4  29927  dalem39  29973  paddasslem12  30093  psubcliN  30200  pmapojoinN  30230  lhpm0atN  30291  lhprelat3N  30302  trlnid  30441  trlval3  30449  cdleme22b  30603  trljco  31002  diaglbN  31318  dibvalrel  31426  dicvalrelN  31448  diclspsn  31457  dih1dimatlem  31592  dihlatat  31600  lcfl6  31763  lcfl8  31765  lcfrvalsnN  31804  lcfrlem9  31813  mapdheq2  31992  hlhillcs  32224  hlhilhillem  32226
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