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  euor  2308  euan  2338  cgsexg  2987  cgsex2g  2988  cgsex4g  2989  ceqsex  2990  sbciegft  3191  sbeqalb  3213  syl5sseq  3396  euotd  4457  ralxfr2d  4739  elpwunsn  4757  limsssuc  4830  relop  5023  resiexg  5188  fnbr  5547  f1o00  5710  dffv2  5796  iinpreima  5860  funressn  5919  fnex  5961  weniso  6075  f1ocnv2d  6295  ofrval  6315  eloprabi  6413  1stconst  6435  2ndconst  6436  frxp  6456  poxp  6458  riotasvdOLD  6593  smodm2  6617  smoiso  6624  tz7.44lem1  6663  oev2  6767  oesuclem  6769  oecl  6781  omordi  6809  omwordri  6815  omword2  6817  omordlim  6820  omlimcl  6821  omeulem2  6826  oeordi  6830  oewordri  6835  oelim2  6838  oeoa  6840  oeoe  6842  nnawordi  6864  nnaordex  6881  erth  6949  iiner  6976  pw2f1olem  7212  pw2f1o  7213  onomeneq  7296  onfin2  7298  unxpdomlem2  7314  isinf  7322  findcard2  7348  fipreima  7412  fipwss  7434  cantnfp1lem3  7636  carden2b  7854  carddomi2  7857  infxpenlem  7895  acni2  7927  numacn  7930  alephfp  7989  pwsdompw  8084  ackbij2lem3  8121  cfeq0  8136  cfsuc  8137  cfsmolem  8150  domfin4  8191  axdc3lem2  8331  axdc3lem4  8333  alephreg  8457  fpwwe2  8518  winainflem  8568  r1limwun  8611  inar1  8650  grudomon  8692  nlt1pi  8783  indpi  8784  nqereu  8806  ltbtwnnq  8855  prlem934  8910  prlem936  8924  addgt0sr  8979  leltne  9164  ne0gt0  9178  mullt0  9547  msqgt0  9548  mulne0  9664  divne0  9690  div2neg  9737  ltmul12a  9866  recgt1i  9907  nn2ge  10025  peano5uzi  10358  eluzp1m1  10509  eluzaddi  10512  eluzsubi  10513  uz2m1nn  10550  rpnnen1lem5  10604  rphalflt  10638  xrleltne  10738  max0sub  10782  xmulpnf1n  10857  xmulge0  10863  xadddi  10874  supxr  10891  supxr2  10892  ixxdisj  10931  ixxun  10932  ixxub  10937  ixxlb  10938  icodisj  11022  difreicc  11028  iccf1o  11039  fzsuc2  11104  elfznelfzo  11192  flge0nn0  11225  flge1nn  11226  seqf1olem2  11363  expubnd  11440  sqlecan  11487  bernneq  11505  bernneq2  11506  expnbnd  11508  discr1  11515  facwordi  11580  faclbnd4lem4  11587  bcpasc  11612  elprchashprn2  11667  iswrdi  11731  ccatass  11750  revccat  11798  revrev  11799  revco  11803  s2f1o  11863  s4f1o  11865  sqr0lem  12046  sqrlem2  12049  sqrlem7  12054  max0add  12115  recval  12126  nnabscl  12129  absmax  12133  sqreulem  12163  climi0  12306  lo1bdd2  12318  rlimresb  12359  lo1eq  12362  rlimeq  12363  isercolllem3  12460  climsup  12463  fsumsplit  12533  fsumcom2  12558  explecnv  12644  eftlub  12710  sin02gt0  12793  rpnnen2lem10  12823  odd2np1  12908  oexpneg  12911  bitsf1  12958  sadcaddlem  12969  bitsuz  12986  rplpwr  13056  rppwr  13057  nn0seqcvgd  13061  qredeq  13106  qgt0numnn  13143  phibndlem  13159  coprimeprodsq2  13184  pythagtrip  13208  fldivp1  13266  unbenlem  13276  4sqlem9  13314  4sqlem15  13327  4sqlem16  13328  vdwlem6  13354  vdwlem10  13358  vdwlem11  13359  vdwlem13  13361  vdw  13362  mreuni  13825  cidpropd  13936  subsubc  14050  ffthiso  14126  fuciso  14172  setcmon  14242  setcepi  14243  catciso  14262  hofcl  14356  hofpropd  14364  yonedalem4c  14374  yonedainv  14378  imasmnd  14733  pwsco1mhm  14769  imasgrp  14934  subginv  14951  subgmulg  14958  eqger  14990  subgga  15077  orbstafun  15088  orbsta  15090  symggrp  15103  dfod2  15200  gexval  15212  gex1  15225  sylow2blem1  15254  sylow3lem1  15261  pj1eu  15328  efgredlema  15372  frgp0  15392  frgpmhm  15397  odadd1  15463  0cyg  15502  gsumzres  15517  gsumzsplit  15529  dprd2dlem1  15599  dprd2da  15600  dmdprdsplit2  15604  dprdsplit  15606  pgpfaclem3  15641  ablfac2  15647  imasrng  15725  subrg1  15878  abvneg  15922  lmhmf1o  16122  lmhmima  16123  reslmhm2b  16130  lsmspsn  16156  lspdisj  16197  lidlmcl  16288  fidomndrnglem  16366  mplsubglem  16498  mplmonmul  16527  mplbas2  16531  subrgascl  16558  subrgasclcl  16559  absabv  16756  elcls  17137  clsndisj  17139  isclo2  17152  neiuni  17186  neissex  17191  neiptopreu  17197  tgrest  17223  neitr  17244  tgcnp  17317  lmfpm  17359  lmcl  17361  lmss  17362  lmff  17365  ist1-2  17411  cnt1  17414  cmpsublem  17462  clscon  17493  kgeni  17569  kgenidm  17579  txcnpi  17640  ptpjopn  17644  ptclsg  17647  txcmplem1  17673  qtoptop2  17731  qtoptopon  17736  r0sep  17780  ptunhmeo  17840  t0kq  17850  fsubbas  17899  neifil  17912  uffixsn  17957  ufildr  17963  rnelfm  17985  isfcls2  18045  uffclsflim  18063  alexsublem  18075  cnextfun  18095  cnextfvval  18096  cnextf  18097  cnextcn  18098  tmdcn2  18119  symgtgp  18131  tsmssplit  18181  ustuni  18256  trust  18259  utoptop  18264  restutop  18267  restutopopn  18268  ustuqtop1  18271  ustuqtop2  18272  ustuqtop3  18273  ustuqtop4  18274  utop2nei  18280  utop3cls  18281  isucn2  18309  ucncn  18315  trcfilu  18324  cfiluweak  18325  psmetdmdm  18336  xblss2ps  18431  xmeter  18463  prdsbl  18521  neibl  18531  methaus  18550  prdsxmslem2  18559  metusttoOLD  18587  metustto  18588  metustexhalfOLD  18593  metustexhalf  18594  metustOLD  18597  metust  18598  cfilucfilOLD  18599  cfilucfil  18600  metutopOLD  18612  psmetutop  18613  metucnOLD  18618  metucn  18619  tngngp2  18693  tngngp  18695  tgqioo  18831  xrsxmet  18840  icccmplem1  18853  icccmplem2  18854  cnmpt2pc  18953  iihalf2  18958  icoopnst  18964  iocopnst  18965  xrhmeo  18971  lebnumlem1  18986  lebnumlem3  18988  pi1blem  19064  pi1grplem  19074  pi1xfrf  19078  pi1xfr  19080  pi1xfrcnvlem  19081  pi1cof  19084  pi1coghm  19086  cmetcaulem  19241  causs  19251  metcld  19258  lmcau  19265  cmetcusp  19308  minveclem4  19333  ivthlem2  19349  ivthlem3  19350  ivthicc  19355  ovolshftlem1  19405  ovolicc1  19412  ovolicopnf  19420  volfiniun  19441  uniioombllem3  19477  dyaddisjlem  19487  vitalilem2  19501  itg1ge0  19578  mbfi1fseqlem3  19609  xrge0f  19623  itg2seq  19634  itg2monolem1  19642  itg2addlem  19650  itg2gt0  19652  iblcnlem  19680  itgss3  19706  itgsplit  19727  dvnff  19809  dvferm2  19871  dvlip2  19879  dveq0  19884  dvge0  19890  dvcnvre  19903  dvfsumle  19905  dvfsumabs  19907  dvfsumlem2  19911  ftc1lem2  19920  ftc1lem4  19923  ftc1lem5  19924  ftc1cn  19927  ftc2  19928  itgsubstlem  19932  evlsval2  19941  mpfind  19965  coe1mul3  20022  ply1divex  20059  dgrlem  20148  dgrlb  20155  coemulhi  20172  dgrlt  20184  dgrmul  20188  plydivlem4  20213  fta1  20225  aaliou2b  20258  taylplem2  20280  dvtaylp  20286  ulmcau  20311  tanabsge  20414  sinq12gt0  20415  argimgt0  20507  cxplea  20587  cxple2  20588  cxpsqr  20594  cxpaddlelem  20635  loglesqr  20642  ang180lem2  20652  lawcos  20658  logrec  20661  asinlem3a  20710  asinlem3  20711  asinsin  20732  atanlogaddlem  20753  atanlogadd  20754  atanlogsub  20756  atantan  20763  atanbnd  20766  atantayl2  20778  efrlim  20808  wilthlem2  20852  basellem2  20864  sqfpc  20920  ppieq0  20959  sqff1o  20965  fsumdvdscom  20970  ppiub  20988  chpeq0  20992  chtleppi  20994  fsumvma  20997  fsumvma2  20998  mersenne  21011  dchrabs2  21046  dchr1re  21047  dchrpt  21051  lgsdilem  21106  lgsdinn0  21124  lgsquad3  21145  m1lgs  21146  2sqlem6  21153  rpvmasumlem  21181  dchrisumlem3  21185  dchrisum0flblem1  21202  pntibndlem2a  21284  pntlem3  21303  padicabv  21324  usgra1  21393  usgraedg4  21406  nbgraop  21436  nbgracnvfv  21450  nbcusgra  21472  wlkdvspthlem  21607  fargshiftf1  21624  fargshiftfo  21625  eupatrl  21690  eupap1  21698  vcoprnelem  22057  cnnv  22168  nmounbseqi  22278  nmounbseqiOLD  22279  nmlnogt0  22298  nmblolbii  22300  blocnilem  22305  ajmoi  22360  minvecolem4  22382  hhnv  22667  norm1  22751  hhssnv  22764  pjhtheu  22896  pjpreeq  22900  spanunsni  23081  fh1  23120  fh2  23121  cm2j  23122  chscllem4  23142  pjid  23197  adjmo  23335  eleigveccl  23462  eigvalcl  23464  eigvec1  23465  eighmre  23466  eighmorth  23467  nmop0h  23494  nmbdoplbi  23527  nmcoplbi  23531  nmophmi  23534  lncnopbd  23540  nmbdfnlbi  23552  nmcfnlbi  23555  cnlnadjeui  23580  branmfn  23608  rnbra  23610  nmopleid  23642  strlem5  23758  hstrlem5  23766  dmdbr3  23808  dmdbr4  23809  mdsl3  23819  hatomistici  23865  cvexchlem  23871  chirredlem1  23893  chirredlem2  23894  chirredi  23897  atcvat3i  23899  atcvat4i  23900  atabsi  23904  mdsymlem1  23906  mdsymlem3  23908  mdsymlem5  23910  dmdbr5ati  23925  cdj1i  23936  elabreximd  23991  elpreq  23999  f1o3d  24041  disjdsct  24090  xrofsup  24126  iccgelb  24136  eliccelico  24140  elicoelioo  24141  numdenneg  24160  xrge0addgt0  24214  xrge0adddir  24215  xrge0npcan  24216  kerf1hrm  24262  metideq  24288  unitdivcld  24299  cnre2csqlem  24308  fmcncfil  24317  lmxrge0  24337  zrhunitpreima  24362  elzdif0  24364  qqhval2lem  24365  qqhf  24370  indf1ofs  24423  esumfsup  24460  esumpcvgval  24468  sigasspw  24499  issgon  24506  meascnbl  24573  voliune  24585  volfiniune  24586  ballotlemfrcn0  24787  ballotlemirc  24789  subfacp1lem5  24870  subfacp1lem6  24871  erdszelem9  24885  ptpcon  24920  rescon  24933  cvmlift3lem7  25012  fprodser  25275  fprodsplit  25289  fprodcom2  25308  sspred  25447  trpredrec  25516  axcontlem2  25904  axcontlem12  25914  btwnintr  25953  btwnouttr  25958  cgrxfr  25989  btwnconn1lem12  26032  colinbtwnle  26052  lineelsb2  26082  onintopsscon  26190  mblfinlem2  26244  itg2gt0cn  26260  itgaddnclem2  26264  ftc1cnnclem  26278  ftc1cnnc  26279  ftc1anclem2  26281  ftc1anclem5  26284  ftc1anclem7  26286  ftc1anc  26288  ftc2nc  26289  areacirclem5  26296  areacirc  26297  nn0prpwlem  26325  locfindis  26385  neibastop3  26391  fdc  26449  incsequz  26452  blbnd  26496  prdstotbnd  26503  cnpwstotbnd  26506  ismtyres  26517  rngohomf  26582  rngohom1  26584  rngohomadd  26585  rngohommul  26586  idlss  26626  idl0cl  26628  idladdcl  26629  idllmulcl  26630  idlrmulcl  26631  maxidlnr  26652  maxidlmax  26653  smprngopr  26662  pridlc  26681  ceqsex3OLD  26709  mzpindd  26803  lzunuz  26826  2rexfrabdioph  26856  irrapxlem3  26887  pellexlem2  26893  pellexlem5  26896  pell1234qrreccl  26917  pell14qrdich  26932  pell1qrge1  26933  elpell1qr2  26935  reglogltb  26954  reglogleb  26955  rmxycomplete  26980  2nn0ind  27008  congabseq  27039  acongrep  27045  acongeq  27048  dvdsleabs2  27055  jm2.22  27066  jm2.26lem3  27072  pw2f1ocnv  27108  limsuc2  27115  fnwe2lem3  27127  aomclem6  27134  kercvrlsm  27158  pwssplit0  27164  pwssplit1  27165  pwssplit4  27168  frlmbas  27200  elfilspd  27232  f1lindf  27269  lpirlnr  27298  hashgcdeq  27494  dvconstbi  27528  mulltgt0  27669  refsumcn  27677  cncmpmax  27679  climinf  27708  climreeq  27715  stoweidlem27  27752  stoweidlem29  27754  stoweidlem31  27756  stoweidlem34  27759  stoweidlem48  27773  stoweidlem59  27784  sigarcol  27830  reuan  27934  ndmaovg  28024  fzonmapblen  28134  2submod  28152  iswrd0i  28169  wrdsymb0  28170  ccatsymb  28179  swrd0swrd  28197  swrdswrdlem  28198  swrdswrd  28199  swrdswrd0  28201  swrdccatin12lem3b  28209  reumodprminv  28227  usgra2pthlem1  28310  usg2spthonot  28355  frgrancvvdeqlemA  28426  frgrancvvdeqlemB  28427  frgrancvvdeqlemC  28428  frgrawopreglem4  28436  bi2imp  28565  a9e2ndeqALT  29043  bnj563  29111  bnj1001  29329  lshpnel2N  29783  islsati  29792  lkr0f  29892  lfl1dim  29919  lfl1dim2N  29920  omlfh1N  30056  leat  30091  atlatmstc  30117  cvlatexch3  30136  lnnat  30224  cvrat3  30239  cvrat4  30240  3dim3  30266  dalem4  30462  dalem39  30508  paddasslem12  30628  psubcliN  30735  pmapojoinN  30765  lhpm0atN  30826  lhprelat3N  30837  trlnid  30976  trlval3  30984  cdleme22b  31138  trljco  31537  diaglbN  31853  dibvalrel  31961  dicvalrelN  31983  diclspsn  31992  dih1dimatlem  32127  dihlatat  32135  lcfl6  32298  lcfl8  32300  lcfrvalsnN  32339  lcfrlem9  32348  mapdheq2  32527  hlhillcs  32759  hlhilhillem  32761
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