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  1601  spfw  1658  spw  1661  cbvalw  1676  cbvalvw  1677  alcomiw  1679  19.9d  1786  dvelimv  1881  dral1  1908  cbval  1927  chvar  1929  spv  1943  sbequi  1998  dral1-o  2095  2eu3  2226  eqrdav  2283  cleqh  2381  ralcom2  2705  ceqsalg  2813  vtoclf  2838  vtocl2  2840  vtocl3  2841  spcdv  2867  rspcdv  2888  elabgt  2912  sbeqalb  3044  ssunsn2  3774  euotd  4266  sotr2  4342  onmindif  4481  elpwunsn  4567  onint  4585  oneqmin  4595  ordunisuc2  4634  tfindsg  4650  findsg  4682  relop  4833  elres  4989  elimasni  5039  sotri2  5071  relcnvtr  5190  dffv2  5554  mpteqb  5576  chfnrn  5598  elpreima  5607  iinpreima  5617  exfo  5640  ffnfv  5647  f1elima  5749  f1eqcocnv  5767  fliftfun  5773  soisores  5786  isotr  5795  isomin  5796  f1oweALT  5813  ovmpt2dv2  5943  iotaval  6264  smoiso  6375  seqomlem2  6459  oaordi  6540  oawordri  6544  oaordex  6552  oalimcl  6554  omwordi  6565  oewordi  6585  oelim2  6589  nnmwordi  6629  xpider  6726  iiner  6727  undifixp  6848  mptelixpg  6849  dom2lem  6897  nneneq  7040  fineqvlem  7073  pssnn  7077  dif1enOLD  7086  dif1en  7087  findcard2s  7095  unfilem2  7118  xpfi  7124  domunfican  7125  dffi2  7172  wemaplem2  7258  suc11reg  7316  noinfep  7356  cantnflem1  7387  r1fin  7441  tcrank  7550  cardlim  7601  pr2nelem  7630  fseqenlem1  7647  alephnbtwn  7694  alephord2i  7700  alephf1  7708  cardaleph  7712  alephiso  7721  dfac12lem2  7766  ackbij1lem16  7857  cflm  7872  cfcoflem  7894  sornom  7899  fin23lem27  7950  isf32lem7  7981  fin17  8016  fin1a2lem2  8023  fin1a2lem4  8025  fin1a2lem6  8027  fin1a2lem9  8030  axdc3lem2  8073  zorn2lem7  8125  uniimadom  8162  inar1  8393  grothomex  8447  addcanpi  8519  mulcanpi  8520  enqer  8541  genpcd  8626  genpnmax  8627  ltexprlem4  8659  reclem3pr  8669  reclem4pr  8670  suplem2pr  8673  axpre-ltadd  8785  axpre-sup  8787  ltletr  8909  00id  8983  mul0or  9404  prodgt02  9598  prodge02  9600  lemul1a  9606  mulgt1  9611  divgt0  9620  divge0  9621  ledivp1i  9678  ltdivp1i  9679  cju  9738  nnsub  9780  nominpos  9944  btwnnz  10084  uzindOLD  10102  ublbneg  10298  zmax  10309  cnref1o  10345  ltsubrp  10381  ltaddrp  10382  xrltletr  10484  qbtwnre  10522  xltnegi  10539  iccsupr  10732  icoshft  10754  difreicc  10763  iccshftri  10766  iccshftli  10768  iccdili  10770  icccntri  10772  fzen  10807  fzm1  10858  flval2  10940  flval3  10941  fseqsupubi  11036  sq01  11219  ccatopth2  11459  cjre  11620  o1lo1  12007  o1of2  12082  o1rlimmul  12088  zsum  12187  reeff1  12396  dvds2lem  12537  muldvds1  12549  dvdscmulr  12553  dvdsmulcr  12554  divalglem8  12595  ndvdsadd  12603  gcdmultiple  12725  isprm6  12784  isprm5  12787  prmdvdsexpr  12791  divgcdodd  12794  phiprmpw  12840  pythagtriplem4  12868  pcz  12929  1arith  12970  divsfval  13445  fthmon  13797  setcmon  13915  setcepi  13916  pltnle  14096  pltval3  14097  lubid  14112  latasym  14157  odupos  14235  mrelatglb  14283  mrelatlub  14285  cnvpsb  14318  isgrpid2  14514  ghmf1  14707  orbsta  14763  resscntz  14803  mndodcongi  14854  odf1  14871  lsmss1  14971  lsmss2  14973  efgredeu  15057  lt6abl  15177  ablfaclem3  15318  lspsneq  15871  lspsneu  15872  lsmcv  15890  lidldvgen  16003  domnmuln0  16035  opprdomn  16038  ply1scln0  16362  domnchr  16482  znf1o  16501  zntoslem  16506  znfld  16510  cygznlem2a  16517  cygznlem3  16519  0ntr  16804  islpi  16876  lmss  17022  cmpcld  17125  cmpfi  17131  1stcelcls  17183  ptcnplem  17311  qtophmeo  17504  fbdmn0  17525  fbasrn  17575  elfm3  17641  fmfnfmlem4  17648  fclscf  17716  cnpfcf  17732  alexsubALTlem3  17739  tsmsres  17822  nmoleub  18236  nmhmcn  18597  iscau4  18701  caussi  18719  cniccbdd  18817  ovoliunnul  18862  mbfinf  19016  itg2splitlem  19099  dvcn  19266  c1lip1  19340  c1lip3  19342  dvcnvrelem1  19360  ply1divex  19518  quotcan  19685  aannenlem1  19704  taylf  19736  ulmcaulem  19767  ulmcau  19768  reeff1o  19819  logccv  20006  logreclem  20112  isosctrlem2  20115  xrlimcnp  20259  rlimcxp  20264  ftalem7  20312  vmappw  20350  fsumvma  20448  dchreq  20493  dchrptlem1  20499  dchrsum  20504  bposlem7  20525  lgsqrlem2  20577  lgsdchr  20583  lgseisenlem2  20585  lgsquad2  20595  2sqlem6  20604  gxid  20934  opidon  20983  opidon2  20985  grpomndo  21007  elghomlem2  21023  rngoueqz  21091  dvrunz  21094  hlipgt0  21487  ocin  21871  ocnel  21873  shmodsi  21964  pjmf1  22291  unopf1o  22492  staddi  22822  stadd3i  22824  mdi  22871  dmdmd  22876  dmdi  22878  dmdbr2  22879  dmdbr3  22881  dmdbr4  22882  dmdi4  22883  mdsl1i  22897  superpos  22930  cvbr4i  22943  atssma  22954  atcv1  22956  atomli  22958  chirredlem1  22966  addltmulALT  23022  ifeqeqx  23030  elabreximd  23035  ballotlemfc0  23047  ballotlemfcc  23048  ballotlemsgt1  23065  ballotlemsel1i  23067  ballotlemfrceq  23083  ballotlemfrcn0  23084  ballotlemirc  23086  erdsze2lem2  23142  trpredrec  23645  poseq  23657  soseq  23658  sltval2  23713  sltres  23721  axdenselem7  23745  axdenselem8  23746  axdense  23747  axfelem9  23758  axfelem10  23759  axfelem16  23765  axfelem18  23767  dfrdg4  23898  altopthsn  23905  brbtwn  23937  brcgr  23938  axcgrid  23954  axeuclidlem  24000  axeuclid  24001  btwncomim  24046  btwnexch3  24053  btwnexch2  24056  endofsegid  24118  onsuct0  24290  ordcmp  24296  nndivsub  24306  dvreasin  24333  areacirclem2  24335  areacirclem3  24336  areacirclem5  24339  areacirc  24341  boxbid  24421  nxtbid  24422  diabid  24423  untbi12d  24432  domrngref  24470  restidsing  24486  fixpc  24504  reflincror  24522  eqfnung2  24529  prjpacp1  24538  prjpacp2  24539  injsurinj  24560  repfuntw  24571  islatalg  24594  oriso  24625  ubpar  24672  inpc  24688  dominc  24691  rninc  24692  toplat  24701  clfsebsr  24760  trooo  24805  imtr  24809  rngoridfz  24848  svs2  24898  truni1  24916  truni3  24918  inttop4  24928  nsn  24941  intcont  24954  cmptdst  24979  limptlimpr2lem2  24986  flfnei2  24988  islimrs4  24993  bwt2  25003  dmse1  25014  iintlem1  25021  supnuf  25040  negveud  25079  negveudr  25080  icccon2  25111  icccon4  25113  rdmob  25159  eqidob  25206  ismonc  25225  cmpmon  25226  idmon  25228  iepiclem  25234  isepic  25235  propsrc  25279  domcatfun  25336  codcatfun  25345  cmp2morp  25369  setiscat  25390  clscnc  25421  lineval6a  25500  sgplpte21c  25546  bosser  25578  pdiveql  25579  abhp  25584  bhp3  25588  opnrebl2  25647  nn0prpwlem  25649  comppfsc  25718  brabg2  25777  enf1f1oOLD  25808  fzmul  25854  fdc  25866  incsequz2  25870  isbnd2  25918  divrngidl  26064  rexrabdioph  26286  fphpdo  26311  icodiamlt  26316  irrapxlem3  26320  rmxypairf1o  26407  rmxycomplete  26413  zindbi  26442  lermxnn0  26448  ltrmy  26450  rmyeq0  26451  rmyeq  26452  lermy  26453  acongsym  26474  acongneg2  26475  wepwsolem  26549  expgrowthi  26961  ordpss  27065  refsum2cnlem1  27119  climinf  27143  stoweidlem7  27167  stoweidlem34  27194  stoweidlem59  27219  stoweidlem62  27222  2reu3  27357  ralbinrald  27368  funressnfv  27382  afv0fv0  27403  afv0nbfvbi  27405  afvfv0bi  27406  fnbrafvb  27407  afvres  27425  tz6.12-afv  27426  afvco2  27428  ndmaovcl  27454  bitr3  27555  rspsbc2  27580  tratrb  27582  sbcim2g  27585  truniALT  27588  tpid3gVD  27898  orbi1rVD  27904  sbc3orgVD  27907  rspsbc2VD  27911  tratrbVD  27917  sbcim2gVD  27931  sbcbiVD  27932  truniALTVD  27934  trintALTVD  27936  trintALT  27937  csbingVD  27940  csbsngVD  27949  csbxpgVD  27950  csbresgVD  27951  csbrngVD  27952  csbima12gALTVD  27953  csbunigVD  27954  csbfv12gALTVD  27955  relopabVD  27957  bnj517  28196  a12stdy2-x12  28391  ax10lem17ALT  28402  ax9lem17  28435  lsatn0  28468  l1cvpat  28523  leat2  28763  atnle  28786  cvlcvr1  28808  cvrexchlem  28887  cvratlem  28889  cvrat  28890  atcvrj0  28896  atle  28904  snatpsubN  29218  linepsubN  29220  pmapsub  29236  lneq2at  29246  lncvrelatN  29249  2llnma3r  29256  cdlemblem  29261  paddasslem5  29292  poml4N  29421  lhpmcvr4N  29494  trlval2  29631  cdlemd6  29671  cdleme7ga  29716  cdleme25b  29822  cdleme29b  29843  cdleme35fnpq  29917  cdleme50f1  30011  cdlemf1  30029  cdlemg27b  30164  cdlemk28-3  30376  tendospcanN  30492  diaf11N  30518  dia2dimlem1  30533  dibf11N  30630  dihf11  30736  dihmeetlem1N  30759  dochvalr  30826  dochnel2  30861  dvh4dimlem  30912  dochsat0  30926  mapd1o  31117  hdmapf1oN  31337  hgmapval0  31364  hgmapf1oN  31375  hlhilhillem  31432
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