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

Theorem biimpa 471
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 199 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
32imp 419 1  |-  ( (
ph  /\  ps )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  simprbda  607  simplbda  608  pm5.1  831  bimsc1  905  biimp3a  1283  equsex  1957  euor  2265  euan  2295  cgsexg  2930  cgsex2g  2931  cgsex4g  2932  ceqsex  2933  sbciegft  3134  sbeqalb  3156  syl5sseq  3339  euotd  4398  ralxfr2d  4679  elpwunsn  4697  limsssuc  4770  relop  4963  resiexg  5128  fnbr  5487  f1o00  5650  dffv2  5735  iinpreima  5799  funressn  5858  fnex  5900  weniso  6014  f1ocnv2d  6234  ofrval  6254  eloprabi  6352  1stconst  6374  2ndconst  6375  frxp  6392  poxp  6394  riotasvdOLD  6529  smodm2  6553  smoiso  6560  tz7.44lem1  6599  oev2  6703  oesuclem  6705  oecl  6717  omordi  6745  omwordri  6751  omword2  6753  omordlim  6756  omlimcl  6757  omeulem2  6762  oeordi  6766  oewordri  6771  oelim2  6774  oeoa  6776  oeoe  6778  nnawordi  6800  nnaordex  6817  erth  6885  iiner  6912  pw2f1olem  7148  pw2f1o  7149  onomeneq  7232  onfin2  7234  unxpdomlem2  7250  isinf  7258  findcard2  7284  fipreima  7347  fipwss  7369  cantnfp1lem3  7569  carden2b  7787  carddomi2  7790  infxpenlem  7828  acni2  7860  numacn  7863  alephfp  7922  pwsdompw  8017  ackbij2lem3  8054  cfeq0  8069  cfsuc  8070  cfsmolem  8083  domfin4  8124  axdc3lem2  8264  axdc3lem4  8266  alephreg  8390  fpwwe2  8451  winainflem  8501  r1limwun  8544  inar1  8583  grudomon  8625  nlt1pi  8716  indpi  8717  nqereu  8739  ltbtwnnq  8788  prlem934  8843  prlem936  8857  addgt0sr  8912  leltne  9097  ne0gt0  9111  mullt0  9479  msqgt0  9480  mulne0  9596  divne0  9622  div2neg  9669  ltmul12a  9798  recgt1i  9839  nn2ge  9957  peano5uzi  10290  eluzp1m1  10441  eluzaddi  10444  eluzsubi  10445  uz2m1nn  10482  rpnnen1lem5  10536  rphalflt  10570  xrleltne  10670  max0sub  10714  xmulpnf1n  10789  xmulge0  10795  xadddi  10806  supxr  10823  supxr2  10824  ixxdisj  10863  ixxun  10864  ixxub  10869  ixxlb  10870  icodisj  10954  difreicc  10960  iccf1o  10971  fzsuc2  11035  elfznelfzo  11119  flge0nn0  11152  flge1nn  11153  seqf1olem2  11290  expubnd  11367  sqlecan  11414  bernneq  11432  bernneq2  11433  expnbnd  11435  discr1  11442  facwordi  11507  faclbnd4lem4  11514  bcpasc  11539  elprchashprn2  11594  iswrdi  11658  ccatass  11677  revccat  11725  revrev  11726  revco  11730  s2f1o  11790  s4f1o  11792  sqr0lem  11973  sqrlem2  11976  sqrlem7  11981  max0add  12042  recval  12053  nnabscl  12056  absmax  12060  sqreulem  12090  climi0  12233  lo1bdd2  12245  rlimresb  12286  lo1eq  12289  rlimeq  12290  isercolllem3  12387  climsup  12390  fsumsplit  12460  fsumcom2  12485  explecnv  12571  eftlub  12637  sin02gt0  12720  rpnnen2lem10  12750  odd2np1  12835  oexpneg  12838  bitsf1  12885  sadcaddlem  12896  bitsuz  12913  rplpwr  12983  rppwr  12984  nn0seqcvgd  12988  qredeq  13033  qgt0numnn  13070  phibndlem  13086  coprimeprodsq2  13111  pythagtrip  13135  fldivp1  13193  unbenlem  13203  4sqlem9  13241  4sqlem15  13254  4sqlem16  13255  vdwlem6  13281  vdwlem10  13285  vdwlem11  13286  vdwlem13  13288  vdw  13289  mreuni  13752  cidpropd  13863  subsubc  13977  ffthiso  14053  fuciso  14099  setcmon  14169  setcepi  14170  catciso  14189  hofcl  14283  hofpropd  14291  yonedalem4c  14301  yonedainv  14305  imasmnd  14660  pwsco1mhm  14696  imasgrp  14861  subginv  14878  subgmulg  14885  eqger  14917  subgga  15004  orbstafun  15015  orbsta  15017  symggrp  15030  dfod2  15127  gexval  15139  gex1  15152  sylow2blem1  15181  sylow3lem1  15188  pj1eu  15255  efgredlema  15299  frgp0  15319  frgpmhm  15324  odadd1  15390  0cyg  15429  gsumzres  15444  gsumzsplit  15456  dprd2dlem1  15526  dprd2da  15527  dmdprdsplit2  15531  dprdsplit  15533  pgpfaclem3  15568  ablfac2  15574  imasrng  15652  subrg1  15805  abvneg  15849  lmhmf1o  16049  lmhmima  16050  reslmhm2b  16057  lsmspsn  16083  lspdisj  16124  lidlmcl  16215  fidomndrnglem  16293  mplsubglem  16425  mplmonmul  16454  mplbas2  16458  subrgascl  16485  subrgasclcl  16486  absabv  16679  elcls  17060  clsndisj  17062  isclo2  17075  neiuni  17109  neissex  17114  neiptopreu  17120  tgrest  17145  neitr  17166  tgcnp  17239  lmfpm  17281  lmcl  17283  lmss  17284  lmff  17287  ist1-2  17333  cnt1  17336  cmpsublem  17384  clscon  17414  kgeni  17490  kgenidm  17500  txcnpi  17561  ptpjopn  17565  ptclsg  17568  txcmplem1  17594  qtoptop2  17652  qtoptopon  17657  r0sep  17701  ptunhmeo  17761  t0kq  17771  fsubbas  17820  neifil  17833  uffixsn  17878  ufildr  17884  rnelfm  17906  isfcls2  17966  uffclsflim  17984  alexsublem  17996  cnextfun  18016  cnextfvval  18017  cnextf  18018  cnextcn  18019  tmdcn2  18040  symgtgp  18052  tsmssplit  18102  ustuni  18177  trust  18180  utoptop  18185  restutop  18188  restutopopn  18189  ustuqtop1  18192  ustuqtop2  18193  ustuqtop3  18194  ustuqtop4  18195  utop2nei  18201  utop3cls  18202  isucn2  18230  ucncn  18236  trcfilu  18245  cfiluweak  18246  xmeter  18353  prdsbl  18411  neibl  18421  methaus  18440  prdsxmslem2  18449  metustto  18473  metustexhalf  18476  metust  18478  cfilucfil  18479  metutop  18487  metucn  18490  tngngp2  18564  tngngp  18566  tgqioo  18702  xrsxmet  18711  icccmplem1  18724  icccmplem2  18725  cnmpt2pc  18824  iihalf2  18829  icoopnst  18835  iocopnst  18836  xrhmeo  18842  lebnumlem1  18857  lebnumlem3  18859  pi1blem  18935  pi1grplem  18945  pi1xfrf  18949  pi1xfr  18951  pi1xfrcnvlem  18952  pi1cof  18955  pi1coghm  18957  cmetcaulem  19112  causs  19122  metcld  19129  lmcau  19136  minveclem4  19200  ivthlem2  19216  ivthlem3  19217  ivthicc  19222  ovolshftlem1  19272  ovolicc1  19279  ovolicopnf  19287  volfiniun  19308  uniioombllem3  19344  dyaddisjlem  19354  vitalilem2  19368  itg1ge0  19445  mbfi1fseqlem3  19476  xrge0f  19490  itg2seq  19501  itg2monolem1  19509  itg2addlem  19517  itg2gt0  19519  iblcnlem  19547  itgss3  19573  itgsplit  19594  dvnff  19676  dvferm2  19738  dvlip2  19746  dveq0  19751  dvge0  19757  dvcnvre  19770  dvfsumle  19772  dvfsumabs  19774  dvfsumlem2  19778  ftc1lem2  19787  ftc1lem4  19790  ftc1lem5  19791  ftc1cn  19794  ftc2  19795  itgsubstlem  19799  evlsval2  19808  mpfind  19832  coe1mul3  19889  ply1divex  19926  dgrlem  20015  dgrlb  20022  coemulhi  20039  dgrlt  20051  dgrmul  20055  plydivlem4  20080  fta1  20092  aaliou2b  20125  taylplem2  20147  dvtaylp  20153  ulmcau  20178  tanabsge  20281  sinq12gt0  20282  argimgt0  20374  cxplea  20454  cxple2  20455  cxpsqr  20461  cxpaddlelem  20502  loglesqr  20509  ang180lem2  20519  lawcos  20525  logrec  20528  asinlem3a  20577  asinlem3  20578  asinsin  20599  atanlogaddlem  20620  atanlogadd  20621  atanlogsub  20623  atantan  20630  atanbnd  20633  atantayl2  20645  efrlim  20675  wilthlem2  20719  basellem2  20731  sqfpc  20787  ppieq0  20826  sqff1o  20832  fsumdvdscom  20837  ppiub  20855  chpeq0  20859  chtleppi  20861  fsumvma  20864  fsumvma2  20865  mersenne  20878  dchrabs2  20913  dchr1re  20914  dchrpt  20918  lgsdilem  20973  lgsdinn0  20991  lgsquad3  21012  m1lgs  21013  2sqlem6  21020  rpvmasumlem  21048  dchrisumlem3  21052  dchrisum0flblem1  21069  pntibndlem2a  21151  pntlem3  21170  padicabv  21191  usgra1  21260  usgraedg4  21272  nbgraop  21302  nbgracnvfv  21316  nbcusgra  21338  wlkdvspthlem  21455  fargshiftf1  21472  fargshiftfo  21473  eupatrl  21538  eupap1  21546  vcoprnelem  21905  cnnv  22016  nmounbseqi  22126  nmounbseqiOLD  22127  nmlnogt0  22146  nmblolbii  22148  blocnilem  22153  ajmoi  22208  minvecolem4  22230  hhnv  22515  norm1  22599  hhssnv  22612  pjhtheu  22744  pjpreeq  22748  spanunsni  22929  fh1  22968  fh2  22969  cm2j  22970  chscllem4  22990  pjid  23045  adjmo  23183  eleigveccl  23310  eigvalcl  23312  eigvec1  23313  eighmre  23314  eighmorth  23315  nmop0h  23342  nmbdoplbi  23375  nmcoplbi  23379  nmophmi  23382  lncnopbd  23388  nmbdfnlbi  23400  nmcfnlbi  23403  cnlnadjeui  23428  branmfn  23456  rnbra  23458  nmopleid  23490  strlem5  23606  hstrlem5  23614  dmdbr3  23656  dmdbr4  23657  mdsl3  23667  hatomistici  23713  cvexchlem  23719  chirredlem1  23741  chirredlem2  23742  chirredi  23745  atcvat3i  23747  atcvat4i  23748  atabsi  23752  mdsymlem1  23754  mdsymlem3  23756  mdsymlem5  23758  dmdbr5ati  23773  cdj1i  23784  elabreximd  23835  elpreq  23843  f1o3d  23884  disjdsct  23931  xrofsup  23962  iccgelb  23972  eliccelico  23976  elicoelioo  23977  numdenneg  23998  xrge0addgt0  24043  xrge0adddir  24044  xrge0npcan  24045  kerf1hrm  24078  unitdivcld  24103  cnre2csqlem  24112  fmcncfil  24121  lmxrge0  24141  zrhunitpreima  24161  elzdif0  24163  qqhval2lem  24164  qqhf  24169  indf1ofs  24219  esumfsup  24256  esumpcvgval  24264  sigasspw  24295  issgon  24302  meascnbl  24367  voliune  24379  volfiniune  24380  ballotlemfrcn0  24566  ballotlemirc  24568  subfacp1lem5  24649  subfacp1lem6  24650  erdszelem9  24664  ptpcon  24699  rescon  24712  cvmlift3lem7  24791  fprodser  25054  fprodsplit  25068  sspred  25198  trpredrec  25265  axcontlem2  25618  axcontlem12  25628  btwnintr  25667  btwnouttr  25672  cgrxfr  25703  btwnconn1lem12  25746  colinbtwnle  25766  lineelsb2  25796  onintopsscon  25904  itg2gt0cn  25960  ftc1cnnclem  25978  ftc1cnnc  25979  areacirclem6  25987  areacirc  25988  nn0prpwlem  26016  locfindis  26076  neibastop3  26082  fdc  26140  incsequz  26143  blbnd  26187  prdstotbnd  26194  cnpwstotbnd  26197  ismtyres  26208  rngohomf  26273  rngohom1  26275  rngohomadd  26276  rngohommul  26277  idlss  26317  idl0cl  26319  idladdcl  26320  idllmulcl  26321  idlrmulcl  26322  maxidlnr  26343  maxidlmax  26344  smprngopr  26353  pridlc  26372  ceqsex3OLD  26400  mzpindd  26494  lzunuz  26517  2rexfrabdioph  26547  irrapxlem3  26578  pellexlem2  26584  pellexlem5  26587  pell1234qrreccl  26608  pell14qrdich  26623  pell1qrge1  26624  elpell1qr2  26626  reglogltb  26645  reglogleb  26646  rmxycomplete  26671  2nn0ind  26699  congabseq  26730  acongrep  26736  acongeq  26739  dvdsleabs2  26746  jm2.22  26757  jm2.26lem3  26763  pw2f1ocnv  26799  limsuc2  26806  fnwe2lem3  26818  aomclem6  26825  kercvrlsm  26850  pwssplit0  26856  pwssplit1  26857  pwssplit4  26860  frlmbas  26892  elfilspd  26924  f1lindf  26961  lpirlnr  26990  hashgcdeq  27186  dvconstbi  27220  mulltgt0  27361  refsumcn  27369  cncmpmax  27371  climinf  27400  climreeq  27407  stoweidlem27  27444  stoweidlem29  27446  stoweidlem31  27448  stoweidlem34  27451  stoweidlem48  27465  stoweidlem59  27476  sigarcol  27522  reuan  27626  ndmaovg  27717  frgrancvvdeqlemA  27789  frgrancvvdeqlemB  27790  frgrancvvdeqlemC  27791  frgrawopreglem4  27799  bi2imp  27911  a9e2ndeqALT  28385  bnj563  28449  bnj1001  28667  lshpnel2N  29100  islsati  29109  lkr0f  29209  lfl1dim  29236  lfl1dim2N  29237  omlfh1N  29373  leat  29408  atlatmstc  29434  cvlatexch3  29453  lnnat  29541  cvrat3  29556  cvrat4  29557  3dim3  29583  dalem4  29779  dalem39  29825  paddasslem12  29945  psubcliN  30052  pmapojoinN  30082  lhpm0atN  30143  lhprelat3N  30154  trlnid  30293  trlval3  30301  cdleme22b  30455  trljco  30854  diaglbN  31170  dibvalrel  31278  dicvalrelN  31300  diclspsn  31309  dih1dimatlem  31444  dihlatat  31452  lcfl6  31615  lcfl8  31617  lcfrvalsnN  31656  lcfrlem9  31665  mapdheq2  31844  hlhillcs  32076  hlhilhillem  32078
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 178  df-an 361
  Copyright terms: Public domain W3C validator