MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  biimpa Structured version   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  2002  sbie  2122  euor  2307  euan  2337  cgsexg  2979  cgsex2g  2980  cgsex4g  2981  ceqsex  2982  sbciegft  3183  sbeqalb  3205  syl5sseq  3388  euotd  4449  ralxfr2d  4731  elpwunsn  4749  limsssuc  4822  relop  5015  resiexg  5180  fnbr  5539  f1o00  5702  dffv2  5788  iinpreima  5852  funressn  5911  fnex  5953  weniso  6067  f1ocnv2d  6287  ofrval  6307  eloprabi  6405  1stconst  6427  2ndconst  6428  frxp  6448  poxp  6450  riotasvdOLD  6585  smodm2  6609  smoiso  6616  tz7.44lem1  6655  oev2  6759  oesuclem  6761  oecl  6773  omordi  6801  omwordri  6807  omword2  6809  omordlim  6812  omlimcl  6813  omeulem2  6818  oeordi  6822  oewordri  6827  oelim2  6830  oeoa  6832  oeoe  6834  nnawordi  6856  nnaordex  6873  erth  6941  iiner  6968  pw2f1olem  7204  pw2f1o  7205  onomeneq  7288  onfin2  7290  unxpdomlem2  7306  isinf  7314  findcard2  7340  fipreima  7404  fipwss  7426  cantnfp1lem3  7626  carden2b  7844  carddomi2  7847  infxpenlem  7885  acni2  7917  numacn  7920  alephfp  7979  pwsdompw  8074  ackbij2lem3  8111  cfeq0  8126  cfsuc  8127  cfsmolem  8140  domfin4  8181  axdc3lem2  8321  axdc3lem4  8323  alephreg  8447  fpwwe2  8508  winainflem  8558  r1limwun  8601  inar1  8640  grudomon  8682  nlt1pi  8773  indpi  8774  nqereu  8796  ltbtwnnq  8845  prlem934  8900  prlem936  8914  addgt0sr  8969  leltne  9154  ne0gt0  9168  mullt0  9537  msqgt0  9538  mulne0  9654  divne0  9680  div2neg  9727  ltmul12a  9856  recgt1i  9897  nn2ge  10015  peano5uzi  10348  eluzp1m1  10499  eluzaddi  10502  eluzsubi  10503  uz2m1nn  10540  rpnnen1lem5  10594  rphalflt  10628  xrleltne  10728  max0sub  10772  xmulpnf1n  10847  xmulge0  10853  xadddi  10864  supxr  10881  supxr2  10882  ixxdisj  10921  ixxun  10922  ixxub  10927  ixxlb  10928  icodisj  11012  difreicc  11018  iccf1o  11029  fzsuc2  11094  elfznelfzo  11182  flge0nn0  11215  flge1nn  11216  seqf1olem2  11353  expubnd  11430  sqlecan  11477  bernneq  11495  bernneq2  11496  expnbnd  11498  discr1  11505  facwordi  11570  faclbnd4lem4  11577  bcpasc  11602  elprchashprn2  11657  iswrdi  11721  ccatass  11740  revccat  11788  revrev  11789  revco  11793  s2f1o  11853  s4f1o  11855  sqr0lem  12036  sqrlem2  12039  sqrlem7  12044  max0add  12105  recval  12116  nnabscl  12119  absmax  12123  sqreulem  12153  climi0  12296  lo1bdd2  12308  rlimresb  12349  lo1eq  12352  rlimeq  12353  isercolllem3  12450  climsup  12453  fsumsplit  12523  fsumcom2  12548  explecnv  12634  eftlub  12700  sin02gt0  12783  rpnnen2lem10  12813  odd2np1  12898  oexpneg  12901  bitsf1  12948  sadcaddlem  12959  bitsuz  12976  rplpwr  13046  rppwr  13047  nn0seqcvgd  13051  qredeq  13096  qgt0numnn  13133  phibndlem  13149  coprimeprodsq2  13174  pythagtrip  13198  fldivp1  13256  unbenlem  13266  4sqlem9  13304  4sqlem15  13317  4sqlem16  13318  vdwlem6  13344  vdwlem10  13348  vdwlem11  13349  vdwlem13  13351  vdw  13352  mreuni  13815  cidpropd  13926  subsubc  14040  ffthiso  14116  fuciso  14162  setcmon  14232  setcepi  14233  catciso  14252  hofcl  14346  hofpropd  14354  yonedalem4c  14364  yonedainv  14368  imasmnd  14723  pwsco1mhm  14759  imasgrp  14924  subginv  14941  subgmulg  14948  eqger  14980  subgga  15067  orbstafun  15078  orbsta  15080  symggrp  15093  dfod2  15190  gexval  15202  gex1  15215  sylow2blem1  15244  sylow3lem1  15251  pj1eu  15318  efgredlema  15362  frgp0  15382  frgpmhm  15387  odadd1  15453  0cyg  15492  gsumzres  15507  gsumzsplit  15519  dprd2dlem1  15589  dprd2da  15590  dmdprdsplit2  15594  dprdsplit  15596  pgpfaclem3  15631  ablfac2  15637  imasrng  15715  subrg1  15868  abvneg  15912  lmhmf1o  16112  lmhmima  16113  reslmhm2b  16120  lsmspsn  16146  lspdisj  16187  lidlmcl  16278  fidomndrnglem  16356  mplsubglem  16488  mplmonmul  16517  mplbas2  16521  subrgascl  16548  subrgasclcl  16549  absabv  16746  elcls  17127  clsndisj  17129  isclo2  17142  neiuni  17176  neissex  17181  neiptopreu  17187  tgrest  17213  neitr  17234  tgcnp  17307  lmfpm  17349  lmcl  17351  lmss  17352  lmff  17355  ist1-2  17401  cnt1  17404  cmpsublem  17452  clscon  17483  kgeni  17559  kgenidm  17569  txcnpi  17630  ptpjopn  17634  ptclsg  17637  txcmplem1  17663  qtoptop2  17721  qtoptopon  17726  r0sep  17770  ptunhmeo  17830  t0kq  17840  fsubbas  17889  neifil  17902  uffixsn  17947  ufildr  17953  rnelfm  17975  isfcls2  18035  uffclsflim  18053  alexsublem  18065  cnextfun  18085  cnextfvval  18086  cnextf  18087  cnextcn  18088  tmdcn2  18109  symgtgp  18121  tsmssplit  18171  ustuni  18246  trust  18249  utoptop  18254  restutop  18257  restutopopn  18258  ustuqtop1  18261  ustuqtop2  18262  ustuqtop3  18263  ustuqtop4  18264  utop2nei  18270  utop3cls  18271  isucn2  18299  ucncn  18305  trcfilu  18314  cfiluweak  18315  psmetdmdm  18326  xblss2ps  18421  xmeter  18453  prdsbl  18511  neibl  18521  methaus  18540  prdsxmslem2  18549  metusttoOLD  18577  metustto  18578  metustexhalfOLD  18583  metustexhalf  18584  metustOLD  18587  metust  18588  cfilucfilOLD  18589  cfilucfil  18590  metutopOLD  18602  psmetutop  18603  metucnOLD  18608  metucn  18609  tngngp2  18683  tngngp  18685  tgqioo  18821  xrsxmet  18830  icccmplem1  18843  icccmplem2  18844  cnmpt2pc  18943  iihalf2  18948  icoopnst  18954  iocopnst  18955  xrhmeo  18961  lebnumlem1  18976  lebnumlem3  18978  pi1blem  19054  pi1grplem  19064  pi1xfrf  19068  pi1xfr  19070  pi1xfrcnvlem  19071  pi1cof  19074  pi1coghm  19076  cmetcaulem  19231  causs  19241  metcld  19248  lmcau  19255  cmetcusp  19298  minveclem4  19323  ivthlem2  19339  ivthlem3  19340  ivthicc  19345  ovolshftlem1  19395  ovolicc1  19402  ovolicopnf  19410  volfiniun  19431  uniioombllem3  19467  dyaddisjlem  19477  vitalilem2  19491  itg1ge0  19568  mbfi1fseqlem3  19599  xrge0f  19613  itg2seq  19624  itg2monolem1  19632  itg2addlem  19640  itg2gt0  19642  iblcnlem  19670  itgss3  19696  itgsplit  19717  dvnff  19799  dvferm2  19861  dvlip2  19869  dveq0  19874  dvge0  19880  dvcnvre  19893  dvfsumle  19895  dvfsumabs  19897  dvfsumlem2  19901  ftc1lem2  19910  ftc1lem4  19913  ftc1lem5  19914  ftc1cn  19917  ftc2  19918  itgsubstlem  19922  evlsval2  19931  mpfind  19955  coe1mul3  20012  ply1divex  20049  dgrlem  20138  dgrlb  20145  coemulhi  20162  dgrlt  20174  dgrmul  20178  plydivlem4  20203  fta1  20215  aaliou2b  20248  taylplem2  20270  dvtaylp  20276  ulmcau  20301  tanabsge  20404  sinq12gt0  20405  argimgt0  20497  cxplea  20577  cxple2  20578  cxpsqr  20584  cxpaddlelem  20625  loglesqr  20632  ang180lem2  20642  lawcos  20648  logrec  20651  asinlem3a  20700  asinlem3  20701  asinsin  20722  atanlogaddlem  20743  atanlogadd  20744  atanlogsub  20746  atantan  20753  atanbnd  20756  atantayl2  20768  efrlim  20798  wilthlem2  20842  basellem2  20854  sqfpc  20910  ppieq0  20949  sqff1o  20955  fsumdvdscom  20960  ppiub  20978  chpeq0  20982  chtleppi  20984  fsumvma  20987  fsumvma2  20988  mersenne  21001  dchrabs2  21036  dchr1re  21037  dchrpt  21041  lgsdilem  21096  lgsdinn0  21114  lgsquad3  21135  m1lgs  21136  2sqlem6  21143  rpvmasumlem  21171  dchrisumlem3  21175  dchrisum0flblem1  21192  pntibndlem2a  21274  pntlem3  21293  padicabv  21314  usgra1  21383  usgraedg4  21396  nbgraop  21426  nbgracnvfv  21440  nbcusgra  21462  wlkdvspthlem  21597  fargshiftf1  21614  fargshiftfo  21615  eupatrl  21680  eupap1  21688  vcoprnelem  22047  cnnv  22158  nmounbseqi  22268  nmounbseqiOLD  22269  nmlnogt0  22288  nmblolbii  22290  blocnilem  22295  ajmoi  22350  minvecolem4  22372  hhnv  22657  norm1  22741  hhssnv  22754  pjhtheu  22886  pjpreeq  22890  spanunsni  23071  fh1  23110  fh2  23111  cm2j  23112  chscllem4  23132  pjid  23187  adjmo  23325  eleigveccl  23452  eigvalcl  23454  eigvec1  23455  eighmre  23456  eighmorth  23457  nmop0h  23484  nmbdoplbi  23517  nmcoplbi  23521  nmophmi  23524  lncnopbd  23530  nmbdfnlbi  23542  nmcfnlbi  23545  cnlnadjeui  23570  branmfn  23598  rnbra  23600  nmopleid  23632  strlem5  23748  hstrlem5  23756  dmdbr3  23798  dmdbr4  23799  mdsl3  23809  hatomistici  23855  cvexchlem  23861  chirredlem1  23883  chirredlem2  23884  chirredi  23887  atcvat3i  23889  atcvat4i  23890  atabsi  23894  mdsymlem1  23896  mdsymlem3  23898  mdsymlem5  23900  dmdbr5ati  23915  cdj1i  23926  elabreximd  23981  elpreq  23989  f1o3d  24031  disjdsct  24080  xrofsup  24116  iccgelb  24126  eliccelico  24130  elicoelioo  24131  numdenneg  24150  xrge0addgt0  24204  xrge0adddir  24205  xrge0npcan  24206  kerf1hrm  24252  metideq  24278  unitdivcld  24289  cnre2csqlem  24298  fmcncfil  24307  lmxrge0  24327  zrhunitpreima  24352  elzdif0  24354  qqhval2lem  24355  qqhf  24360  indf1ofs  24413  esumfsup  24450  esumpcvgval  24458  sigasspw  24489  issgon  24496  meascnbl  24563  voliune  24575  volfiniune  24576  ballotlemfrcn0  24777  ballotlemirc  24779  subfacp1lem5  24860  subfacp1lem6  24861  erdszelem9  24875  ptpcon  24910  rescon  24923  cvmlift3lem7  25002  fprodser  25265  fprodsplit  25279  fprodcom2  25298  sspred  25434  trpredrec  25501  axcontlem2  25869  axcontlem12  25879  btwnintr  25918  btwnouttr  25923  cgrxfr  25954  btwnconn1lem12  25997  colinbtwnle  26017  lineelsb2  26047  onintopsscon  26155  mblfinlem  26207  itg2gt0cn  26223  itgaddnclem2  26227  ftc1cnnclem  26241  ftc1cnnc  26242  areacirclem6  26250  areacirc  26251  nn0prpwlem  26279  locfindis  26339  neibastop3  26345  fdc  26403  incsequz  26406  blbnd  26450  prdstotbnd  26457  cnpwstotbnd  26460  ismtyres  26471  rngohomf  26536  rngohom1  26538  rngohomadd  26539  rngohommul  26540  idlss  26580  idl0cl  26582  idladdcl  26583  idllmulcl  26584  idlrmulcl  26585  maxidlnr  26606  maxidlmax  26607  smprngopr  26616  pridlc  26635  ceqsex3OLD  26663  mzpindd  26757  lzunuz  26780  2rexfrabdioph  26810  irrapxlem3  26841  pellexlem2  26847  pellexlem5  26850  pell1234qrreccl  26871  pell14qrdich  26886  pell1qrge1  26887  elpell1qr2  26889  reglogltb  26908  reglogleb  26909  rmxycomplete  26934  2nn0ind  26962  congabseq  26993  acongrep  26999  acongeq  27002  dvdsleabs2  27009  jm2.22  27020  jm2.26lem3  27026  pw2f1ocnv  27062  limsuc2  27069  fnwe2lem3  27081  aomclem6  27088  kercvrlsm  27113  pwssplit0  27119  pwssplit1  27120  pwssplit4  27123  frlmbas  27155  elfilspd  27187  f1lindf  27224  lpirlnr  27253  hashgcdeq  27449  dvconstbi  27483  mulltgt0  27624  refsumcn  27632  cncmpmax  27634  climinf  27663  climreeq  27670  stoweidlem27  27707  stoweidlem29  27709  stoweidlem31  27711  stoweidlem34  27714  stoweidlem48  27728  stoweidlem59  27739  sigarcol  27785  reuan  27889  ndmaovg  27979  fzonmapblen  28081  2submod  28094  iswrd0i  28110  wrdsymb0  28111  ccatsymb  28116  swrd0swrd  28127  swrdswrdlem  28128  swrdswrd  28129  swrdswrd0  28131  swrdccatin12lem3b  28139  reumodprminv  28157  usgra2pthlem1  28227  usg2spthonot  28272  frgrancvvdeqlemA  28327  frgrancvvdeqlemB  28328  frgrancvvdeqlemC  28329  frgrawopreglem4  28337  bi2imp  28466  a9e2ndeqALT  28944  bnj563  29012  bnj1001  29230  lshpnel2N  29684  islsati  29693  lkr0f  29793  lfl1dim  29820  lfl1dim2N  29821  omlfh1N  29957  leat  29992  atlatmstc  30018  cvlatexch3  30037  lnnat  30125  cvrat3  30140  cvrat4  30141  3dim3  30167  dalem4  30363  dalem39  30409  paddasslem12  30529  psubcliN  30636  pmapojoinN  30666  lhpm0atN  30727  lhprelat3N  30738  trlnid  30877  trlval3  30885  cdleme22b  31039  trljco  31438  diaglbN  31754  dibvalrel  31862  dicvalrelN  31884  diclspsn  31893  dih1dimatlem  32028  dihlatat  32036  lcfl6  32199  lcfl8  32201  lcfrvalsnN  32240  lcfrlem9  32249  mapdheq2  32428  hlhillcs  32660  hlhilhillem  32662
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