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  2236  euan  2266  cgsexg  2895  cgsex2g  2896  cgsex4g  2897  ceqsex  2898  sbciegft  3097  sbeqalb  3119  syl5sseq  3302  euotd  4346  ralxfr2d  4629  elpwunsn  4647  limsssuc  4720  relop  4913  resiexg  5076  fnbr  5425  f1o00  5588  dffv2  5672  iinpreima  5735  funressn  5787  fnex  5824  weniso  5936  f1ocnv2d  6152  ofrval  6172  eloprabi  6270  1stconst  6291  2ndconst  6292  frxp  6309  poxp  6311  riotasvdOLD  6432  smodm2  6456  smoiso  6463  tz7.44lem1  6502  oev2  6606  oesuclem  6608  oecl  6620  omordi  6648  omwordri  6654  omword2  6656  omordlim  6659  omlimcl  6660  omeulem2  6665  oeordi  6669  oewordri  6674  oelim2  6677  oeoa  6679  oeoe  6681  nnawordi  6703  nnaordex  6720  erth  6788  iiner  6815  pw2f1olem  7051  pw2f1o  7052  onomeneq  7135  onfin2  7137  unxpdomlem2  7153  isinf  7161  findcard2  7185  fipreima  7248  fipwss  7269  cantnfp1lem3  7469  carden2b  7687  carddomi2  7690  infxpenlem  7728  acni2  7760  numacn  7763  alephfp  7822  pwsdompw  7917  ackbij2lem3  7954  cfeq0  7969  cfsuc  7970  cfsmolem  7983  domfin4  8024  axdc3lem2  8164  axdc3lem4  8166  alephreg  8291  fpwwe2  8352  winainflem  8402  r1limwun  8445  inar1  8484  grudomon  8526  nlt1pi  8617  indpi  8618  nqereu  8640  ltbtwnnq  8689  prlem934  8744  prlem936  8758  addgt0sr  8813  leltne  8998  ne0gt0  9012  mullt0  9380  msqgt0  9381  mulne0  9497  divne0  9523  div2neg  9570  ltmul12a  9699  recgt1i  9740  nn2ge  9858  peano5uzi  10189  eluzp1m1  10340  eluzaddi  10343  eluzsubi  10344  uz2m1nn  10381  rpnnen1lem5  10435  rphalflt  10469  xrleltne  10568  max0sub  10612  xmulpnf1n  10687  xmulge0  10693  xadddi  10704  supxr  10720  supxr2  10721  ixxdisj  10760  ixxun  10761  ixxub  10766  ixxlb  10767  icodisj  10850  difreicc  10856  iccf1o  10867  fzsuc2  10931  flge0nn0  11037  flge1nn  11038  seqf1olem2  11175  expubnd  11252  sqlecan  11299  bernneq  11317  bernneq2  11318  expnbnd  11320  discr1  11327  facwordi  11392  faclbnd4lem4  11399  bcpasc  11423  iswrdi  11507  ccatass  11526  revccat  11574  revrev  11575  revco  11579  sqr0lem  11816  sqrlem2  11819  sqrlem7  11824  max0add  11885  recval  11896  nnabscl  11899  absmax  11903  sqreulem  11933  climi0  12076  lo1bdd2  12088  rlimresb  12129  lo1eq  12132  rlimeq  12133  isercolllem3  12230  climsup  12233  fsumsplit  12303  fsumcom2  12328  explecnv  12414  eftlub  12480  sin02gt0  12563  rpnnen2lem10  12593  odd2np1  12678  oexpneg  12681  bitsf1  12728  sadcaddlem  12739  bitsuz  12756  rplpwr  12826  rppwr  12827  nn0seqcvgd  12831  qredeq  12876  qgt0numnn  12913  phibndlem  12929  coprimeprodsq2  12954  pythagtrip  12978  fldivp1  13036  unbenlem  13046  4sqlem9  13084  4sqlem15  13097  4sqlem16  13098  vdwlem6  13124  vdwlem10  13128  vdwlem11  13129  vdwlem13  13131  vdw  13132  mreuni  13595  cidpropd  13706  subsubc  13820  ffthiso  13896  fuciso  13942  setcmon  14012  setcepi  14013  catciso  14032  hofcl  14126  hofpropd  14134  yonedalem4c  14144  yonedainv  14148  ipoval  14350  imasmnd  14503  pwsco1mhm  14539  imasgrp  14704  subginv  14721  subgmulg  14728  eqger  14760  subgga  14847  orbstafun  14858  orbsta  14860  symggrp  14873  dfod2  14970  gexval  14982  gex1  14995  sylow2blem1  15024  sylow3lem1  15031  pj1eu  15098  efgredlema  15142  frgp0  15162  frgpmhm  15167  odadd1  15233  0cyg  15272  gsumzres  15287  gsumzsplit  15299  dprd2dlem1  15369  dprd2da  15370  dmdprdsplit2  15374  dprdsplit  15376  pgpfaclem3  15411  ablfac2  15417  imasrng  15495  subrg1  15648  abvneg  15692  lmhmf1o  15896  lmhmima  15897  reslmhm2b  15904  lsmspsn  15930  lspdisj  15971  lidlmcl  16062  fidomndrnglem  16140  mplsubglem  16272  mplmonmul  16301  mplbas2  16305  subrgascl  16332  subrgasclcl  16333  absabv  16529  elcls  16910  clsndisj  16912  isclo2  16925  neiuni  16959  neissex  16964  tgrest  16990  tgcnp  17083  lmfpm  17123  lmcl  17125  lmss  17126  lmff  17129  ist1-2  17175  cnt1  17178  cmpsublem  17226  clscon  17256  kgeni  17332  kgenidm  17342  txcnpi  17402  ptpjopn  17406  ptclsg  17409  txcmplem1  17435  qtoptop2  17490  qtoptopon  17495  r0sep  17539  ptunhmeo  17599  t0kq  17609  fsubbas  17658  neifil  17671  uffixsn  17716  ufildr  17722  rnelfm  17744  isfcls2  17804  uffclsflim  17822  alexsublem  17834  tmdcn2  17868  symgtgp  17880  tsmssplit  17930  xmeter  18075  prdsbl  18133  neibl  18143  methaus  18162  prdsxmslem2  18171  tngngp2  18264  tngngp  18266  tgqioo  18402  xrsxmet  18411  icccmplem1  18424  icccmplem2  18425  cnmpt2pc  18524  iihalf2  18529  icoopnst  18535  iocopnst  18536  xrhmeo  18542  lebnumlem1  18557  lebnumlem3  18559  pi1blem  18635  pi1grplem  18645  pi1xfrf  18649  pi1xfr  18651  pi1xfrcnvlem  18652  pi1cof  18655  pi1coghm  18657  cmetcaulem  18812  causs  18822  metcld  18829  lmcau  18836  minveclem4  18894  ivthlem2  18910  ivthlem3  18911  ivthicc  18916  ovolshftlem1  18966  ovolicc1  18973  ovolicopnf  18981  volfiniun  19002  uniioombllem3  19038  dyaddisjlem  19048  vitalilem2  19062  itg1ge0  19139  mbfi1fseqlem3  19170  xrge0f  19184  itg2seq  19195  itg2monolem1  19203  itg2addlem  19211  itg2gt0  19213  iblcnlem  19241  itgss3  19267  itgsplit  19288  dvnff  19370  dvferm2  19432  dvlip2  19440  dveq0  19445  dvge0  19451  dvcnvre  19464  dvfsumle  19466  dvfsumabs  19468  dvfsumlem2  19472  ftc1lem2  19481  ftc1lem4  19484  ftc1lem5  19485  ftc1cn  19488  ftc2  19489  itgsubstlem  19493  evlsval2  19502  mpfind  19526  coe1mul3  19583  ply1divex  19620  dgrlem  19709  dgrlb  19716  coemulhi  19733  dgrlt  19745  dgrmul  19749  plydivlem4  19774  fta1  19786  aaliou2b  19819  taylplem2  19841  dvtaylp  19847  ulmcau  19872  tanabsge  19975  sinq12gt0  19976  argimgt0  20068  cxplea  20148  cxple2  20149  cxpsqr  20155  cxpaddlelem  20196  loglesqr  20203  ang180lem2  20213  lawcos  20219  logrec  20222  asinlem3a  20271  asinlem3  20272  asinsin  20293  atanlogaddlem  20314  atanlogadd  20315  atanlogsub  20317  atantan  20324  atanbnd  20327  atantayl2  20339  efrlim  20369  wilthlem2  20413  basellem2  20425  sqfpc  20481  ppieq0  20520  sqff1o  20526  fsumdvdscom  20531  ppiub  20549  chpeq0  20553  chtleppi  20555  fsumvma  20558  fsumvma2  20559  mersenne  20572  dchrabs2  20607  dchr1re  20608  dchrpt  20612  lgsdilem  20667  lgsdinn0  20685  lgsquad3  20706  m1lgs  20707  2sqlem6  20714  rpvmasumlem  20742  dchrisumlem3  20746  dchrisum0flblem1  20763  pntibndlem2a  20845  pntlem3  20864  padicabv  20885  vcoprnelem  21242  cnnv  21353  nmounbseqi  21463  nmounbseqiOLD  21464  nmlnogt0  21483  nmblolbii  21485  blocnilem  21490  ajmoi  21545  minvecolem4  21567  hhnv  21852  norm1  21936  hhssnv  21949  pjhtheu  22081  pjpreeq  22085  spanunsni  22266  fh1  22305  fh2  22306  cm2j  22307  chscllem4  22327  pjid  22382  adjmo  22520  eleigveccl  22647  eigvalcl  22649  eigvec1  22650  eighmre  22651  eighmorth  22652  nmop0h  22679  nmbdoplbi  22712  nmcoplbi  22716  nmophmi  22719  lncnopbd  22725  nmbdfnlbi  22737  nmcfnlbi  22740  cnlnadjeui  22765  branmfn  22793  rnbra  22795  nmopleid  22827  strlem5  22943  hstrlem5  22951  dmdbr3  22993  dmdbr4  22994  mdsl3  23004  hatomistici  23050  cvexchlem  23056  chirredlem1  23078  chirredlem2  23079  chirredi  23082  atcvat3i  23084  atcvat4i  23085  atabsi  23089  mdsymlem1  23091  mdsymlem3  23093  mdsymlem5  23095  dmdbr5ati  23110  cdj1i  23121  elpreq  23195  f1o3d  23242  xrofsup  23324  iccgelb  23335  eliccelico  23339  elicoelioo  23340  numdenneg  23364  xrge0addgt0  23406  xrge0adddir  23407  xrge0npcan  23408  kerunit  23427  kerf1hrm  23428  neiptopreu  23446  unitdivcld  23455  fmcncfil  23473  cnextfun  23501  cnextfvval  23502  cnextf  23503  cnextcn  23504  ustuni  23530  trust  23533  utoptop  23538  restutop  23541  restutopopn  23542  ustuqtop1  23545  ustuqtop2  23546  ustuqtop3  23547  ustuqtop4  23548  metustto  23597  metustexhalf  23600  metust  23602  cfilucfil  23603  metutop  23611  cmetcusp  23614  zrhunitpreima  23635  elzdif0  23637  qqhval2lem  23638  qqhf  23643  indf1ofs  23689  esumfsup  23726  baselsiga  23764  sigasspw  23765  issgon  23772  meascnbl  23837  voliune  23849  volfiniune  23850  probun  23926  subfacp1lem5  24119  subfacp1lem6  24120  erdszelem9  24134  ptpcon  24168  rescon  24181  cvmlift3lem7  24260  eupap1  24304  fprodser  24576  fprodsplit  24590  sspred  24732  trpredrec  24799  axcontlem2  25152  axcontlem12  25162  btwnintr  25201  btwnouttr  25206  cgrxfr  25237  btwnconn1lem12  25280  colinbtwnle  25300  lineelsb2  25330  onintopsscon  25438  itg2gt0cn  25495  ftc1cnnclem  25513  ftc1cnnc  25514  areacirclem6  25522  areacirc  25523  nn0prpwlem  25562  locfindis  25629  neibastop3  25635  fdc  25779  incsequz  25782  blbnd  25834  prdstotbnd  25841  cnpwstotbnd  25844  ismtyres  25855  rngohomf  25920  rngohom1  25922  rngohomadd  25923  rngohommul  25924  idlss  25964  idl0cl  25966  idladdcl  25967  idllmulcl  25968  idlrmulcl  25969  maxidlnr  25990  maxidlmax  25991  smprngopr  26000  pridlc  26019  ceqsex3OLD  26049  mzpindd  26147  lzunuz  26170  2rexfrabdioph  26200  irrapxlem3  26232  pellexlem2  26238  pellexlem5  26241  pell1234qrreccl  26262  pell14qrdich  26277  pell1qrge1  26278  elpell1qr2  26280  reglogltb  26299  reglogleb  26300  rmxycomplete  26325  2nn0ind  26353  congabseq  26384  acongrep  26390  acongeq  26393  dvdsleabs2  26400  jm2.22  26411  jm2.26lem3  26417  pw2f1ocnv  26453  limsuc2  26460  fnwe2lem3  26472  aomclem6  26479  kercvrlsm  26504  pwssplit0  26510  pwssplit1  26511  pwssplit4  26514  frlmbas  26546  elfilspd  26578  f1lindf  26615  lpirlnr  26644  hashgcdeq  26840  dvconstbi  26874  mulltgt0  27016  refsumcn  27024  cncmpmax  27026  climinf  27055  climreeq  27062  stoweidlem27  27099  stoweidlem29  27101  stoweidlem31  27103  stoweidlem34  27106  stoweidlem48  27120  stoweidlem59  27131  sigarcol  27177  reuan  27281  ndmaovg  27372  elfznelfzo  27458  elprchashprn2  27464  s2f1o  27494  s4f1o  27496  usgra1  27540  usgraedg4  27552  nbgraop  27582  nbgracnvfv  27596  nbcusgra  27618  wlkdvspthlem  27726  fargshiftf1  27743  fargshiftfo  27744  eupatrl  27746  frgrancvvdeqlemA  27853  frgrancvvdeqlemB  27854  frgrancvvdeqlemC  27855  frgrawopreglem4  27863  bi2imp  27975  biimpa21  28063  a9e2ndeqALT  28453  bnj563  28517  bnj1001  28735  lshpnel2N  29227  islsati  29236  lkr0f  29336  lfl1dim  29363  lfl1dim2N  29364  omlfh1N  29500  leat  29535  atlatmstc  29561  cvlatexch3  29580  lnnat  29668  cvrat3  29683  cvrat4  29684  3dim3  29710  dalem4  29906  dalem39  29952  paddasslem12  30072  psubcliN  30179  pmapojoinN  30209  lhpm0atN  30270  lhprelat3N  30281  trlnid  30420  trlval3  30428  cdleme22b  30582  trljco  30981  diaglbN  31297  dibvalrel  31405  dicvalrelN  31427  diclspsn  31436  dih1dimatlem  31571  dihlatat  31579  lcfl6  31742  lcfl8  31744  lcfrvalsnN  31783  lcfrlem9  31792  mapdheq2  31971  hlhillcs  32203  hlhilhillem  32205
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