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  1969  euor  2281  euan  2311  cgsexg  2947  cgsex2g  2948  cgsex4g  2949  ceqsex  2950  sbciegft  3151  sbeqalb  3173  syl5sseq  3356  euotd  4417  ralxfr2d  4698  elpwunsn  4716  limsssuc  4789  relop  4982  resiexg  5147  fnbr  5506  f1o00  5669  dffv2  5755  iinpreima  5819  funressn  5878  fnex  5920  weniso  6034  f1ocnv2d  6254  ofrval  6274  eloprabi  6372  1stconst  6394  2ndconst  6395  frxp  6415  poxp  6417  riotasvdOLD  6552  smodm2  6576  smoiso  6583  tz7.44lem1  6622  oev2  6726  oesuclem  6728  oecl  6740  omordi  6768  omwordri  6774  omword2  6776  omordlim  6779  omlimcl  6780  omeulem2  6785  oeordi  6789  oewordri  6794  oelim2  6797  oeoa  6799  oeoe  6801  nnawordi  6823  nnaordex  6840  erth  6908  iiner  6935  pw2f1olem  7171  pw2f1o  7172  onomeneq  7255  onfin2  7257  unxpdomlem2  7273  isinf  7281  findcard2  7307  fipreima  7370  fipwss  7392  cantnfp1lem3  7592  carden2b  7810  carddomi2  7813  infxpenlem  7851  acni2  7883  numacn  7886  alephfp  7945  pwsdompw  8040  ackbij2lem3  8077  cfeq0  8092  cfsuc  8093  cfsmolem  8106  domfin4  8147  axdc3lem2  8287  axdc3lem4  8289  alephreg  8413  fpwwe2  8474  winainflem  8524  r1limwun  8567  inar1  8606  grudomon  8648  nlt1pi  8739  indpi  8740  nqereu  8762  ltbtwnnq  8811  prlem934  8866  prlem936  8880  addgt0sr  8935  leltne  9120  ne0gt0  9134  mullt0  9503  msqgt0  9504  mulne0  9620  divne0  9646  div2neg  9693  ltmul12a  9822  recgt1i  9863  nn2ge  9981  peano5uzi  10314  eluzp1m1  10465  eluzaddi  10468  eluzsubi  10469  uz2m1nn  10506  rpnnen1lem5  10560  rphalflt  10594  xrleltne  10694  max0sub  10738  xmulpnf1n  10813  xmulge0  10819  xadddi  10830  supxr  10847  supxr2  10848  ixxdisj  10887  ixxun  10888  ixxub  10893  ixxlb  10894  icodisj  10978  difreicc  10984  iccf1o  10995  fzsuc2  11060  elfznelfzo  11147  flge0nn0  11180  flge1nn  11181  seqf1olem2  11318  expubnd  11395  sqlecan  11442  bernneq  11460  bernneq2  11461  expnbnd  11463  discr1  11470  facwordi  11535  faclbnd4lem4  11542  bcpasc  11567  elprchashprn2  11622  iswrdi  11686  ccatass  11705  revccat  11753  revrev  11754  revco  11758  s2f1o  11818  s4f1o  11820  sqr0lem  12001  sqrlem2  12004  sqrlem7  12009  max0add  12070  recval  12081  nnabscl  12084  absmax  12088  sqreulem  12118  climi0  12261  lo1bdd2  12273  rlimresb  12314  lo1eq  12317  rlimeq  12318  isercolllem3  12415  climsup  12418  fsumsplit  12488  fsumcom2  12513  explecnv  12599  eftlub  12665  sin02gt0  12748  rpnnen2lem10  12778  odd2np1  12863  oexpneg  12866  bitsf1  12913  sadcaddlem  12924  bitsuz  12941  rplpwr  13011  rppwr  13012  nn0seqcvgd  13016  qredeq  13061  qgt0numnn  13098  phibndlem  13114  coprimeprodsq2  13139  pythagtrip  13163  fldivp1  13221  unbenlem  13231  4sqlem9  13269  4sqlem15  13282  4sqlem16  13283  vdwlem6  13309  vdwlem10  13313  vdwlem11  13314  vdwlem13  13316  vdw  13317  mreuni  13780  cidpropd  13891  subsubc  14005  ffthiso  14081  fuciso  14127  setcmon  14197  setcepi  14198  catciso  14217  hofcl  14311  hofpropd  14319  yonedalem4c  14329  yonedainv  14333  imasmnd  14688  pwsco1mhm  14724  imasgrp  14889  subginv  14906  subgmulg  14913  eqger  14945  subgga  15032  orbstafun  15043  orbsta  15045  symggrp  15058  dfod2  15155  gexval  15167  gex1  15180  sylow2blem1  15209  sylow3lem1  15216  pj1eu  15283  efgredlema  15327  frgp0  15347  frgpmhm  15352  odadd1  15418  0cyg  15457  gsumzres  15472  gsumzsplit  15484  dprd2dlem1  15554  dprd2da  15555  dmdprdsplit2  15559  dprdsplit  15561  pgpfaclem3  15596  ablfac2  15602  imasrng  15680  subrg1  15833  abvneg  15877  lmhmf1o  16077  lmhmima  16078  reslmhm2b  16085  lsmspsn  16111  lspdisj  16152  lidlmcl  16243  fidomndrnglem  16321  mplsubglem  16453  mplmonmul  16482  mplbas2  16486  subrgascl  16513  subrgasclcl  16514  absabv  16711  elcls  17092  clsndisj  17094  isclo2  17107  neiuni  17141  neissex  17146  neiptopreu  17152  tgrest  17177  neitr  17198  tgcnp  17271  lmfpm  17313  lmcl  17315  lmss  17316  lmff  17319  ist1-2  17365  cnt1  17368  cmpsublem  17416  clscon  17446  kgeni  17522  kgenidm  17532  txcnpi  17593  ptpjopn  17597  ptclsg  17600  txcmplem1  17626  qtoptop2  17684  qtoptopon  17689  r0sep  17733  ptunhmeo  17793  t0kq  17803  fsubbas  17852  neifil  17865  uffixsn  17910  ufildr  17916  rnelfm  17938  isfcls2  17998  uffclsflim  18016  alexsublem  18028  cnextfun  18048  cnextfvval  18049  cnextf  18050  cnextcn  18051  tmdcn2  18072  symgtgp  18084  tsmssplit  18134  ustuni  18209  trust  18212  utoptop  18217  restutop  18220  restutopopn  18221  ustuqtop1  18224  ustuqtop2  18225  ustuqtop3  18226  ustuqtop4  18227  utop2nei  18233  utop3cls  18234  isucn2  18262  ucncn  18268  trcfilu  18277  cfiluweak  18278  psmetdmdm  18289  xblss2ps  18384  xmeter  18416  prdsbl  18474  neibl  18484  methaus  18503  prdsxmslem2  18512  metusttoOLD  18540  metustto  18541  metustexhalfOLD  18546  metustexhalf  18547  metustOLD  18550  metust  18551  cfilucfilOLD  18552  cfilucfil  18553  metutopOLD  18565  psmetutop  18566  metucnOLD  18571  metucn  18572  tngngp2  18646  tngngp  18648  tgqioo  18784  xrsxmet  18793  icccmplem1  18806  icccmplem2  18807  cnmpt2pc  18906  iihalf2  18911  icoopnst  18917  iocopnst  18918  xrhmeo  18924  lebnumlem1  18939  lebnumlem3  18941  pi1blem  19017  pi1grplem  19027  pi1xfrf  19031  pi1xfr  19033  pi1xfrcnvlem  19034  pi1cof  19037  pi1coghm  19039  cmetcaulem  19194  causs  19204  metcld  19211  lmcau  19218  cmetcusp  19261  minveclem4  19286  ivthlem2  19302  ivthlem3  19303  ivthicc  19308  ovolshftlem1  19358  ovolicc1  19365  ovolicopnf  19373  volfiniun  19394  uniioombllem3  19430  dyaddisjlem  19440  vitalilem2  19454  itg1ge0  19531  mbfi1fseqlem3  19562  xrge0f  19576  itg2seq  19587  itg2monolem1  19595  itg2addlem  19603  itg2gt0  19605  iblcnlem  19633  itgss3  19659  itgsplit  19680  dvnff  19762  dvferm2  19824  dvlip2  19832  dveq0  19837  dvge0  19843  dvcnvre  19856  dvfsumle  19858  dvfsumabs  19860  dvfsumlem2  19864  ftc1lem2  19873  ftc1lem4  19876  ftc1lem5  19877  ftc1cn  19880  ftc2  19881  itgsubstlem  19885  evlsval2  19894  mpfind  19918  coe1mul3  19975  ply1divex  20012  dgrlem  20101  dgrlb  20108  coemulhi  20125  dgrlt  20137  dgrmul  20141  plydivlem4  20166  fta1  20178  aaliou2b  20211  taylplem2  20233  dvtaylp  20239  ulmcau  20264  tanabsge  20367  sinq12gt0  20368  argimgt0  20460  cxplea  20540  cxple2  20541  cxpsqr  20547  cxpaddlelem  20588  loglesqr  20595  ang180lem2  20605  lawcos  20611  logrec  20614  asinlem3a  20663  asinlem3  20664  asinsin  20685  atanlogaddlem  20706  atanlogadd  20707  atanlogsub  20709  atantan  20716  atanbnd  20719  atantayl2  20731  efrlim  20761  wilthlem2  20805  basellem2  20817  sqfpc  20873  ppieq0  20912  sqff1o  20918  fsumdvdscom  20923  ppiub  20941  chpeq0  20945  chtleppi  20947  fsumvma  20950  fsumvma2  20951  mersenne  20964  dchrabs2  20999  dchr1re  21000  dchrpt  21004  lgsdilem  21059  lgsdinn0  21077  lgsquad3  21098  m1lgs  21099  2sqlem6  21106  rpvmasumlem  21134  dchrisumlem3  21138  dchrisum0flblem1  21155  pntibndlem2a  21237  pntlem3  21256  padicabv  21277  usgra1  21346  usgraedg4  21359  nbgraop  21389  nbgracnvfv  21403  nbcusgra  21425  wlkdvspthlem  21560  fargshiftf1  21577  fargshiftfo  21578  eupatrl  21643  eupap1  21651  vcoprnelem  22010  cnnv  22121  nmounbseqi  22231  nmounbseqiOLD  22232  nmlnogt0  22251  nmblolbii  22253  blocnilem  22258  ajmoi  22313  minvecolem4  22335  hhnv  22620  norm1  22704  hhssnv  22717  pjhtheu  22849  pjpreeq  22853  spanunsni  23034  fh1  23073  fh2  23074  cm2j  23075  chscllem4  23095  pjid  23150  adjmo  23288  eleigveccl  23415  eigvalcl  23417  eigvec1  23418  eighmre  23419  eighmorth  23420  nmop0h  23447  nmbdoplbi  23480  nmcoplbi  23484  nmophmi  23487  lncnopbd  23493  nmbdfnlbi  23505  nmcfnlbi  23508  cnlnadjeui  23533  branmfn  23561  rnbra  23563  nmopleid  23595  strlem5  23711  hstrlem5  23719  dmdbr3  23761  dmdbr4  23762  mdsl3  23772  hatomistici  23818  cvexchlem  23824  chirredlem1  23846  chirredlem2  23847  chirredi  23850  atcvat3i  23852  atcvat4i  23853  atabsi  23857  mdsymlem1  23859  mdsymlem3  23861  mdsymlem5  23863  dmdbr5ati  23878  cdj1i  23889  elabreximd  23944  elpreq  23952  f1o3d  23994  disjdsct  24043  xrofsup  24079  iccgelb  24089  eliccelico  24093  elicoelioo  24094  numdenneg  24113  xrge0addgt0  24167  xrge0adddir  24168  xrge0npcan  24169  kerf1hrm  24215  metideq  24241  unitdivcld  24252  cnre2csqlem  24261  fmcncfil  24270  lmxrge0  24290  zrhunitpreima  24315  elzdif0  24317  qqhval2lem  24318  qqhf  24323  indf1ofs  24376  esumfsup  24413  esumpcvgval  24421  sigasspw  24452  issgon  24459  meascnbl  24526  voliune  24538  volfiniune  24539  ballotlemfrcn0  24740  ballotlemirc  24742  subfacp1lem5  24823  subfacp1lem6  24824  erdszelem9  24838  ptpcon  24873  rescon  24886  cvmlift3lem7  24965  fprodser  25228  fprodsplit  25242  fprodcom2  25261  sspred  25388  trpredrec  25455  axcontlem2  25808  axcontlem12  25818  btwnintr  25857  btwnouttr  25862  cgrxfr  25893  btwnconn1lem12  25936  colinbtwnle  25956  lineelsb2  25986  onintopsscon  26094  mblfinlem  26143  itg2gt0cn  26159  itgaddnclem2  26163  ftc1cnnclem  26177  ftc1cnnc  26178  areacirclem6  26186  areacirc  26187  nn0prpwlem  26215  locfindis  26275  neibastop3  26281  fdc  26339  incsequz  26342  blbnd  26386  prdstotbnd  26393  cnpwstotbnd  26396  ismtyres  26407  rngohomf  26472  rngohom1  26474  rngohomadd  26475  rngohommul  26476  idlss  26516  idl0cl  26518  idladdcl  26519  idllmulcl  26520  idlrmulcl  26521  maxidlnr  26542  maxidlmax  26543  smprngopr  26552  pridlc  26571  ceqsex3OLD  26599  mzpindd  26693  lzunuz  26716  2rexfrabdioph  26746  irrapxlem3  26777  pellexlem2  26783  pellexlem5  26786  pell1234qrreccl  26807  pell14qrdich  26822  pell1qrge1  26823  elpell1qr2  26825  reglogltb  26844  reglogleb  26845  rmxycomplete  26870  2nn0ind  26898  congabseq  26929  acongrep  26935  acongeq  26938  dvdsleabs2  26945  jm2.22  26956  jm2.26lem3  26962  pw2f1ocnv  26998  limsuc2  27005  fnwe2lem3  27017  aomclem6  27024  kercvrlsm  27049  pwssplit0  27055  pwssplit1  27056  pwssplit4  27059  frlmbas  27091  elfilspd  27123  f1lindf  27160  lpirlnr  27189  hashgcdeq  27385  dvconstbi  27419  mulltgt0  27560  refsumcn  27568  cncmpmax  27570  climinf  27599  climreeq  27606  stoweidlem27  27643  stoweidlem29  27645  stoweidlem31  27647  stoweidlem34  27650  stoweidlem48  27664  stoweidlem59  27675  sigarcol  27721  reuan  27825  ndmaovg  27915  iswrd0i  27999  swrd0swrd  28009  swrdswrdlem  28010  swrdswrd  28011  swrdswrd0  28013  swrdccat3a0  28015  swrdccatin2  28018  swrdccat3b  28031  usgra2pthlem1  28040  usg2spthonot  28085  frgrancvvdeqlemA  28140  frgrancvvdeqlemB  28141  frgrancvvdeqlemC  28142  frgrawopreglem4  28150  bi2imp  28279  a9e2ndeqALT  28753  bnj563  28817  bnj1001  29035  lshpnel2N  29468  islsati  29477  lkr0f  29577  lfl1dim  29604  lfl1dim2N  29605  omlfh1N  29741  leat  29776  atlatmstc  29802  cvlatexch3  29821  lnnat  29909  cvrat3  29924  cvrat4  29925  3dim3  29951  dalem4  30147  dalem39  30193  paddasslem12  30313  psubcliN  30420  pmapojoinN  30450  lhpm0atN  30511  lhprelat3N  30522  trlnid  30661  trlval3  30669  cdleme22b  30823  trljco  31222  diaglbN  31538  dibvalrel  31646  dicvalrelN  31668  diclspsn  31677  dih1dimatlem  31812  dihlatat  31820  lcfl6  31983  lcfl8  31985  lcfrvalsnN  32024  lcfrlem9  32033  mapdheq2  32212  hlhillcs  32444  hlhilhillem  32446
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