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  2171  euan  2201  cgsexg  2820  cgsex2g  2821  cgsex4g  2822  ceqsex  2823  sbciegft  3022  sbeqalb  3044  syl5sseq  3227  euotd  4266  ralxfr2d  4549  elpwunsn  4567  limsssuc  4640  relop  4833  resiexg  4996  fnbr  5312  f1o00  5474  dffv2  5554  iinpreima  5617  funressn  5668  fnex  5703  weniso  5814  f1ocnv2d  6030  ofrval  6050  eloprabi  6148  1stconst  6169  2ndconst  6170  frxp  6187  poxp  6189  riotasvdOLD  6344  smodm2  6368  smoiso  6375  tz7.44lem1  6414  oev2  6518  oesuclem  6520  oecl  6532  omordi  6560  omwordri  6566  omword2  6568  omordlim  6571  omlimcl  6572  omeulem2  6577  oeordi  6581  oewordri  6586  oelim2  6589  oeoa  6591  oeoe  6593  nnawordi  6615  nnaordex  6632  erth  6700  iiner  6727  pw2f1olem  6962  pw2f1o  6963  onomeneq  7046  onfin2  7048  unxpdomlem2  7064  isinf  7072  findcard2  7094  fipreima  7157  fipwss  7178  cantnfp1lem3  7378  carden2b  7596  carddomi2  7599  infxpenlem  7637  acni2  7669  numacn  7672  alephfp  7731  pwsdompw  7826  ackbij2lem3  7863  cfeq0  7878  cfsuc  7879  cfsmolem  7892  domfin4  7933  axdc3lem2  8073  axdc3lem4  8075  alephreg  8200  fpwwe2  8261  winainflem  8311  r1limwun  8354  inar1  8393  grudomon  8435  nlt1pi  8526  indpi  8527  nqereu  8549  ltbtwnnq  8598  prlem934  8653  prlem936  8667  addgt0sr  8722  leltne  8907  ne0gt0  8921  mullt0  9289  msqgt0  9290  mulne0  9406  divne0  9432  div2neg  9479  ltmul12a  9608  recgt1i  9649  nn2ge  9767  peano5uzi  10096  eluzp1m1  10247  eluzaddi  10250  eluzsubi  10251  uz2m1nn  10288  rpnnen1lem5  10342  rphalflt  10376  xrleltne  10475  max0sub  10519  xmulpnf1n  10594  xmulge0  10600  xadddi  10611  supxr  10627  supxr2  10628  ixxdisj  10667  ixxun  10668  ixxub  10673  ixxlb  10674  icodisj  10757  difreicc  10763  iccf1o  10774  fzsuc2  10838  flge0nn0  10944  flge1nn  10945  seqf1olem2  11082  expubnd  11158  sqlecan  11205  bernneq  11223  bernneq2  11224  expnbnd  11226  discr1  11233  facwordi  11298  faclbnd4lem4  11305  bcpasc  11329  iswrdi  11413  ccatass  11432  revccat  11480  revrev  11481  revco  11485  sqr0lem  11722  sqrlem2  11725  sqrlem7  11730  max0add  11791  recval  11802  nnabscl  11805  absmax  11809  sqreulem  11839  climi0  11982  lo1bdd2  11994  rlimresb  12035  lo1eq  12038  rlimeq  12039  isercolllem3  12136  climsup  12139  fsumsplit  12208  fsumcom2  12233  explecnv  12319  eftlub  12385  sin02gt0  12468  rpnnen2lem10  12498  odd2np1  12583  oexpneg  12586  bitsf1  12633  sadcaddlem  12644  bitsuz  12661  rplpwr  12731  rppwr  12732  nn0seqcvgd  12736  qredeq  12781  qgt0numnn  12818  phibndlem  12834  coprimeprodsq2  12859  pythagtrip  12883  fldivp1  12941  unbenlem  12951  4sqlem9  12989  4sqlem15  13002  4sqlem16  13003  vdwlem6  13029  vdwlem10  13033  vdwlem11  13034  vdwlem13  13036  vdw  13037  mreuni  13498  cidpropd  13609  subsubc  13723  ffthiso  13799  fuciso  13845  setcmon  13915  setcepi  13916  catciso  13935  hofcl  14029  hofpropd  14037  yonedalem4c  14047  yonedainv  14051  ipoval  14253  imasmnd  14406  pwsco1mhm  14442  imasgrp  14607  subginv  14624  subgmulg  14631  eqger  14663  subgga  14750  orbstafun  14761  orbsta  14763  symggrp  14776  dfod2  14873  gexval  14885  gex1  14898  sylow2blem1  14927  sylow3lem1  14934  pj1eu  15001  efgredlema  15045  frgp0  15065  frgpmhm  15070  odadd1  15136  0cyg  15175  gsumzres  15190  gsumzsplit  15202  dprd2dlem1  15272  dprd2da  15273  dmdprdsplit2  15277  dprdsplit  15279  pgpfaclem3  15314  ablfac2  15320  imasrng  15398  subrg1  15551  abvneg  15595  lmhmf1o  15799  lmhmima  15800  reslmhm2b  15807  lsmspsn  15833  lspdisj  15874  lidlmcl  15965  fidomndrnglem  16043  mplsubglem  16175  mplmonmul  16204  mplbas2  16208  subrgascl  16235  subrgasclcl  16236  absabv  16425  elcls  16806  clsndisj  16808  isclo2  16821  neiuni  16855  neissex  16860  tgrest  16886  tgcnp  16979  lmfpm  17019  lmcl  17021  lmss  17022  lmff  17025  ist1-2  17071  cnt1  17074  cmpsublem  17122  clscon  17152  kgeni  17228  kgenidm  17238  txcnpi  17298  ptpjopn  17302  ptclsg  17305  txcmplem1  17331  qtoptop2  17386  qtoptopon  17391  r0sep  17435  ptunhmeo  17495  t0kq  17505  fsubbas  17558  neifil  17571  uffixsn  17616  ufildr  17622  rnelfm  17644  isfcls2  17704  uffclsflim  17722  alexsublem  17734  tmdcn2  17768  symgtgp  17780  tsmssplit  17830  xmeter  17975  prdsbl  18033  neibl  18043  methaus  18062  prdsxmslem2  18071  tngngp2  18164  tngngp  18166  tgqioo  18302  xrsxmet  18311  icccmplem1  18323  icccmplem2  18324  cnmpt2pc  18422  iihalf2  18427  icoopnst  18433  iocopnst  18434  xrhmeo  18440  lebnumlem1  18455  lebnumlem3  18457  pi1blem  18533  pi1grplem  18543  pi1xfrf  18547  pi1xfr  18549  pi1xfrcnvlem  18550  pi1cof  18553  pi1coghm  18555  cmetcaulem  18710  causs  18720  metcld  18727  lmcau  18734  minveclem4  18792  ivthlem2  18808  ivthlem3  18809  ivthicc  18814  ovolshftlem1  18864  ovolicc1  18871  ovolicopnf  18879  volfiniun  18900  uniioombllem3  18936  dyaddisjlem  18946  vitalilem2  18960  itg1ge0  19037  mbfi1fseqlem3  19068  xrge0f  19082  itg2seq  19093  itg2monolem1  19101  itg2addlem  19109  itg2gt0  19111  iblcnlem  19139  itgss3  19165  itgsplit  19186  dvnff  19268  dvferm2  19330  dvlip2  19338  dveq0  19343  dvge0  19349  dvcnvre  19362  dvfsumle  19364  dvfsumabs  19366  dvfsumlem2  19370  ftc1lem2  19379  ftc1lem4  19382  ftc1lem5  19383  ftc1cn  19386  ftc2  19387  itgsubstlem  19391  evlsval2  19400  mpfind  19424  coe1mul3  19481  ply1divex  19518  dgrlem  19607  dgrlb  19614  coemulhi  19631  dgrlt  19643  dgrmul  19647  plydivlem4  19672  fta1  19684  aaliou2b  19717  taylplem2  19739  dvtaylp  19745  ulmcau  19768  tanabsge  19870  sinq12gt0  19871  argimgt0  19962  cxplea  20039  cxple2  20040  cxpsqr  20046  cxpaddlelem  20087  loglesqr  20094  ang180lem2  20104  lawcos  20110  logrec  20113  asinlem3a  20162  asinlem3  20163  asinsin  20184  atanlogaddlem  20205  atanlogadd  20206  atanlogsub  20208  atantan  20215  atanbnd  20218  atantayl2  20230  efrlim  20260  wilthlem2  20303  basellem2  20315  sqfpc  20371  ppieq0  20410  sqff1o  20416  fsumdvdscom  20421  ppiub  20439  chpeq0  20443  chtleppi  20445  fsumvma  20448  fsumvma2  20449  mersenne  20462  dchrabs2  20497  dchr1re  20498  dchrpt  20502  lgsdilem  20557  lgsdinn0  20575  lgsquad3  20596  m1lgs  20597  2sqlem6  20604  rpvmasumlem  20632  dchrisumlem3  20636  dchrisum0flblem1  20653  pntibndlem2a  20735  pntlem3  20754  padicabv  20775  vcoprnelem  21128  cnnv  21239  nmounbseqi  21349  nmounbseqiOLD  21350  nmlnogt0  21369  nmblolbii  21371  blocnilem  21376  ajmoi  21431  minvecolem4  21453  hhnv  21740  norm1  21824  hhssnv  21837  pjhtheu  21969  pjpreeq  21973  spanunsni  22154  fh1  22193  fh2  22194  cm2j  22195  chscllem4  22215  pjid  22270  adjmo  22408  eleigveccl  22535  eigvalcl  22537  eigvec1  22538  eighmre  22539  eighmorth  22540  nmop0h  22567  nmbdoplbi  22600  nmcoplbi  22604  nmophmi  22607  lncnopbd  22613  nmbdfnlbi  22625  nmcfnlbi  22628  cnlnadjeui  22653  branmfn  22681  rnbra  22683  nmopleid  22715  strlem5  22831  hstrlem5  22839  dmdbr3  22881  dmdbr4  22882  mdsl3  22892  hatomistici  22938  cvexchlem  22944  chirredlem1  22966  chirredlem2  22967  chirredi  22970  atcvat3i  22972  atcvat4i  22973  atabsi  22977  mdsymlem1  22979  mdsymlem3  22981  mdsymlem5  22983  dmdbr5ati  22998  cdj1i  23009  f1o3d  23033  subfacp1lem5  23122  subfacp1lem6  23123  erdszelem9  23137  ptpcon  23171  rescon  23184  cvmlift3lem7  23263  eupap1  23307  sspred  23578  trpredrec  23645  axcontlem2  24003  axcontlem12  24013  btwnintr  24052  btwnouttr  24057  cgrxfr  24088  btwnconn1lem12  24131  colinbtwnle  24151  lineelsb2  24181  onintopsscon  24289  areacirclem6  24340  areacirc  24341  mapmapmap  24559  repcpwti  24572  cbicp  24577  valcurfn1  24615  prsubrtr  24810  basexre  24933  limptlimpr2lem2  24986  mslb1  25018  supnuf  25040  ehm  25202  dehm  25203  cehm  25204  idsubfun  25269  domcatfun  25336  codcatfun  25345  pdiveql  25579  nn0prpwlem  25649  locfindis  25716  neibastop3  25722  fdc  25866  incsequz  25869  blbnd  25922  prdstotbnd  25929  cnpwstotbnd  25932  ismtyres  25943  rngohomf  26008  rngohom1  26010  rngohomadd  26011  rngohommul  26012  idlss  26052  idl0cl  26054  idladdcl  26055  idllmulcl  26056  idlrmulcl  26057  maxidlnr  26078  maxidlmax  26079  smprngopr  26088  pridlc  26107  ceqsex3OLD  26137  mzpindd  26235  lzunuz  26258  2rexfrabdioph  26288  irrapxlem3  26320  pellexlem2  26326  pellexlem5  26329  pell1234qrreccl  26350  pell14qrdich  26365  pell1qrge1  26366  elpell1qr2  26368  reglogltb  26387  reglogleb  26388  rmxycomplete  26413  2nn0ind  26441  congabseq  26472  acongrep  26478  acongeq  26481  dvdsleabs2  26488  jm2.22  26499  jm2.26lem3  26505  pw2f1ocnv  26541  limsuc2  26548  fnwe2lem3  26560  aomclem6  26567  kercvrlsm  26592  pwssplit0  26598  pwssplit1  26599  pwssplit4  26602  frlmbas  26634  elfilspd  26666  f1lindf  26703  lpirlnr  26732  hashgcdeq  26928  dvconstbi  26962  mulltgt0  27104  refsumcn  27112  cncmpmax  27114  climinf  27143  climreeq  27150  stoweidlem27  27187  stoweidlem29  27189  stoweidlem31  27191  stoweidlem34  27194  stoweidlem48  27208  stoweidlem59  27219  reuan  27349  ndmaovg  27435  biimpa21  27618  a9e2ndeqALT  27988  bnj563  28051  bnj1001  28269  lshpnel2N  28454  islsati  28463  lkr0f  28563  lfl1dim  28590  lfl1dim2N  28591  omlfh1N  28727  leat  28762  atlatmstc  28788  cvlatexch3  28807  lnnat  28895  cvrat3  28910  cvrat4  28911  3dim3  28937  dalem4  29133  dalem39  29179  paddasslem12  29299  psubcliN  29406  pmapojoinN  29436  lhpm0atN  29497  lhprelat3N  29508  trlnid  29647  trlval3  29655  cdleme22b  29809  trljco  30208  diaglbN  30524  dibvalrel  30632  dicvalrelN  30654  diclspsn  30663  dih1dimatlem  30798  dihlatat  30806  lcfl6  30969  lcfl8  30971  lcfrvalsnN  31010  lcfrlem9  31019  mapdheq2  31198  hlhillcs  31430  hlhilhillem  31432
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