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

Theorem biimpd 210
Description: Deduce an implication from a logical equivalence. Deduction associated with biimp 196 and biimpi 197. (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 biimp 196 . 2  |-  ( ( ps  <->  ch )  ->  ( ps  ->  ch ) )
31, 2syl 17 1  |-  ( ph  ->  ( ps  ->  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187
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 188
This theorem is referenced by:  mpbid  213  sylibd  217  sylbid  218  mpbidi  219  syl5ib  222  syl6bi  231  ibi  244  con4bid  294  mtbird  302  mtbiri  304  imbi1d  318  pm5.21im  350  biimpa  486  exintr  1749  spfw  1858  cbvalw  1860  alcomiw  1863  19.9dOLD  1949  19.23tOLD  1967  spimt  2061  spv  2067  chvar  2069  cbval  2077  nfsb4t  2184  2eu3  2357  eqrdav  2427  eqrdavOLD  2428  cleqhOLD  2545  rgen2a  2859  ralcom2  3000  ceqsalgALT  3113  vtoclf  3138  vtocl2  3140  vtocl3  3141  spcdv  3170  rspcdv  3191  rexraleqim  3203  elabgt  3221  sbcn1  3351  sbcim1  3352  sbcbi1  3353  sbeqalb  3358  sbcel21v  3366  eqrd  3488  elpwunsn  4043  rabsnifsb  4071  ssunsn2  4162  euotd  4722  sotr2  4804  relop  5005  elres  5160  restidsing  5181  elimasni  5215  sotri2  5249  relcnvtr  5375  onmindif  5531  iotaval  5576  dffv2  5954  mpteqb  5980  elfvmptrab  5987  chfnrn  6008  elpreima  6017  iinpreima  6025  exfo  6055  ffnfv  6064  f1elima  6179  f1eqcocnv  6214  fliftfun  6220  soisores  6233  isotr  6242  isomin  6243  ovmpt2dv2  6444  difsnexi  6613  onint  6636  oneqmin  6646  ordunisuc2  6685  tfindsg  6701  findsg  6734  f1oweALT  6791  ressuppss  6945  funsssuppss  6952  imacosupp  6966  smoiso  7089  seqomlem2  7176  oaordi  7255  oawordri  7259  oaordex  7267  oalimcl  7269  omwordi  7280  oewordi  7300  oelim2  7304  nnmwordi  7344  xpider  7442  iiner  7443  undifixp  7566  mptelixpg  7567  dom2lem  7616  nneneq  7761  fineqvlem  7792  pssnn  7796  dif1en  7810  findcard2s  7818  unfilem2  7842  xpfi  7848  domunfican  7850  f1dmvrnfibi  7864  fsuppimp  7895  dffi2  7943  wemaplem2  8062  suc11reg  8124  noinfep  8164  cantnflem1  8193  r1fin  8243  tcrank  8354  cardlim  8405  pr2nelem  8434  fseqenlem1  8453  alephnbtwn  8500  alephord2i  8506  alephf1  8514  cardaleph  8518  alephiso  8527  dfac12lem2  8572  ackbij1lem16  8663  cflm  8678  cfcoflem  8700  sornom  8705  fin23lem27  8756  isf32lem7  8787  fin17  8822  fin1a2lem2  8829  fin1a2lem4  8831  fin1a2lem6  8833  fin1a2lem9  8836  axdc3lem2  8879  zorn2lem7  8930  uniimadom  8967  inar1  9199  grothomex  9253  addcanpi  9323  mulcanpi  9324  enqer  9345  genpcd  9430  genpnmax  9431  ltexprlem4  9463  reclem3pr  9473  reclem4pr  9474  suplem2pr  9477  axpre-ltadd  9590  axpre-sup  9592  ltletr  9724  00id  9807  mul0or  10251  prodgt02  10450  prodge02  10452  lemul1a  10458  mulgt1  10463  divgt0  10472  divge0  10473  ledivp1i  10532  ltdivp1i  10533  cju  10605  nnsub  10648  nominpos  10849  nn0n0n1ge2  10932  btwnnz  11012  suprfinzcl  11050  ublbneg  11248  zmax  11261  cnref1o  11297  ltsubrp  11335  ltaddrp  11336  xrltletr  11454  qbtwnre  11492  xltnegi  11509  iccsupr  11727  icoshft  11752  difreicc  11762  iccshftri  11765  iccshftli  11767  iccdili  11769  icccntri  11771  fzen  11814  elfzmlbmOLD  11899  fzofzim  11960  eluzgtdifelfzo  11973  injresinjlem  12021  injresinj  12022  flval2  12046  flval3  12047  modaddmodup  12150  fseqsupubi  12188  ssnn0fi  12194  mptnn0fsuppr  12208  sq01  12391  hashf1rn  12532  hashle00  12574  hashgt12el  12590  hashgt12el2  12591  hash2pr  12624  hash2prb  12626  hashtpg  12632  hash3tr  12638  lswlgt0cl  12703  2swrd1eqwrdeq  12795  ccatopth2  12812  reuccats1lem  12821  swrdccatin2  12828  swrdccat  12834  swrdccat3a  12835  swrdccat3blem  12836  repsdf2  12866  repswsymball  12867  repswrevw  12874  cshweqrep  12905  cshw1  12906  2cshwcshw  12909  scshwfzeqfzo  12910  cshwcsh2id  12912  swrdco  12919  swrd2lsw  13006  2swrd2eqwrdeq  13007  wwlktovfo  13012  cjre  13181  o1lo1  13579  o1of2  13654  o1rlimmul  13660  zsum  13762  modfsummods  13831  zprod  13969  reeff1  14152  dvds2lem  14293  muldvds1  14305  dvdscmulr  14309  dvdsmulcr  14310  divalglem8  14356  ndvdsadd  14364  gcdmultiple  14489  absproddvds  14558  lcmftp  14580  prmn2uzge3  14615  isprm5  14622  divgcdodd  14624  isprm6  14637  prmdvdsexpr  14640  phiprmpw  14693  modprm0  14719  pythagtriplem4  14732  pcz  14793  1arith  14834  prmgaplem5  14988  prmgaplem6  14989  cshwrepswhash1  15036  divsfval  15404  catsubcat  15695  fthmon  15783  isinitoi  15849  istermoi  15850  iszeroi  15855  setcmon  15933  setcepi  15934  funcestrcsetclem8  15983  fthestrcsetc  15986  funcsetcestrclem8  15998  fthsetcestrc  16001  pltnle  16163  pltval3  16164  lublecllem  16185  latasym  16252  odupos  16332  mrelatglb  16381  mrelatlub  16383  cnvpsb  16410  isgrpid2  16653  ghmf1  16862  orbsta  16918  resscntz  16936  gsmsymgrfixlem1  17019  gsmsymgreqlem2  17023  mndodcongi  17134  odf1  17151  lsmss1  17251  lsmss2  17253  efgredeu  17337  cntzcmnss  17416  lt6abl  17464  ablfaclem3  17655  kerf1hrm  17906  lspsneq  18280  lspsneu  18281  lsmcv  18299  lidldvgen  18414  0ringnnzr  18428  domnmuln0  18457  opprdomn  18460  ply1scln0  18819  gsummoncoe1  18833  domnchr  19034  znf1o  19053  zntoslem  19058  znfld  19062  cygznlem2a  19069  cygznlem3  19071  islindf4  19327  uvcendim  19336  matvscl  19387  scmataddcl  19472  scmatsubcl  19473  scmatfo  19486  scmatghm  19489  maducoeval2  19596  slesolinv  19636  cramerimplem2  19640  cpmatelimp  19667  cpmatelimp2  19669  cpmatacl  19671  cpmatinvcl  19672  pm2mpf1  19754  cayhamlem1  19821  cayleyhamilton1  19847  0ntr  20018  islpi  20096  lmss  20245  cmpcld  20348  cmpfi  20354  1stcelcls  20407  comppfsc  20478  ptcnplem  20567  qtophmeo  20763  fbdmn0  20780  fbasrn  20830  elfm3  20896  fmfnfmlem4  20903  fclscf  20971  cnpfcf  20987  alexsubALTlem3  20995  tsmsres  21089  blval2  21508  nmoleub  21663  nmhmcn  22027  iscau4  22142  caussi  22160  cniccbdd  22293  ovoliunnul  22338  mbfinf  22498  mbfinfOLD  22499  itg2splitlem  22583  dvcn  22752  c1lip1  22826  c1lip3  22828  dvcnvrelem1  22846  ply1divex  22962  quotcan  23130  aannenlem1  23149  taylf  23181  ulmcaulem  23214  ulmcau  23215  reeff1o  23267  logccv  23473  logreclem  23564  isosctrlem2  23613  xrlimcnp  23759  rlimcxp  23764  ftalem7  23868  vmappw  23906  fsumvma  24004  dchreq  24049  dchrptlem1  24055  dchrsum  24060  bposlem7  24081  lgsqrlem2  24133  lgsdchr  24139  lgseisenlem2  24141  lgsquad2  24151  2sqlem6  24160  tgcgrcomimp  24384  isperp2  24617  xmstrkgc  24762  brbtwn  24775  brcgr  24776  axcgrid  24792  axeuclidlem  24838  axeuclid  24839  uhgraeq12d  24880  usgrac  24924  usgraeq12d  24935  usgranloopv  24951  nbgraf1olem5  25018  iscusgra0  25030  cusgrasize2inds  25050  cusgrafilem3  25054  usgramaxsize  25060  iswlkg  25097  wlkcompim  25099  wlkcpr  25102  wlkonprop  25108  trlonprop  25117  0wlkon  25122  usgrnloop  25138  pthonprop  25152  spthonprp  25160  redwlk  25181  wlkdvspthlem  25182  usgra2wlkspthlem2  25193  fargshiftfv  25208  wwlknimp  25260  vfwlkniswwlkn  25279  usg2wlkeq  25281  wwlknred  25296  wwlknext  25297  wwlknextbi  25298  wwlkextwrd  25301  wwlkextinj  25303  wwlkextsur  25304  wwlkm1edg  25308  isclwlkg  25328  clwlkcompim  25337  0clwlk  25338  clwwlkn2  25348  clwlkisclwwlklem2a1  25352  clwlkisclwwlklem2a4  25357  clwlkisclwwlklem2a  25358  clwlkisclwwlklem1  25360  clwwlkf  25367  wwlkext2clwwlk  25376  clwwisshclwwlem1  25378  wlklenvclwlk  25412  clwlkfclwwlk  25417  el2spthonot  25443  usg2wotspth  25457  usg2spthonot  25461  usg2spthonot0  25462  rgraprop  25501  rusgraprop  25502  rusgraprop3  25516  frgranbnb  25593  frgrancvvdeqlem3  25605  frgrancvvdeqlem4  25606  frgrancvvdeqlem7  25609  frgrawopreglem2  25618  frgrawopreg  25622  frgregordn0  25643  clwwlkextfrlem1  25649  extwwlkfablem2  25651  numclwwlkun  25652  numclwwlkovf2ex  25659  numclwlk1lem2foa  25664  numclwlk1lem2f1  25667  numclwwlk8  25688  gxid  25846  opidonOLD  25895  opidon2OLD  25897  grpomndo  25919  elghomlem2OLD  25935  rngoueqz  26003  dvrunz  26006  rngoridfz  26008  hlipgt0  26401  ocin  26784  ocnel  26786  shmodsi  26877  pjmf1  27204  unopf1o  27404  staddi  27734  stadd3i  27736  mdi  27783  dmdmd  27788  dmdi  27790  dmdbr2  27791  dmdbr3  27793  dmdbr4  27794  dmdi4  27795  mdsl1i  27809  superpos  27842  cvbr4i  27855  atssma  27866  atcv1  27868  atomli  27870  chirredlem1  27878  addltmulALT  27934  bian1d  27935  ifeqeqx  27997  disjxpin  28037  suppss3  28155  fpwrelmap  28161  xrge0infss  28181  ogrpaddlt  28319  metider  28536  tpr2rico  28557  xrge0iifiso  28580  qqhcn  28634  qqhucn  28635  esumlub  28720  esumpinfval  28733  esumpinfsum  28737  ballotlemfc0  29151  ballotlemfcc  29152  bnj517  29484  erdsze2lem2  29715  trpredrec  30266  poseq  30278  soseq  30279  sltval2  30330  sltres  30338  nodenselem7  30361  nodenselem8  30362  nodense  30363  nobndup  30374  nobnddown  30375  nofulllem5  30380  dfrdg4  30503  altopthsn  30513  btwncomim  30565  btwnexch3  30572  btwnexch2  30575  endofsegid  30637  opnrebl2  30762  nn0prpwlem  30763  onsuct0  30886  ordcmp  30892  nndivsub  30902  bj-cbvexw  31015  bj-cbv3tb  31051  bj-spimtv  31058  bj-spvv  31064  bj-chvarv  31066  bj-cbvalv  31076  bj-cleqh  31138  bj-equsal  31179  bj-ax8  31245  bj-vtoclf  31265  bj-snsetex  31306  bj-inftyexpiinj  31396  bj-finsumval0  31447  bj-bary1lem1  31461  bj-bary1  31462  f1omptsnlem  31472  iooelexlt  31499  relowlpssretop  31501  wl-equsal1i  31583  wl-ax11-lem10  31628  ltflcei  31637  sin2h  31639  cos2h  31640  tan2h  31641  poimirlem3  31647  poimirlem4  31648  poimirlem18  31662  poimirlem20  31664  poimirlem21  31665  poimirlem22  31666  poimirlem24  31668  poimirlem25  31669  poimirlem26  31670  poimirlem27  31671  poimirlem28  31672  poimirlem31  31675  poimir  31677  heicant  31679  mblfinlem1  31681  mblfinlem2  31682  mblfinlem3  31683  mblfinlem4  31684  mbfresfi  31691  cnambfre  31693  dvtanlemOLD  31695  ftc1anc  31729  dvasin  31732  areacirclem1  31736  areacirclem4  31739  areacirc  31741  brabg2  31746  fzmul  31773  fdc  31778  incsequz2  31782  isbnd2  31819  divrngidl  31965  dral1-o  32183  lsatn0  32274  l1cvpat  32329  leat2  32569  atnle  32592  cvlcvr1  32614  cvrexchlem  32693  cvratlem  32695  cvrat  32696  atcvrj0  32702  atle  32710  snatpsubN  33024  linepsubN  33026  pmapsub  33042  lneq2at  33052  lncvrelatN  33055  2llnma3r  33062  cdlemblem  33067  paddasslem5  33098  poml4N  33227  lhpmcvr4N  33300  trlval2  33438  cdlemd6  33478  cdleme7ga  33523  cdleme25b  33630  cdleme29b  33651  cdleme35fnpq  33725  cdleme50f1  33819  cdlemf1  33837  cdlemg27b  33972  cdlemk28-3  34184  tendospcanN  34300  diaf11N  34326  dia2dimlem1  34341  dibf11N  34438  dihf11  34544  dihmeetlem1N  34567  dochvalr  34634  dochnel2  34669  dvh4dimlem  34720  dochsat0  34734  mapd1o  34925  hdmapf1oN  35145  hgmapval0  35172  hgmapf1oN  35183  hlhilhillem  35240  rexrabdioph  35346  fphpdo  35369  icodiamlt  35374  irrapxlem3  35378  rmxypairf1o  35465  rmxycomplete  35471  zindbi  35500  lermxnn0  35506  ltrmy  35508  rmyeq0  35509  rmyeq  35510  lermy  35511  acongsym  35532  acongneg2  35533  wepwsolem  35606  ss2iundf  35890  frege129d  35994  frege133d  35996  axfrege52a  36089  axfrege52c  36120  suprleubrd  36246  suprlubrd  36250  radcnvrat  36300  nzss  36303  expgrowthi  36319  ordpss  36441  bi23impib  36478  bi23imp13  36484  bitr3  36504  rspsbc2  36532  tratrb  36534  sbcim2g  36536  truniALT  36539  3impcombi  36844  tpid3gVD  36878  orbi1rVD  36884  sbc3orgVD  36887  rspsbc2VD  36891  tratrbVD  36898  sbcim2gVD  36912  sbcbiVD  36913  truniALTVD  36915  trintALTVD  36917  trintALT  36918  csbingVD  36921  csbsngVD  36930  csbxpgVD  36931  csbresgVD  36932  csbrngVD  36933  csbima12gALTVD  36934  csbunigVD  36935  csbfv12gALTVD  36936  relopabVD  36938  isosctrlem1ALT  36971  fzisoeu  37127  climinf  37256  climinfOLD  37257  stoweidlem7  37436  stoweidlem62  37492  stoweidlem62OLD  37493  sge0gerpmpt  37778  carageniuncllem2  37852  2reu3  38009  ralbinrald  38020  funressnfv  38029  afv0fv0  38050  afv0nbfvbi  38052  afvfv0bi  38053  fnbrafvb  38055  afvres  38073  tz6.12-afv  38074  afvco2  38077  ndmaovcl  38104  nltle2tri  38115  mod2eq1n2dvds  38124  iccpartres  38131  iccpartiltu  38135  evennodd  38172  oddneven  38173  oexpnegALTV  38205  oexpnegnz  38206  gboge7  38263  gbege6  38265  bgoldbwt  38277  bgoldbst  38278  nnsum3primesle9  38288  bgoldbtbndlem2  38300  pfxfv  38339  pfxsuff1eqwrdeq  38347  reuccatpfxs1lem  38373  zm1nn  38407  subsubelfzo0  38420  usgra2pth  38433  usgpredgv  38478  usgpredgvALT  38479  usgfis  38525  usgfisALT  38529  mgmpropd  38542  clintop  38611  isassintop  38613  lidldomn1  38688  uzlidlring  38696  2zrngnmlid2  38718  rngccatidALTV  38758  ringccatidALTV  38821  srhmsubc  38845  srhmsubcALTV  38864  ztprmneprm  38897  pgrpgt2nabl  38920  lindslinindimp2lem4  39023  lincresunit3  39043  fldivexpfllog2  39146  digexp  39188
  Copyright terms: Public domain W3C validator