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  1657  spw  1660  cbvalw  1675  cbvalvw  1676  alcomiw  1678  19.9d  1784  dvelimv  1879  dral1  1905  cbval  1924  chvar  1926  spv  1938  sbequi  1999  dral1-o  2093  2eu3  2225  eqrdav  2282  cleqh  2380  ralcom2  2704  ceqsalg  2812  vtoclf  2837  vtocl2  2839  vtocl3  2840  spcdv  2866  rspcdv  2887  elabgt  2911  sbeqalb  3043  ssunsn2  3773  euotd  4267  sotr2  4343  onmindif  4482  elpwunsn  4568  onint  4586  oneqmin  4596  ordunisuc2  4635  tfindsg  4651  findsg  4683  relop  4834  elres  4990  elimasni  5040  sotri2  5072  relcnvtr  5192  iotaval  5230  tz6.12-1  5544  dffv2  5592  mpteqb  5614  chfnrn  5636  elpreima  5645  iinpreima  5655  exfo  5678  ffnfv  5685  f1elima  5787  f1eqcocnv  5805  fliftfun  5811  soisores  5824  isotr  5833  isomin  5834  f1oweALT  5851  ovmpt2dv2  5981  smoiso  6379  seqomlem2  6463  oaordi  6544  oawordri  6548  oaordex  6556  oalimcl  6558  omwordi  6569  oewordi  6589  oelim2  6593  nnmwordi  6633  xpider  6730  iiner  6731  undifixp  6852  mptelixpg  6853  dom2lem  6901  nneneq  7044  fineqvlem  7077  pssnn  7081  dif1enOLD  7090  dif1en  7091  findcard2s  7099  unfilem2  7122  xpfi  7128  domunfican  7129  dffi2  7176  wemaplem2  7262  suc11reg  7320  noinfep  7360  cantnflem1  7391  r1fin  7445  tcrank  7554  cardlim  7605  pr2nelem  7634  fseqenlem1  7651  alephnbtwn  7698  alephord2i  7704  alephf1  7712  cardaleph  7716  alephiso  7725  dfac12lem2  7770  ackbij1lem16  7861  cflm  7876  cfcoflem  7898  sornom  7903  fin23lem27  7954  isf32lem7  7985  fin17  8020  fin1a2lem2  8027  fin1a2lem4  8029  fin1a2lem6  8031  fin1a2lem9  8034  axdc3lem2  8077  zorn2lem7  8129  uniimadom  8166  inar1  8397  grothomex  8451  addcanpi  8523  mulcanpi  8524  enqer  8545  genpcd  8630  genpnmax  8631  ltexprlem4  8663  reclem3pr  8673  reclem4pr  8674  suplem2pr  8677  axpre-ltadd  8789  axpre-sup  8791  ltletr  8913  00id  8987  mul0or  9408  prodgt02  9602  prodge02  9604  lemul1a  9610  mulgt1  9615  divgt0  9624  divge0  9625  ledivp1i  9682  ltdivp1i  9683  cju  9742  nnsub  9784  nominpos  9948  btwnnz  10088  uzindOLD  10106  ublbneg  10302  zmax  10313  cnref1o  10349  ltsubrp  10385  ltaddrp  10386  xrltletr  10488  qbtwnre  10526  xltnegi  10543  iccsupr  10736  icoshft  10758  difreicc  10767  iccshftri  10770  iccshftli  10772  iccdili  10774  icccntri  10776  fzen  10811  fzm1  10862  flval2  10944  flval3  10945  fseqsupubi  11040  sq01  11223  ccatopth2  11463  cjre  11624  o1lo1  12011  o1of2  12086  o1rlimmul  12092  zsum  12191  reeff1  12400  dvds2lem  12541  muldvds1  12553  dvdscmulr  12557  dvdsmulcr  12558  divalglem8  12599  ndvdsadd  12607  gcdmultiple  12729  isprm6  12788  isprm5  12791  prmdvdsexpr  12795  divgcdodd  12798  phiprmpw  12844  pythagtriplem4  12872  pcz  12933  1arith  12974  divsfval  13449  fthmon  13801  setcmon  13919  setcepi  13920  pltnle  14100  pltval3  14101  lubid  14116  latasym  14161  odupos  14239  mrelatglb  14287  mrelatlub  14289  cnvpsb  14322  isgrpid2  14518  ghmf1  14711  orbsta  14767  resscntz  14807  mndodcongi  14858  odf1  14875  lsmss1  14975  lsmss2  14977  efgredeu  15061  lt6abl  15181  ablfaclem3  15322  lspsneq  15875  lspsneu  15876  lsmcv  15894  lidldvgen  16007  domnmuln0  16039  opprdomn  16042  ply1scln0  16366  domnchr  16486  znf1o  16505  zntoslem  16510  znfld  16514  cygznlem2a  16521  cygznlem3  16523  0ntr  16808  islpi  16880  lmss  17026  cmpcld  17129  cmpfi  17135  1stcelcls  17187  ptcnplem  17315  qtophmeo  17508  fbdmn0  17529  fbasrn  17579  elfm3  17645  fmfnfmlem4  17652  fclscf  17720  cnpfcf  17736  alexsubALTlem3  17743  tsmsres  17826  nmoleub  18240  nmhmcn  18601  iscau4  18705  caussi  18723  cniccbdd  18821  ovoliunnul  18866  mbfinf  19020  itg2splitlem  19103  dvcn  19270  c1lip1  19344  c1lip3  19346  dvcnvrelem1  19364  ply1divex  19522  quotcan  19689  aannenlem1  19708  taylf  19740  ulmcaulem  19771  ulmcau  19772  reeff1o  19823  logccv  20010  logreclem  20116  isosctrlem2  20119  xrlimcnp  20263  rlimcxp  20268  ftalem7  20316  vmappw  20354  fsumvma  20452  dchreq  20497  dchrptlem1  20503  dchrsum  20508  bposlem7  20529  lgsqrlem2  20581  lgsdchr  20587  lgseisenlem2  20589  lgsquad2  20599  2sqlem6  20608  gxid  20940  opidon  20989  opidon2  20991  grpomndo  21013  elghomlem2  21029  rngoueqz  21097  dvrunz  21100  hlipgt0  21493  ocin  21875  ocnel  21877  shmodsi  21968  pjmf1  22295  unopf1o  22496  staddi  22826  stadd3i  22828  mdi  22875  dmdmd  22880  dmdi  22882  dmdbr2  22883  dmdbr3  22885  dmdbr4  22886  dmdi4  22887  mdsl1i  22901  superpos  22934  cvbr4i  22947  atssma  22958  atcv1  22960  atomli  22962  chirredlem1  22970  addltmulALT  23026  ifeqeqx  23034  elabreximd  23039  ballotlemfc0  23051  ballotlemfcc  23052  ballotlemsgt1  23069  ballotlemsel1i  23071  ballotlemfrceq  23087  ballotlemfrcn0  23088  ballotlemirc  23090  bian1d  23122  eqrd  23126  cnre2csqlem  23294  tpr2rico  23296  xrsinvgval  23306  xrge0iifiso  23317  xrge0addass  23329  ctex  23336  disjdsct  23369  lmxrge0  23375  esumpinfval  23441  esumpinfsum  23445  esumpcvgval  23446  mbfmf  23560  mbfmcnt  23573  erdsze2lem2  23735  trpredrec  24241  poseq  24253  soseq  24254  sltval2  24310  sltres  24318  nodenselem7  24341  nodenselem8  24342  nodense  24343  nobndup  24354  nobnddown  24355  nofulllem5  24360  dfrdg4  24488  altopthsn  24495  brbtwn  24527  brcgr  24528  axcgrid  24544  axeuclidlem  24590  axeuclid  24591  btwncomim  24636  btwnexch3  24643  btwnexch2  24646  endofsegid  24708  onsuct0  24880  ordcmp  24886  nndivsub  24896  dvreasin  24923  areacirclem2  24925  areacirclem3  24926  areacirclem5  24929  areacirc  24931  boxbid  25011  nxtbid  25012  diabid  25013  untbi12d  25022  domrngref  25060  restidsing  25076  fixpc  25094  reflincror  25112  eqfnung2  25118  prjpacp1  25127  prjpacp2  25128  injsurinj  25149  islatalg  25183  oriso  25214  ubpar  25261  inpc  25277  dominc  25280  rninc  25281  toplat  25290  clfsebsr  25349  trooo  25394  imtr  25398  rngoridfz  25437  svs2  25487  truni1  25505  truni3  25507  inttop4  25517  nsn  25530  intcont  25543  cmptdst  25568  limptlimpr2lem2  25575  flfnei2  25577  islimrs4  25582  bwt2  25592  dmse1  25603  iintlem1  25610  supnuf  25629  negveud  25668  negveudr  25669  icccon2  25700  icccon4  25702  rdmob  25748  eqidob  25795  ismonc  25814  cmpmon  25815  idmon  25817  iepiclem  25823  isepic  25824  propsrc  25868  domcatfun  25925  codcatfun  25934  cmp2morp  25958  setiscat  25979  clscnc  26010  lineval6a  26089  sgplpte21c  26135  bosser  26167  pdiveql  26168  abhp  26173  bhp3  26177  opnrebl2  26236  nn0prpwlem  26238  comppfsc  26307  brabg2  26366  enf1f1oOLD  26397  fzmul  26443  fdc  26455  incsequz2  26459  isbnd2  26507  divrngidl  26653  rexrabdioph  26875  fphpdo  26900  icodiamlt  26905  irrapxlem3  26909  rmxypairf1o  26996  rmxycomplete  27002  zindbi  27031  lermxnn0  27037  ltrmy  27039  rmyeq0  27040  rmyeq  27041  lermy  27042  acongsym  27063  acongneg2  27064  wepwsolem  27138  expgrowthi  27550  ordpss  27654  refsum2cnlem1  27708  climinf  27732  stoweidlem7  27756  stoweidlem34  27783  stoweidlem59  27808  stoweidlem62  27811  2reu3  27966  ralbinrald  27977  funressnfv  27991  afv0fv0  28012  afv0nbfvbi  28014  afvfv0bi  28015  fnbrafvb  28016  afvres  28034  tz6.12-afv  28035  afvco2  28037  ndmaovcl  28063  usgraeq12d  28111  usgranloop  28124  nbusgra  28143  iscusgra0  28154  bitr3  28272  rspsbc2  28297  tratrb  28299  sbcim2g  28302  truniALT  28305  tpid3gVD  28618  orbi1rVD  28624  sbc3orgVD  28627  rspsbc2VD  28631  tratrbVD  28637  sbcim2gVD  28651  sbcbiVD  28652  truniALTVD  28654  trintALTVD  28656  trintALT  28657  csbingVD  28660  csbsngVD  28669  csbxpgVD  28670  csbresgVD  28671  csbrngVD  28672  csbima12gALTVD  28673  csbunigVD  28674  csbfv12gALTVD  28675  relopabVD  28677  bnj517  28917  a12stdy2-x12  29112  ax10lem17ALT  29123  ax9lem17  29156  lsatn0  29189  l1cvpat  29244  leat2  29484  atnle  29507  cvlcvr1  29529  cvrexchlem  29608  cvratlem  29610  cvrat  29611  atcvrj0  29617  atle  29625  snatpsubN  29939  linepsubN  29941  pmapsub  29957  lneq2at  29967  lncvrelatN  29970  2llnma3r  29977  cdlemblem  29982  paddasslem5  30013  poml4N  30142  lhpmcvr4N  30215  trlval2  30352  cdlemd6  30392  cdleme7ga  30437  cdleme25b  30543  cdleme29b  30564  cdleme35fnpq  30638  cdleme50f1  30732  cdlemf1  30750  cdlemg27b  30885  cdlemk28-3  31097  tendospcanN  31213  diaf11N  31239  dia2dimlem1  31254  dibf11N  31351  dihf11  31457  dihmeetlem1N  31480  dochvalr  31547  dochnel2  31582  dvh4dimlem  31633  dochsat0  31647  mapd1o  31838  hdmapf1oN  32058  hgmapval0  32085  hgmapf1oN  32096  hlhilhillem  32153
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