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

Theorem biimpd 199
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 179 . 2  |-  ( ( ps  <->  ch )  ->  ( ps  ->  ch ) )
31, 2syl 16 1  |-  ( ph  ->  ( ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  mpbid  202  sylibd  206  sylbid  207  mpbidi  208  syl5ib  211  syl6bi  220  ibi  233  con4bid  285  mtbird  293  mtbiri  295  imbi1d  309  pm5.21im  339  biimpa  471  exintr  1624  spfw  1703  spwOLD  1707  cbvalw  1714  cbvalvwOLD  1716  alcomiw  1718  19.9d  1796  19.23t  1818  spimt  1955  spv  1965  chvar  1968  cbval  1982  dvelimvOLD  2028  dral1OLD  2054  sbequiOLD  2137  nfsb4t  2154  dral1-o  2230  2eu3  2362  eqrdav  2434  cleqh  2532  ralcom2  2864  ceqsalg  2972  vtoclf  2997  vtocl2  2999  vtocl3  3000  spcdv  3026  rspcdv  3047  elabgt  3071  sbeqalb  3205  eqrd  3358  ssunsn2  3950  euotd  4449  sotr2  4524  onmindif  4663  elpwunsn  4749  onint  4767  oneqmin  4777  ordunisuc2  4816  tfindsg  4832  findsg  4864  relop  5015  elres  5173  elimasni  5223  sotri2  5255  relcnvtr  5381  iotaval  5421  dffv2  5788  mpteqb  5811  chfnrn  5833  elpreima  5842  iinpreima  5852  exfo  5879  ffnfv  5886  f1elima  6001  f1eqcocnv  6020  fliftfun  6026  soisores  6039  isotr  6048  isomin  6049  f1oweALT  6066  ovmpt2dv2  6199  smoiso  6616  seqomlem2  6700  oaordi  6781  oawordri  6785  oaordex  6793  oalimcl  6795  omwordi  6806  oewordi  6826  oelim2  6830  nnmwordi  6870  xpider  6967  iiner  6968  undifixp  7090  mptelixpg  7091  dom2lem  7139  nneneq  7282  fineqvlem  7315  pssnn  7319  dif1enOLD  7332  dif1en  7333  findcard2s  7341  unfilem2  7364  xpfi  7370  domunfican  7371  dffi2  7420  wemaplem2  7508  suc11reg  7566  noinfep  7606  cantnflem1  7637  r1fin  7691  tcrank  7800  cardlim  7851  pr2nelem  7880  fseqenlem1  7897  alephnbtwn  7944  alephord2i  7950  alephf1  7958  cardaleph  7962  alephiso  7971  dfac12lem2  8016  ackbij1lem16  8107  cflm  8122  cfcoflem  8144  sornom  8149  fin23lem27  8200  isf32lem7  8231  fin17  8266  fin1a2lem2  8273  fin1a2lem4  8275  fin1a2lem6  8277  fin1a2lem9  8280  axdc3lem2  8323  zorn2lem7  8374  uniimadom  8411  inar1  8642  grothomex  8696  addcanpi  8768  mulcanpi  8769  enqer  8790  genpcd  8875  genpnmax  8876  ltexprlem4  8908  reclem3pr  8918  reclem4pr  8919  suplem2pr  8922  axpre-ltadd  9034  axpre-sup  9036  ltletr  9158  00id  9233  mul0or  9654  prodgt02  9848  prodge02  9850  lemul1a  9856  mulgt1  9861  divgt0  9870  divge0  9871  ledivp1i  9928  ltdivp1i  9929  cju  9988  nnsub  10030  nominpos  10196  nn0n0n1ge2  10272  btwnnz  10338  uzindOLD  10356  ublbneg  10552  zmax  10563  cnref1o  10599  ltsubrp  10635  ltaddrp  10636  xrltletr  10739  qbtwnre  10777  xltnegi  10794  iccsupr  10989  icoshft  11011  difreicc  11020  iccshftri  11023  iccshftli  11025  iccdili  11027  icccntri  11029  fzen  11064  fzm1  11119  injresinjlem  11191  injresinj  11192  flval2  11213  flval3  11214  fseqsupubi  11309  sq01  11493  hashf1rn  11628  hashle00  11661  hashgt12el  11674  hashgt12el2  11675  hash2pr  11679  hash2prb  11681  hashtpg  11683  ccatopth2  11769  cjre  11936  o1lo1  12323  o1of2  12398  o1rlimmul  12404  zsum  12504  reeff1  12713  dvds2lem  12854  muldvds1  12866  dvdscmulr  12870  dvdsmulcr  12871  divalglem8  12912  ndvdsadd  12920  gcdmultiple  13042  isprm6  13101  isprm5  13104  prmdvdsexpr  13108  divgcdodd  13111  phiprmpw  13157  pythagtriplem4  13185  pcz  13246  1arith  13287  divsfval  13764  fthmon  14116  setcmon  14234  setcepi  14235  pltnle  14415  pltval3  14416  lubid  14431  latasym  14476  odupos  14554  mrelatglb  14602  mrelatlub  14604  cnvpsb  14637  isgrpid2  14833  ghmf1  15026  orbsta  15082  resscntz  15122  mndodcongi  15173  odf1  15190  lsmss1  15290  lsmss2  15292  efgredeu  15376  lt6abl  15496  ablfaclem3  15637  lspsneq  16186  lspsneu  16187  lsmcv  16205  lidldvgen  16318  domnmuln0  16350  opprdomn  16353  ply1scln0  16674  domnchr  16805  znf1o  16824  zntoslem  16829  znfld  16833  cygznlem2a  16840  cygznlem3  16842  0ntr  17127  islpi  17205  lmss  17354  cmpcld  17457  cmpfi  17463  bwth  17465  1stcelcls  17516  ptcnplem  17645  qtophmeo  17841  fbdmn0  17858  fbasrn  17908  elfm3  17974  fmfnfmlem4  17981  fclscf  18049  cnpfcf  18065  alexsubALTlem3  18072  tsmsres  18165  blval2  18597  nmoleub  18757  nmhmcn  19120  iscau4  19224  caussi  19242  cniccbdd  19350  ovoliunnul  19395  mbfinf  19549  itg2splitlem  19632  dvcn  19799  c1lip1  19873  c1lip3  19875  dvcnvrelem1  19893  ply1divex  20051  quotcan  20218  aannenlem1  20237  taylf  20269  ulmcaulem  20302  ulmcau  20303  reeff1o  20355  logccv  20546  logreclem  20652  isosctrlem2  20655  xrlimcnp  20799  rlimcxp  20804  ftalem7  20853  vmappw  20891  fsumvma  20989  dchreq  21034  dchrptlem1  21040  dchrsum  21045  bposlem7  21066  lgsqrlem2  21118  lgsdchr  21124  lgseisenlem2  21126  lgsquad2  21136  2sqlem6  21145  uhgraeq12d  21334  usgraeq12d  21377  usgranloopv  21390  nbgraf1olem5  21447  iscusgra0  21458  cusgrasize2inds  21478  cusgrafilem3  21482  usgramaxsize  21488  wlkonprop  21524  trlonprop  21534  0wlkon  21539  usgrnloop  21555  pthonprop  21569  spthonprp  21577  redwlk  21598  wlkdvspthlem  21599  fargshiftfv  21614  gxid  21853  opidon  21902  opidon2  21904  grpomndo  21926  elghomlem2  21942  rngoueqz  22010  dvrunz  22013  rngoridfz  22015  hlipgt0  22408  ocin  22790  ocnel  22792  shmodsi  22883  pjmf1  23210  unopf1o  23411  staddi  23741  stadd3i  23743  mdi  23790  dmdmd  23795  dmdi  23797  dmdbr2  23798  dmdbr3  23800  dmdbr4  23801  dmdi4  23802  mdsl1i  23816  superpos  23849  cvbr4i  23862  atssma  23873  atcv1  23875  atomli  23877  chirredlem1  23885  addltmulALT  23941  bian1d  23942  ifeqeqx  23993  disjxpin  24020  metider  24281  tpr2rico  24302  xrge0iifiso  24313  qqhcn  24367  qqhucn  24368  esumlub  24444  esumpinfval  24455  esumpinfsum  24459  ballotlemfc0  24742  ballotlemfcc  24743  erdsze2lem2  24882  zprod  25255  trpredrec  25508  poseq  25520  soseq  25521  sltval2  25603  sltres  25611  nodenselem7  25634  nodenselem8  25635  nodense  25636  nobndup  25647  nobnddown  25648  nofulllem5  25653  dfrdg4  25787  altopthsn  25798  brbtwn  25830  brcgr  25831  axcgrid  25847  axeuclidlem  25893  axeuclid  25894  btwncomim  25939  btwnexch3  25946  btwnexch2  25949  endofsegid  26011  onsuct0  26183  ordcmp  26189  nndivsub  26199  ltflcei  26231  mblfinlem  26234  mblfinlem2  26235  mblfinlem3  26236  mbfresfi  26243  cnambfre  26245  ftc1anc  26278  dvreasin  26280  areacirclem2  26282  areacirclem3  26283  areacirclem5  26286  areacirc  26288  opnrebl2  26315  nn0prpwlem  26316  comppfsc  26378  brabg2  26408  fzmul  26435  fdc  26440  incsequz2  26444  isbnd2  26483  divrngidl  26629  rexrabdioph  26845  fphpdo  26869  icodiamlt  26874  irrapxlem3  26878  rmxypairf1o  26965  rmxycomplete  26971  zindbi  27000  lermxnn0  27006  ltrmy  27008  rmyeq0  27009  rmyeq  27010  lermy  27011  acongsym  27032  acongneg2  27033  wepwsolem  27107  expgrowthi  27518  ordpss  27621  climinf  27699  stoweidlem7  27723  stoweidlem62  27778  2reu3  27933  ralbinrald  27944  funressnfv  27959  afv0fv0  27980  afv0nbfvbi  27982  afvfv0bi  27983  fnbrafvb  27985  afvres  28003  tz6.12-afv  28004  afvco2  28007  ndmaovcl  28034  elfzmlbm  28090  ubmelm1fzo  28110  subsubelfzo0  28118  swrdnd  28154  swrdccatin2  28176  swrdccat  28182  swrdccat3a  28183  swrdccat3blem  28184  modprm0  28194  2cshw1lem1  28214  2cshw1lem2  28215  2cshw2lem3  28220  2cshwmod  28223  cshweqrep  28237  cshw1  28238  cshwssizelem1a  28242  cshwssizesame  28251  usgra2wlkspthlem2  28260  usgra2pth  28264  el2spthonot  28290  usg2wotspth  28304  usg2spthonot  28308  usg2spthonot0  28309  frgranbnb  28347  frgrancvvdeqlem3  28358  frgrancvvdeqlem4  28359  frgrancvvdeqlem7  28362  frgrawopreglem2  28371  frgrawopreg  28375  frgregordn0  28396  bi23impib  28505  bi23imp13  28511  bitr3  28530  rspsbc2  28555  tratrb  28557  sbcim2g  28560  truniALT  28563  3impcombi  28866  tpid3gVD  28891  orbi1rVD  28897  sbc3orgVD  28900  rspsbc2VD  28904  tratrbVD  28910  sbcim2gVD  28924  sbcbiVD  28925  truniALTVD  28927  trintALTVD  28929  trintALT  28930  csbingVD  28933  csbsngVD  28942  csbxpgVD  28943  csbresgVD  28944  csbrngVD  28945  csbima12gALTVD  28946  csbunigVD  28947  csbfv12gALTVD  28948  relopabVD  28950  isosctrlem1ALT  28983  bnj517  29193  dvelimvNEW7  29399  dral1NEW7  29430  cbvalwwAUX7  29456  sbequiNEW7  29516  chvarNEW7  29557  spvNEW7  29560  ax7w15AUX7  29605  ax7w14AUX7  29607  cbvalOLD7  29662  lsatn0  29734  l1cvpat  29789  leat2  30029  atnle  30052  cvlcvr1  30074  cvrexchlem  30153  cvratlem  30155  cvrat  30156  atcvrj0  30162  atle  30170  snatpsubN  30484  linepsubN  30486  pmapsub  30502  lneq2at  30512  lncvrelatN  30515  2llnma3r  30522  cdlemblem  30527  paddasslem5  30558  poml4N  30687  lhpmcvr4N  30760  trlval2  30897  cdlemd6  30937  cdleme7ga  30982  cdleme25b  31088  cdleme29b  31109  cdleme35fnpq  31183  cdleme50f1  31277  cdlemf1  31295  cdlemg27b  31430  cdlemk28-3  31642  tendospcanN  31758  diaf11N  31784  dia2dimlem1  31799  dibf11N  31896  dihf11  32002  dihmeetlem1N  32025  dochvalr  32092  dochnel2  32127  dvh4dimlem  32178  dochsat0  32192  mapd1o  32383  hdmapf1oN  32603  hgmapval0  32630  hgmapf1oN  32641  hlhilhillem  32698
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 178
  Copyright terms: Public domain W3C validator