MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  biimpd 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  1621  spfw  1698  spw  1701  cbvalw  1708  cbvalvw  1709  alcomiw  1711  19.9d  1790  19.23t  1808  dvelimvOLD  1985  dral1  2004  cbval  2019  chvar  2021  spv  2032  sbequi  2092  dral1-o  2188  2eu3  2320  eqrdav  2386  cleqh  2484  ralcom2  2815  ceqsalg  2923  vtoclf  2948  vtocl2  2950  vtocl3  2951  spcdv  2977  rspcdv  2998  elabgt  3022  sbeqalb  3156  eqrd  3309  ssunsn2  3901  euotd  4398  sotr2  4473  onmindif  4611  elpwunsn  4697  onint  4715  oneqmin  4725  ordunisuc2  4764  tfindsg  4780  findsg  4812  relop  4963  elres  5121  elimasni  5171  sotri2  5203  relcnvtr  5329  iotaval  5369  dffv2  5735  mpteqb  5758  chfnrn  5780  elpreima  5789  iinpreima  5799  exfo  5826  ffnfv  5833  f1elima  5948  f1eqcocnv  5967  fliftfun  5973  soisores  5986  isotr  5995  isomin  5996  f1oweALT  6013  ovmpt2dv2  6146  smoiso  6560  seqomlem2  6644  oaordi  6725  oawordri  6729  oaordex  6737  oalimcl  6739  omwordi  6750  oewordi  6770  oelim2  6774  nnmwordi  6814  xpider  6911  iiner  6912  undifixp  7034  mptelixpg  7035  dom2lem  7083  nneneq  7226  fineqvlem  7259  pssnn  7263  dif1enOLD  7276  dif1en  7277  findcard2s  7285  unfilem2  7308  xpfi  7314  domunfican  7315  dffi2  7363  wemaplem2  7449  suc11reg  7507  noinfep  7547  cantnflem1  7578  r1fin  7632  tcrank  7741  cardlim  7792  pr2nelem  7821  fseqenlem1  7838  alephnbtwn  7885  alephord2i  7891  alephf1  7899  cardaleph  7903  alephiso  7912  dfac12lem2  7957  ackbij1lem16  8048  cflm  8063  cfcoflem  8085  sornom  8090  fin23lem27  8141  isf32lem7  8172  fin17  8207  fin1a2lem2  8214  fin1a2lem4  8216  fin1a2lem6  8218  fin1a2lem9  8221  axdc3lem2  8264  zorn2lem7  8315  uniimadom  8352  inar1  8583  grothomex  8637  addcanpi  8709  mulcanpi  8710  enqer  8731  genpcd  8816  genpnmax  8817  ltexprlem4  8849  reclem3pr  8859  reclem4pr  8860  suplem2pr  8863  axpre-ltadd  8975  axpre-sup  8977  ltletr  9099  00id  9173  mul0or  9594  prodgt02  9788  prodge02  9790  lemul1a  9796  mulgt1  9801  divgt0  9810  divge0  9811  ledivp1i  9868  ltdivp1i  9869  cju  9928  nnsub  9970  nominpos  10136  nn0n0n1ge2  10212  btwnnz  10278  uzindOLD  10296  ublbneg  10492  zmax  10503  cnref1o  10539  ltsubrp  10575  ltaddrp  10576  xrltletr  10679  qbtwnre  10717  xltnegi  10734  iccsupr  10929  icoshft  10951  difreicc  10960  iccshftri  10963  iccshftli  10965  iccdili  10967  icccntri  10969  fzen  11004  fzm1  11057  injresinjlem  11126  injresinj  11127  flval2  11148  flval3  11149  fseqsupubi  11244  sq01  11428  hashf1rn  11563  hashle00  11596  hashgt12el  11609  hashgt12el2  11610  hash2pr  11614  hash2prb  11616  hashtpg  11618  ccatopth2  11704  cjre  11871  o1lo1  12258  o1of2  12333  o1rlimmul  12339  zsum  12439  reeff1  12648  dvds2lem  12789  muldvds1  12801  dvdscmulr  12805  dvdsmulcr  12806  divalglem8  12847  ndvdsadd  12855  gcdmultiple  12977  isprm6  13036  isprm5  13039  prmdvdsexpr  13043  divgcdodd  13046  phiprmpw  13092  pythagtriplem4  13120  pcz  13181  1arith  13222  divsfval  13699  fthmon  14051  setcmon  14169  setcepi  14170  pltnle  14350  pltval3  14351  lubid  14366  latasym  14411  odupos  14489  mrelatglb  14537  mrelatlub  14539  cnvpsb  14572  isgrpid2  14768  ghmf1  14961  orbsta  15017  resscntz  15057  mndodcongi  15108  odf1  15125  lsmss1  15225  lsmss2  15227  efgredeu  15311  lt6abl  15431  ablfaclem3  15572  lspsneq  16121  lspsneu  16122  lsmcv  16140  lidldvgen  16253  domnmuln0  16285  opprdomn  16288  ply1scln0  16609  domnchr  16736  znf1o  16755  zntoslem  16760  znfld  16764  cygznlem2a  16771  cygznlem3  16773  0ntr  17058  islpi  17135  lmss  17284  cmpcld  17387  cmpfi  17393  1stcelcls  17445  ptcnplem  17574  qtophmeo  17770  fbdmn0  17787  fbasrn  17837  elfm3  17903  fmfnfmlem4  17910  fclscf  17978  cnpfcf  17994  alexsubALTlem3  18001  tsmsres  18094  blval2  18482  nmoleub  18636  nmhmcn  18999  iscau4  19103  caussi  19121  cniccbdd  19225  ovoliunnul  19270  mbfinf  19424  itg2splitlem  19507  dvcn  19674  c1lip1  19748  c1lip3  19750  dvcnvrelem1  19768  ply1divex  19926  quotcan  20093  aannenlem1  20112  taylf  20144  ulmcaulem  20177  ulmcau  20178  reeff1o  20230  logccv  20421  logreclem  20527  isosctrlem2  20530  xrlimcnp  20674  rlimcxp  20679  ftalem7  20728  vmappw  20766  fsumvma  20864  dchreq  20909  dchrptlem1  20915  dchrsum  20920  bposlem7  20941  lgsqrlem2  20993  lgsdchr  20999  lgseisenlem2  21001  lgsquad2  21011  2sqlem6  21020  uhgraeq12d  21209  usgraeq12d  21252  usgranloop  21265  nbusgra  21306  nbgraf1olem5  21321  iscusgra0  21332  cusgrasize2inds  21352  cusgrafilem3  21356  usgramaxsize  21362  wlkonprop  21396  trlonprop  21406  0wlkon  21411  usgrnloop  21419  pthonprop  21431  redwlk  21454  wlkdvspthlem  21455  fargshiftfv  21470  gxid  21709  opidon  21758  opidon2  21760  grpomndo  21782  elghomlem2  21798  rngoueqz  21866  dvrunz  21869  rngoridfz  21871  hlipgt0  22264  ocin  22646  ocnel  22648  shmodsi  22739  pjmf1  23066  unopf1o  23267  staddi  23597  stadd3i  23599  mdi  23646  dmdmd  23651  dmdi  23653  dmdbr2  23654  dmdbr3  23656  dmdbr4  23657  dmdi4  23658  mdsl1i  23672  superpos  23705  cvbr4i  23718  atssma  23729  atcv1  23731  atomli  23733  chirredlem1  23741  addltmulALT  23797  bian1d  23798  ifeqeqx  23845  tpr2rico  24114  xrge0iifiso  24125  qqhcn  24174  qqhucn  24175  esumlub  24248  esumpinfval  24259  esumpinfsum  24263  ballotlemfc0  24529  ballotlemfcc  24530  erdsze2lem2  24669  zprod  25042  trpredrec  25265  poseq  25277  soseq  25278  sltval2  25334  sltres  25342  nodenselem7  25365  nodenselem8  25366  nodense  25367  nobndup  25378  nobnddown  25379  nofulllem5  25384  dfrdg4  25513  altopthsn  25520  brbtwn  25552  brcgr  25553  axcgrid  25569  axeuclidlem  25615  axeuclid  25616  btwncomim  25661  btwnexch3  25668  btwnexch2  25671  endofsegid  25733  onsuct0  25905  ordcmp  25911  nndivsub  25921  ltflcei  25950  dvreasin  25980  areacirclem2  25982  areacirclem3  25983  areacirclem5  25986  areacirc  25988  opnrebl2  26015  nn0prpwlem  26016  comppfsc  26078  brabg2  26108  fzmul  26135  fdc  26140  incsequz2  26144  isbnd2  26183  divrngidl  26329  rexrabdioph  26545  fphpdo  26569  icodiamlt  26574  irrapxlem3  26578  rmxypairf1o  26665  rmxycomplete  26671  zindbi  26700  lermxnn0  26706  ltrmy  26708  rmyeq0  26709  rmyeq  26710  lermy  26711  acongsym  26732  acongneg2  26733  wepwsolem  26807  expgrowthi  27219  ordpss  27322  climinf  27400  stoweidlem7  27424  stoweidlem62  27479  2reu3  27634  ralbinrald  27645  funressnfv  27661  afv0fv0  27682  afv0nbfvbi  27684  afvfv0bi  27685  fnbrafvb  27687  afvres  27705  tz6.12-afv  27706  afvco2  27709  ndmaovcl  27736  frgranbnb  27773  frgrancvvdeqlem3  27784  frgrancvvdeqlem4  27785  frgrancvvdeqlem7  27788  frgrawopreglem2  27797  frgrawopreg  27801  bi23impib  27914  bi23imp13  27920  bitr3  27936  rspsbc2  27961  tratrb  27963  sbcim2g  27966  truniALT  27969  3impcombi  28270  tpid3gVD  28295  orbi1rVD  28301  sbc3orgVD  28304  rspsbc2VD  28308  tratrbVD  28314  sbcim2gVD  28328  sbcbiVD  28329  truniALTVD  28331  trintALTVD  28333  trintALT  28334  csbingVD  28337  csbsngVD  28346  csbxpgVD  28347  csbresgVD  28348  csbrngVD  28349  csbima12gALTVD  28350  csbunigVD  28351  csbfv12gALTVD  28352  relopabVD  28354  bnj517  28594  dvelimvNEW7  28800  dral1NEW7  28831  cbvalwwAUX7  28855  sbequiNEW7  28914  chvarNEW7  28953  spvNEW7  28956  cbvalOLD7  29041  lsatn0  29114  l1cvpat  29169  leat2  29409  atnle  29432  cvlcvr1  29454  cvrexchlem  29533  cvratlem  29535  cvrat  29536  atcvrj0  29542  atle  29550  snatpsubN  29864  linepsubN  29866  pmapsub  29882  lneq2at  29892  lncvrelatN  29895  2llnma3r  29902  cdlemblem  29907  paddasslem5  29938  poml4N  30067  lhpmcvr4N  30140  trlval2  30277  cdlemd6  30317  cdleme7ga  30362  cdleme25b  30468  cdleme29b  30489  cdleme35fnpq  30563  cdleme50f1  30657  cdlemf1  30675  cdlemg27b  30810  cdlemk28-3  31022  tendospcanN  31138  diaf11N  31164  dia2dimlem1  31179  dibf11N  31276  dihf11  31382  dihmeetlem1N  31405  dochvalr  31472  dochnel2  31507  dvh4dimlem  31558  dochsat0  31572  mapd1o  31763  hdmapf1oN  31983  hgmapval0  32010  hgmapf1oN  32021  hlhilhillem  32078
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