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

Theorem biimpd 198
Description: Deduce an implication from a logical equivalence. (Contributed by NM, 5-Aug-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 178 . 2  |-  ( ( ps  <->  ch )  ->  ( ps  ->  ch ) )
31, 2syl 15 1  |-  ( ph  ->  ( ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  mpbid  201  sylibd  205  sylbid  206  mpbidi  207  syl5ib  210  syl6bi  219  ibi  232  con4bid  284  mtbird  292  mtbiri  294  imbi1d  308  pm5.21im  338  biimpa  470  exintr  1605  spfw  1682  spw  1685  cbvalw  1692  cbvalvw  1693  alcomiw  1695  19.9d  1815  dvelimv  1911  dral1  1937  cbval  1956  chvar  1958  spv  1970  sbequi  2031  dral1-o  2126  2eu3  2258  eqrdav  2315  cleqh  2413  ralcom2  2738  ceqsalg  2846  vtoclf  2871  vtocl2  2873  vtocl3  2874  spcdv  2900  rspcdv  2921  elabgt  2945  sbeqalb  3077  ssunsn2  3810  euotd  4304  sotr2  4380  onmindif  4519  elpwunsn  4605  onint  4623  oneqmin  4633  ordunisuc2  4672  tfindsg  4688  findsg  4720  relop  4871  elres  5027  elimasni  5077  sotri2  5109  relcnvtr  5229  iotaval  5267  tz6.12-1  5582  dffv2  5630  mpteqb  5652  chfnrn  5674  elpreima  5683  iinpreima  5693  exfo  5716  ffnfv  5723  f1elima  5829  f1eqcocnv  5847  fliftfun  5853  soisores  5866  isotr  5875  isomin  5876  f1oweALT  5893  ovmpt2dv2  6023  smoiso  6421  seqomlem2  6505  oaordi  6586  oawordri  6590  oaordex  6598  oalimcl  6600  omwordi  6611  oewordi  6631  oelim2  6635  nnmwordi  6675  xpider  6772  iiner  6773  undifixp  6895  mptelixpg  6896  dom2lem  6944  nneneq  7087  fineqvlem  7120  pssnn  7124  dif1enOLD  7135  dif1en  7136  findcard2s  7144  unfilem2  7167  xpfi  7173  domunfican  7174  dffi2  7221  wemaplem2  7307  suc11reg  7365  noinfep  7405  cantnflem1  7436  r1fin  7490  tcrank  7599  cardlim  7650  pr2nelem  7679  fseqenlem1  7696  alephnbtwn  7743  alephord2i  7749  alephf1  7757  cardaleph  7761  alephiso  7770  dfac12lem2  7815  ackbij1lem16  7906  cflm  7921  cfcoflem  7943  sornom  7948  fin23lem27  7999  isf32lem7  8030  fin17  8065  fin1a2lem2  8072  fin1a2lem4  8074  fin1a2lem6  8076  fin1a2lem9  8079  axdc3lem2  8122  zorn2lem7  8174  uniimadom  8211  inar1  8442  grothomex  8496  addcanpi  8568  mulcanpi  8569  enqer  8590  genpcd  8675  genpnmax  8676  ltexprlem4  8708  reclem3pr  8718  reclem4pr  8719  suplem2pr  8722  axpre-ltadd  8834  axpre-sup  8836  ltletr  8958  00id  9032  mul0or  9453  prodgt02  9647  prodge02  9649  lemul1a  9655  mulgt1  9660  divgt0  9669  divge0  9670  ledivp1i  9727  ltdivp1i  9728  cju  9787  nnsub  9829  nominpos  9995  btwnnz  10135  uzindOLD  10153  ublbneg  10349  zmax  10360  cnref1o  10396  ltsubrp  10432  ltaddrp  10433  xrltletr  10535  qbtwnre  10573  xltnegi  10590  iccsupr  10783  icoshft  10805  difreicc  10814  iccshftri  10817  iccshftli  10819  iccdili  10821  icccntri  10823  fzen  10858  fzm1  10909  flval2  10991  flval3  10992  fseqsupubi  11087  sq01  11270  ccatopth2  11510  cjre  11671  o1lo1  12058  o1of2  12133  o1rlimmul  12139  zsum  12238  reeff1  12447  dvds2lem  12588  muldvds1  12600  dvdscmulr  12604  dvdsmulcr  12605  divalglem8  12646  ndvdsadd  12654  gcdmultiple  12776  isprm6  12835  isprm5  12838  prmdvdsexpr  12842  divgcdodd  12845  phiprmpw  12891  pythagtriplem4  12919  pcz  12980  1arith  13021  divsfval  13498  fthmon  13850  setcmon  13968  setcepi  13969  pltnle  14149  pltval3  14150  lubid  14165  latasym  14210  odupos  14288  mrelatglb  14336  mrelatlub  14338  cnvpsb  14371  isgrpid2  14567  ghmf1  14760  orbsta  14816  resscntz  14856  mndodcongi  14907  odf1  14924  lsmss1  15024  lsmss2  15026  efgredeu  15110  lt6abl  15230  ablfaclem3  15371  lspsneq  15924  lspsneu  15925  lsmcv  15943  lidldvgen  16056  domnmuln0  16088  opprdomn  16091  ply1scln0  16415  domnchr  16542  znf1o  16561  zntoslem  16566  znfld  16570  cygznlem2a  16577  cygznlem3  16579  0ntr  16864  islpi  16936  lmss  17082  cmpcld  17185  cmpfi  17191  1stcelcls  17243  ptcnplem  17371  qtophmeo  17564  fbdmn0  17581  fbasrn  17631  elfm3  17697  fmfnfmlem4  17704  fclscf  17772  cnpfcf  17788  alexsubALTlem3  17795  tsmsres  17878  nmoleub  18292  nmhmcn  18654  iscau4  18758  caussi  18776  cniccbdd  18874  ovoliunnul  18919  mbfinf  19073  itg2splitlem  19156  dvcn  19323  c1lip1  19397  c1lip3  19399  dvcnvrelem1  19417  ply1divex  19575  quotcan  19742  aannenlem1  19761  taylf  19793  ulmcaulem  19824  ulmcau  19825  reeff1o  19876  logccv  20063  logreclem  20169  isosctrlem2  20172  xrlimcnp  20316  rlimcxp  20321  ftalem7  20369  vmappw  20407  fsumvma  20505  dchreq  20550  dchrptlem1  20556  dchrsum  20561  bposlem7  20582  lgsqrlem2  20634  lgsdchr  20640  lgseisenlem2  20642  lgsquad2  20652  2sqlem6  20661  gxid  20993  opidon  21042  opidon2  21044  grpomndo  21066  elghomlem2  21082  rngoueqz  21150  dvrunz  21153  rngoridfz  21155  hlipgt0  21548  ocin  21930  ocnel  21932  shmodsi  22023  pjmf1  22350  unopf1o  22551  staddi  22881  stadd3i  22883  mdi  22930  dmdmd  22935  dmdi  22937  dmdbr2  22938  dmdbr3  22940  dmdbr4  22941  dmdi4  22942  mdsl1i  22956  superpos  22989  cvbr4i  23002  atssma  23013  atcv1  23015  atomli  23017  chirredlem1  23025  addltmulALT  23081  bian1d  23084  elabreximd  23128  eqrd  23132  ifeqeqx  23144  disjdsct  23240  ctex  23250  xrsinvgval  23341  xrge0addass  23349  cnre2csqlem  23377  tpr2rico  23379  xrge0iifiso  23390  lmxrge0  23406  blval2  23506  elzrhunit  23558  qqhval2lem  23560  qqhcn  23570  esumlub  23628  esumpinfval  23639  esumpinfsum  23643  esumpcvgval  23644  mbfmf  23779  mbfmcnt  23792  ballotlemfc0  23924  ballotlemfcc  23925  ballotlemsgt1  23942  ballotlemsel1i  23944  ballotlemfrceq  23960  ballotlemfrcn0  23961  ballotlemirc  23963  erdsze2lem2  24019  zprod  24440  trpredrec  24626  poseq  24638  soseq  24639  sltval2  24695  sltres  24703  nodenselem7  24726  nodenselem8  24727  nodense  24728  nobndup  24739  nobnddown  24740  nofulllem5  24745  dfrdg4  24874  altopthsn  24881  brbtwn  24913  brcgr  24914  axcgrid  24930  axeuclidlem  24976  axeuclid  24977  btwncomim  25022  btwnexch3  25029  btwnexch2  25032  endofsegid  25094  onsuct0  25266  ordcmp  25272  nndivsub  25282  ltflcei  25312  dvreasin  25340  areacirclem2  25342  areacirclem3  25343  areacirclem5  25346  areacirc  25348  opnrebl2  25385  nn0prpwlem  25387  comppfsc  25456  brabg2  25515  enf1f1oOLD  25546  fzmul  25592  fdc  25604  incsequz2  25608  isbnd2  25655  divrngidl  25801  rexrabdioph  26023  fphpdo  26048  icodiamlt  26053  irrapxlem3  26057  rmxypairf1o  26144  rmxycomplete  26150  zindbi  26179  lermxnn0  26185  ltrmy  26187  rmyeq0  26188  rmyeq  26189  lermy  26190  acongsym  26211  acongneg2  26212  wepwsolem  26286  expgrowthi  26698  ordpss  26802  refsum2cnlem1  26856  climinf  26880  stoweidlem7  26904  stoweidlem34  26931  stoweidlem59  26956  stoweidlem62  26959  2reu3  27114  ralbinrald  27125  funressnfv  27141  afv0fv0  27162  afv0nbfvbi  27164  afvfv0bi  27165  fnbrafvb  27167  afvres  27185  tz6.12-afv  27186  afvco2  27189  ndmaovcl  27216  nn0n0n1ge2  27267  injresinjlem  27276  injresinj  27277  hashtpg  27279  hashgt12el  27280  hashgt12el2  27281  hash2pr  27283  uhgraeq12d  27310  usgraeq12d  27337  usgranloop  27350  nbusgra  27377  nbgraf1olem5  27392  iscusgra0  27403  wlkonprop  27444  trlonprop  27454  0wlkon  27459  usgrnloop  27467  pthonprop  27479  redwlk  27502  wlkdvspthlem  27503  fargshiftfv  27518  frgranbnb  27612  frgrancvvdeqlem3  27624  frgrancvvdeqlem4  27625  frgrancvvdeqlem7  27628  bi23impib  27744  bi123impib  27746  bi123impia  27748  bitr3  27766  rspsbc2  27791  tratrb  27793  sbcim2g  27796  truniALT  27799  3impcombi  28101  tpid3gVD  28129  orbi1rVD  28135  sbc3orgVD  28138  rspsbc2VD  28142  tratrbVD  28148  sbcim2gVD  28162  sbcbiVD  28163  truniALTVD  28165  trintALTVD  28167  trintALT  28168  csbingVD  28171  csbsngVD  28180  csbxpgVD  28181  csbresgVD  28182  csbrngVD  28183  csbima12gALTVD  28184  csbunigVD  28185  csbfv12gALTVD  28186  relopabVD  28188  bnj517  28428  dvelimvNEW7  28634  dral1NEW7  28665  cbvalwwAUX7  28689  sbequiNEW7  28748  chvarNEW7  28787  spvNEW7  28790  cbvalOLD7  28875  a12stdy2-x12  28930  ax10lem17ALT  28941  ax9lem17  28974  lsatn0  29007  l1cvpat  29062  leat2  29302  atnle  29325  cvlcvr1  29347  cvrexchlem  29426  cvratlem  29428  cvrat  29429  atcvrj0  29435  atle  29443  snatpsubN  29757  linepsubN  29759  pmapsub  29775  lneq2at  29785  lncvrelatN  29788  2llnma3r  29795  cdlemblem  29800  paddasslem5  29831  poml4N  29960  lhpmcvr4N  30033  trlval2  30170  cdlemd6  30210  cdleme7ga  30255  cdleme25b  30361  cdleme29b  30382  cdleme35fnpq  30456  cdleme50f1  30550  cdlemf1  30568  cdlemg27b  30703  cdlemk28-3  30915  tendospcanN  31031  diaf11N  31057  dia2dimlem1  31072  dibf11N  31169  dihf11  31275  dihmeetlem1N  31298  dochvalr  31365  dochnel2  31400  dvh4dimlem  31451  dochsat0  31465  mapd1o  31656  hdmapf1oN  31876  hgmapval0  31903  hgmapf1oN  31914  hlhilhillem  31971
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
  Copyright terms: Public domain W3C validator