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

Theorem biimpd 207
Description: Deduce an implication from a logical equivalence. (Contributed by NM, 11-Jan-1993.)
Hypothesis
Ref Expression
biimpd.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
biimpd  |-  ( ph  ->  ( ps  ->  ch ) )

Proof of Theorem biimpd
StepHypRef Expression
1 biimpd.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
2 bi1 186 . 2  |-  ( ( ps  <->  ch )  ->  ( ps  ->  ch ) )
31, 2syl 16 1  |-  ( ph  ->  ( ps  ->  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185
This theorem is referenced by:  mpbid  210  sylibd  214  sylbid  215  mpbidi  216  syl5ib  219  syl6bi  228  ibi  241  con4bid  291  mtbird  299  mtbiri  301  imbi1d  315  pm5.21im  347  biimpa  482  exintr  1707  spfw  1811  cbvalw  1813  alcomiw  1816  19.9d  1897  19.23t  1914  spimt  2010  spv  2016  chvar  2018  cbval  2026  nfsb4t  2132  dral1-o  2235  2eu3  2376  eqrdav  2452  eqrdavOLD  2453  cleqhOLD  2570  rgen2a  2881  ralcom2  3019  ceqsalgALT  3132  vtoclf  3157  vtocl2  3159  vtocl3  3160  spcdv  3189  rspcdv  3210  rexraleqim  3222  elabgt  3240  sbcn1  3370  sbcim1  3371  sbcbi1  3372  sbeqalb  3377  sbcel21v  3385  eqrd  3507  elpwunsn  4057  rabsnifsb  4084  ssunsn2  4175  euotd  4737  sotr2  4818  onmindif  4956  relop  5142  elres  5297  restidsing  5318  elimasni  5352  sotri2  5384  relcnvtr  5510  iotaval  5545  dffv2  5921  mpteqb  5946  elfvmptrab  5953  chfnrn  5974  elpreima  5983  iinpreima  5993  exfo  6025  ffnfv  6033  f1elima  6146  f1eqcocnv  6179  fliftfun  6185  soisores  6198  isotr  6207  isomin  6208  ovmpt2dv2  6409  difsnexi  6581  onint  6603  oneqmin  6613  ordunisuc2  6652  tfindsg  6668  findsg  6700  f1oweALT  6757  ressuppss  6911  funsssuppss  6918  imacosupp  6932  smoiso  7025  seqomlem2  7108  oaordi  7187  oawordri  7191  oaordex  7199  oalimcl  7201  omwordi  7212  oewordi  7232  oelim2  7236  nnmwordi  7276  xpider  7374  iiner  7375  undifixp  7498  mptelixpg  7499  dom2lem  7548  nneneq  7693  fineqvlem  7727  pssnn  7731  dif1en  7745  findcard2s  7753  unfilem2  7777  xpfi  7783  domunfican  7785  fsuppimp  7827  dffi2  7875  wemaplem2  7964  suc11reg  8027  noinfep  8067  cantnflem1  8099  cantnflem1OLD  8122  r1fin  8182  tcrank  8293  cardlim  8344  pr2nelem  8373  fseqenlem1  8396  alephnbtwn  8443  alephord2i  8449  alephf1  8457  cardaleph  8461  alephiso  8470  dfac12lem2  8515  ackbij1lem16  8606  cflm  8621  cfcoflem  8643  sornom  8648  fin23lem27  8699  isf32lem7  8730  fin17  8765  fin1a2lem2  8772  fin1a2lem4  8774  fin1a2lem6  8776  fin1a2lem9  8779  axdc3lem2  8822  zorn2lem7  8873  uniimadom  8910  inar1  9142  grothomex  9196  addcanpi  9266  mulcanpi  9267  enqer  9288  genpcd  9373  genpnmax  9374  ltexprlem4  9406  reclem3pr  9416  reclem4pr  9417  suplem2pr  9420  axpre-ltadd  9533  axpre-sup  9535  ltletr  9665  00id  9744  mul0or  10185  prodgt02  10384  prodge02  10386  lemul1a  10392  mulgt1  10397  divgt0  10406  divge0  10407  ledivp1i  10466  ltdivp1i  10467  cju  10527  nnsub  10570  nominpos  10771  nn0n0n1ge2  10855  btwnnz  10935  uzindOLD  10953  suprfinzcl  10975  ublbneg  11167  zmax  11180  cnref1o  11216  ltsubrp  11253  ltaddrp  11254  xrltletr  11363  qbtwnre  11401  xltnegi  11418  iccsupr  11620  icoshft  11645  difreicc  11655  iccshftri  11658  iccshftli  11660  iccdili  11662  icccntri  11664  fzen  11706  elfzmlbmOLD  11789  fzofzim  11846  eluzgtdifelfzo  11859  injresinjlem  11906  injresinj  11907  flval2  11931  flval3  11932  modaddmodup  12032  fseqsupubi  12070  ssnn0fi  12076  mptnn0fsuppr  12087  sq01  12270  hashf1rn  12407  hashle00  12449  hashgt12el  12465  hashgt12el2  12466  hash2pr  12499  hash2prb  12501  hashtpg  12507  hash3tr  12513  lswlgt0cl  12578  2swrd1eqwrdeq  12670  ccatopth2  12687  reuccats1lem  12696  swrdccatin2  12703  swrdccat  12709  swrdccat3a  12710  swrdccat3blem  12711  repsdf2  12741  repswsymball  12742  repswrevw  12749  cshweqrep  12780  cshw1  12781  2cshwcshw  12784  scshwfzeqfzo  12785  cshwcsh2id  12787  swrdco  12794  swrd2lsw  12881  2swrd2eqwrdeq  12882  wwlktovfo  12887  cjre  13054  o1lo1  13442  o1of2  13517  o1rlimmul  13523  zsum  13622  modfsummods  13689  zprod  13826  reeff1  13937  dvds2lem  14080  muldvds1  14092  dvdscmulr  14096  dvdsmulcr  14097  divalglem8  14142  ndvdsadd  14150  gcdmultiple  14272  prmn2uzge3  14321  isprm6  14334  isprm5  14337  prmdvdsexpr  14341  divgcdodd  14344  phiprmpw  14390  modprm0  14414  pythagtriplem4  14427  pcz  14488  1arith  14529  cshwrepswhash1  14671  divsfval  15036  catsubcat  15327  fthmon  15415  isinitoi  15481  istermoi  15482  iszeroi  15487  setcmon  15565  setcepi  15566  funcestrcsetclem8  15615  fthestrcsetc  15618  funcsetcestrclem8  15630  fthsetcestrc  15633  pltnle  15795  pltval3  15796  lublecllem  15817  latasym  15884  odupos  15964  mrelatglb  16013  mrelatlub  16015  cnvpsb  16042  isgrpid2  16285  ghmf1  16494  orbsta  16550  resscntz  16568  gsmsymgrfixlem1  16651  gsmsymgreqlem2  16655  mndodcongi  16766  odf1  16783  lsmss1  16883  lsmss2  16885  efgredeu  16969  cntzcmnss  17048  lt6abl  17096  ablfaclem3  17333  kerf1hrm  17587  lspsneq  17963  lspsneu  17964  lsmcv  17982  lidldvgen  18098  0ringnnzr  18112  domnmuln0  18142  opprdomn  18145  ply1scln0  18527  gsummoncoe1  18541  domnchr  18744  znf1o  18763  zntoslem  18768  znfld  18772  cygznlem2a  18779  cygznlem3  18781  islindf4  19040  uvcendim  19049  matvscl  19100  scmataddcl  19185  scmatsubcl  19186  scmatfo  19199  scmatghm  19202  maducoeval2  19309  slesolinv  19349  cramerimplem2  19353  cpmatelimp  19380  cpmatelimp2  19382  cpmatacl  19384  cpmatinvcl  19385  pm2mpf1  19467  cayhamlem1  19534  cayleyhamilton1  19560  0ntr  19739  islpi  19817  lmss  19966  cmpcld  20069  cmpfi  20075  1stcelcls  20128  comppfsc  20199  ptcnplem  20288  qtophmeo  20484  fbdmn0  20501  fbasrn  20551  elfm3  20617  fmfnfmlem4  20624  fclscf  20692  cnpfcf  20708  alexsubALTlem3  20715  tsmsresOLD  20811  tsmsres  20812  blval2  21244  nmoleub  21404  nmhmcn  21769  iscau4  21884  caussi  21902  cniccbdd  22039  ovoliunnul  22084  mbfinf  22238  itg2splitlem  22321  dvcn  22490  c1lip1  22564  c1lip3  22566  dvcnvrelem1  22584  ply1divex  22703  quotcan  22871  aannenlem1  22890  taylf  22922  ulmcaulem  22955  ulmcau  22956  reeff1o  23008  logccv  23212  logreclem  23301  isosctrlem2  23350  xrlimcnp  23496  rlimcxp  23501  ftalem7  23550  vmappw  23588  fsumvma  23686  dchreq  23731  dchrptlem1  23737  dchrsum  23742  bposlem7  23763  lgsqrlem2  23815  lgsdchr  23821  lgseisenlem2  23823  lgsquad2  23833  2sqlem6  23842  tgcgrcomimp  24069  isperp2  24293  xmstrkgc  24391  brbtwn  24404  brcgr  24405  axcgrid  24421  axeuclidlem  24467  axeuclid  24468  uhgraeq12d  24509  usgrac  24553  usgraeq12d  24564  usgranloopv  24580  nbgraf1olem5  24647  iscusgra0  24659  cusgrasize2inds  24679  cusgrafilem3  24683  usgramaxsize  24689  iswlkg  24726  wlkcompim  24728  wlkcpr  24731  wlkonprop  24737  trlonprop  24746  0wlkon  24751  usgrnloop  24767  pthonprop  24781  spthonprp  24789  redwlk  24810  wlkdvspthlem  24811  usgra2wlkspthlem2  24822  fargshiftfv  24837  wwlknimp  24889  vfwlkniswwlkn  24908  usg2wlkeq  24910  wwlknred  24925  wwlknext  24926  wwlknextbi  24927  wwlkextwrd  24930  wwlkextinj  24932  wwlkextsur  24933  wwlkm1edg  24937  isclwlkg  24957  clwlkcompim  24966  0clwlk  24967  clwwlkn2  24977  clwlkisclwwlklem2a1  24981  clwlkisclwwlklem2a4  24986  clwlkisclwwlklem2a  24987  clwlkisclwwlklem1  24989  clwwlkf  24996  wwlkext2clwwlk  25005  clwwisshclwwlem1  25007  wlklenvclwlk  25041  clwlkfclwwlk  25046  el2spthonot  25072  usg2wotspth  25086  usg2spthonot  25090  usg2spthonot0  25091  rgraprop  25130  rusgraprop  25131  rusgraprop3  25145  frgranbnb  25222  frgrancvvdeqlem3  25234  frgrancvvdeqlem4  25235  frgrancvvdeqlem7  25238  frgrawopreglem2  25247  frgrawopreg  25251  frgregordn0  25272  clwwlkextfrlem1  25278  extwwlkfablem2  25280  numclwwlkun  25281  numclwwlkovf2ex  25288  numclwlk1lem2foa  25293  numclwlk1lem2f1  25296  numclwwlk8  25317  gxid  25473  opidonOLD  25522  opidon2OLD  25524  grpomndo  25546  elghomlem2OLD  25562  rngoueqz  25630  dvrunz  25633  rngoridfz  25635  hlipgt0  26028  ocin  26412  ocnel  26414  shmodsi  26505  pjmf1  26832  unopf1o  27033  staddi  27363  stadd3i  27365  mdi  27412  dmdmd  27417  dmdi  27419  dmdbr2  27420  dmdbr3  27422  dmdbr4  27423  dmdi4  27424  mdsl1i  27438  superpos  27471  cvbr4i  27484  atssma  27495  atcv1  27497  atomli  27499  chirredlem1  27507  addltmulALT  27563  bian1d  27564  ifeqeqx  27625  disjxpin  27658  suppss3  27781  fpwrelmap  27787  xrge0infss  27811  ogrpaddlt  27942  metider  28108  tpr2rico  28129  xrge0iifiso  28152  qqhcn  28206  qqhucn  28207  esumlub  28289  esumpinfval  28302  esumpinfsum  28306  ballotlemfc0  28695  ballotlemfcc  28696  erdsze2lem2  28912  trpredrec  29561  poseq  29573  soseq  29574  sltval2  29656  sltres  29664  nodenselem7  29687  nodenselem8  29688  nodense  29689  nobndup  29700  nobnddown  29701  nofulllem5  29706  dfrdg4  29828  altopthsn  29839  btwncomim  29891  btwnexch3  29898  btwnexch2  29901  endofsegid  29963  onsuct0  30134  ordcmp  30140  nndivsub  30150  wl-equsal1i  30236  wl-ax11-lem10  30274  ltflcei  30283  sin2h  30285  cos2h  30286  tan2h  30287  heicant  30289  mblfinlem1  30291  mblfinlem2  30292  mblfinlem3  30293  mblfinlem4  30294  mbfresfi  30301  cnambfre  30303  dvtanlem  30304  ftc1anc  30338  dvasin  30343  areacirclem1  30347  areacirclem4  30350  areacirc  30352  opnrebl2  30379  nn0prpwlem  30380  brabg2  30446  fzmul  30473  fdc  30478  incsequz2  30482  isbnd2  30519  divrngidl  30665  rexrabdioph  30967  fphpdo  30990  icodiamlt  30995  irrapxlem3  30999  rmxypairf1o  31086  rmxycomplete  31092  zindbi  31121  lermxnn0  31127  ltrmy  31129  rmyeq0  31130  rmyeq  31131  lermy  31132  acongsym  31153  acongneg2  31154  wepwsolem  31226  radcnvrat  31436  nzss  31463  expgrowthi  31479  ordpss  31601  fzisoeu  31739  climinf  31851  stoweidlem7  32028  stoweidlem62  32083  2reu3  32432  ralbinrald  32443  funressnfv  32452  afv0fv0  32473  afv0nbfvbi  32475  afvfv0bi  32476  fnbrafvb  32478  afvres  32496  tz6.12-afv  32497  afvco2  32500  ndmaovcl  32527  mod2eq1n2dvds  32534  evennodd  32557  oddneven  32558  oexpnegALTV  32583  oexpnegnz  32584  pfxfv  32627  pfxsuff1eqwrdeq  32635  reuccatpfxs1lem  32661  f1dmvrnfibi  32686  zm1nn  32699  subsubelfzo0  32712  usgra2pth  32726  usgpredgv  32771  usgpredgvALT  32772  usgfis  32818  usgfisALT  32822  mgmpropd  32835  clintop  32904  isassintop  32906  lidldomn1  32981  uzlidlring  32989  2zrngnmlid2  33011  rngccatidALTV  33051  ringccatidALTV  33114  srhmsubc  33138  srhmsubcALTV  33157  ztprmneprm  33190  pgrpgt2nabl  33213  lindslinindimp2lem4  33316  lincresunit3  33336  fldivexpfllog2  33440  digexp  33482  bi23impib  33641  bi23imp13  33647  bitr3  33667  rspsbc2  33695  tratrb  33697  sbcim2g  33699  truniALT  33702  3impcombi  34008  tpid3gVD  34042  orbi1rVD  34048  sbc3orgVD  34051  rspsbc2VD  34055  tratrbVD  34062  sbcim2gVD  34076  sbcbiVD  34077  truniALTVD  34079  trintALTVD  34081  trintALT  34082  csbingVD  34085  csbsngVD  34094  csbxpgVD  34095  csbresgVD  34096  csbrngVD  34097  csbima12gALTVD  34098  csbunigVD  34099  csbfv12gALTVD  34100  relopabVD  34102  isosctrlem1ALT  34135  bnj517  34344  bj-cbvexw  34636  bj-cbv3tb  34672  bj-spimtv  34679  bj-spvv  34685  bj-chvarv  34687  bj-cbvalv  34697  bj-cleqh  34759  bj-equsal  34800  bj-ax8  34862  bj-vtoclf  34881  bj-snsetex  34922  bj-inftyexpiinj  35012  bj-finsumval0  35063  bj-bary1lem1  35077  bj-bary1  35078  lsatn0  35121  l1cvpat  35176  leat2  35416  atnle  35439  cvlcvr1  35461  cvrexchlem  35540  cvratlem  35542  cvrat  35543  atcvrj0  35549  atle  35557  snatpsubN  35871  linepsubN  35873  pmapsub  35889  lneq2at  35899  lncvrelatN  35902  2llnma3r  35909  cdlemblem  35914  paddasslem5  35945  poml4N  36074  lhpmcvr4N  36147  trlval2  36285  cdlemd6  36325  cdleme7ga  36370  cdleme25b  36477  cdleme29b  36498  cdleme35fnpq  36572  cdleme50f1  36666  cdlemf1  36684  cdlemg27b  36819  cdlemk28-3  37031  tendospcanN  37147  diaf11N  37173  dia2dimlem1  37188  dibf11N  37285  dihf11  37391  dihmeetlem1N  37414  dochvalr  37481  dochnel2  37516  dvh4dimlem  37567  dochsat0  37581  mapd1o  37772  hdmapf1oN  37992  hgmapval0  38019  hgmapf1oN  38030  hlhilhillem  38087  axfrege52a  38333  axfrege52c  38364  suprleubrd  38435  suprlubrd  38439
  Copyright terms: Public domain W3C validator