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

Theorem biimpd 200
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 180 . 2  |-  ( ( ps  <->  ch )  ->  ( ps  ->  ch ) )
31, 2syl 16 1  |-  ( ph  ->  ( ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178
This theorem is referenced by:  mpbid  203  sylibd  207  sylbid  208  mpbidi  209  syl5ib  212  syl6bi  221  ibi  234  con4bid  286  mtbird  294  mtbiri  296  imbi1d  310  pm5.21im  340  biimpa  472  exintr  1625  spfw  1704  spwOLD  1708  cbvalw  1715  cbvalvwOLD  1717  alcomiw  1719  19.9d  1797  19.23t  1819  spimt  1956  spv  1966  chvar  1969  cbval  1983  dvelimvOLD  2029  dral1OLD  2059  sbequiOLD  2116  nfsb4t  2129  dral1-o  2233  2eu3  2365  eqrdav  2437  cleqh  2535  ralcom2  2874  ceqsalg  2982  vtoclf  3007  vtocl2  3009  vtocl3  3010  spcdv  3036  rspcdv  3057  elabgt  3081  sbeqalb  3215  eqrd  3368  ssunsn2  3960  euotd  4459  sotr2  4534  onmindif  4673  elpwunsn  4759  onint  4777  oneqmin  4787  ordunisuc2  4826  tfindsg  4842  findsg  4874  relop  5025  elres  5183  elimasni  5233  sotri2  5265  relcnvtr  5391  iotaval  5431  dffv2  5798  mpteqb  5821  chfnrn  5843  elpreima  5852  iinpreima  5862  exfo  5889  ffnfv  5896  f1elima  6011  f1eqcocnv  6030  fliftfun  6036  soisores  6049  isotr  6058  isomin  6059  f1oweALT  6076  ovmpt2dv2  6209  smoiso  6626  seqomlem2  6710  oaordi  6791  oawordri  6795  oaordex  6803  oalimcl  6805  omwordi  6816  oewordi  6836  oelim2  6840  nnmwordi  6880  xpider  6977  iiner  6978  undifixp  7100  mptelixpg  7101  dom2lem  7149  nneneq  7292  fineqvlem  7325  pssnn  7329  dif1enOLD  7342  dif1en  7343  findcard2s  7351  unfilem2  7374  xpfi  7380  domunfican  7381  dffi2  7430  wemaplem2  7518  suc11reg  7576  noinfep  7616  cantnflem1  7647  r1fin  7701  tcrank  7810  cardlim  7861  pr2nelem  7890  fseqenlem1  7907  alephnbtwn  7954  alephord2i  7960  alephf1  7968  cardaleph  7972  alephiso  7981  dfac12lem2  8026  ackbij1lem16  8117  cflm  8132  cfcoflem  8154  sornom  8159  fin23lem27  8210  isf32lem7  8241  fin17  8276  fin1a2lem2  8283  fin1a2lem4  8285  fin1a2lem6  8287  fin1a2lem9  8290  axdc3lem2  8333  zorn2lem7  8384  uniimadom  8421  inar1  8652  grothomex  8706  addcanpi  8778  mulcanpi  8779  enqer  8800  genpcd  8885  genpnmax  8886  ltexprlem4  8918  reclem3pr  8928  reclem4pr  8929  suplem2pr  8932  axpre-ltadd  9044  axpre-sup  9046  ltletr  9168  00id  9243  mul0or  9664  prodgt02  9858  prodge02  9860  lemul1a  9866  mulgt1  9871  divgt0  9880  divge0  9881  ledivp1i  9938  ltdivp1i  9939  cju  9998  nnsub  10040  nominpos  10206  nn0n0n1ge2  10282  btwnnz  10348  uzindOLD  10366  ublbneg  10562  zmax  10573  cnref1o  10609  ltsubrp  10645  ltaddrp  10646  xrltletr  10749  qbtwnre  10787  xltnegi  10804  iccsupr  10999  icoshft  11021  difreicc  11030  iccshftri  11033  iccshftli  11035  iccdili  11037  icccntri  11039  fzen  11074  fzm1  11129  injresinjlem  11201  injresinj  11202  flval2  11223  flval3  11224  fseqsupubi  11319  sq01  11503  hashf1rn  11638  hashle00  11671  hashgt12el  11684  hashgt12el2  11685  hash2pr  11689  hash2prb  11691  hashtpg  11693  ccatopth2  11779  cjre  11946  o1lo1  12333  o1of2  12408  o1rlimmul  12414  zsum  12514  reeff1  12723  dvds2lem  12864  muldvds1  12876  dvdscmulr  12880  dvdsmulcr  12881  divalglem8  12922  ndvdsadd  12930  gcdmultiple  13052  isprm6  13111  isprm5  13114  prmdvdsexpr  13118  divgcdodd  13121  phiprmpw  13167  pythagtriplem4  13195  pcz  13256  1arith  13297  divsfval  13774  fthmon  14126  setcmon  14244  setcepi  14245  pltnle  14425  pltval3  14426  lubid  14441  latasym  14486  odupos  14564  mrelatglb  14612  mrelatlub  14614  cnvpsb  14647  isgrpid2  14843  ghmf1  15036  orbsta  15092  resscntz  15132  mndodcongi  15183  odf1  15200  lsmss1  15300  lsmss2  15302  efgredeu  15386  lt6abl  15506  ablfaclem3  15647  lspsneq  16196  lspsneu  16197  lsmcv  16215  lidldvgen  16328  domnmuln0  16360  opprdomn  16363  ply1scln0  16684  domnchr  16815  znf1o  16834  zntoslem  16839  znfld  16843  cygznlem2a  16850  cygznlem3  16852  0ntr  17137  islpi  17215  lmss  17364  cmpcld  17467  cmpfi  17473  bwth  17475  1stcelcls  17526  ptcnplem  17655  qtophmeo  17851  fbdmn0  17868  fbasrn  17918  elfm3  17984  fmfnfmlem4  17991  fclscf  18059  cnpfcf  18075  alexsubALTlem3  18082  tsmsres  18175  blval2  18607  nmoleub  18767  nmhmcn  19130  iscau4  19234  caussi  19252  cniccbdd  19360  ovoliunnul  19405  mbfinf  19559  itg2splitlem  19642  dvcn  19809  c1lip1  19883  c1lip3  19885  dvcnvrelem1  19903  ply1divex  20061  quotcan  20228  aannenlem1  20247  taylf  20279  ulmcaulem  20312  ulmcau  20313  reeff1o  20365  logccv  20556  logreclem  20662  isosctrlem2  20665  xrlimcnp  20809  rlimcxp  20814  ftalem7  20863  vmappw  20901  fsumvma  20999  dchreq  21044  dchrptlem1  21050  dchrsum  21055  bposlem7  21076  lgsqrlem2  21128  lgsdchr  21134  lgseisenlem2  21136  lgsquad2  21146  2sqlem6  21155  uhgraeq12d  21344  usgraeq12d  21387  usgranloopv  21400  nbgraf1olem5  21457  iscusgra0  21468  cusgrasize2inds  21488  cusgrafilem3  21492  usgramaxsize  21498  wlkonprop  21534  trlonprop  21544  0wlkon  21549  usgrnloop  21565  pthonprop  21579  spthonprp  21587  redwlk  21608  wlkdvspthlem  21609  fargshiftfv  21624  gxid  21863  opidon  21912  opidon2  21914  grpomndo  21936  elghomlem2  21952  rngoueqz  22020  dvrunz  22023  rngoridfz  22025  hlipgt0  22418  ocin  22800  ocnel  22802  shmodsi  22893  pjmf1  23220  unopf1o  23421  staddi  23751  stadd3i  23753  mdi  23800  dmdmd  23805  dmdi  23807  dmdbr2  23808  dmdbr3  23810  dmdbr4  23811  dmdi4  23812  mdsl1i  23826  superpos  23859  cvbr4i  23872  atssma  23883  atcv1  23885  atomli  23887  chirredlem1  23895  addltmulALT  23951  bian1d  23952  ifeqeqx  24003  disjxpin  24030  metider  24291  tpr2rico  24312  xrge0iifiso  24323  qqhcn  24377  qqhucn  24378  esumlub  24454  esumpinfval  24465  esumpinfsum  24469  ballotlemfc0  24752  ballotlemfcc  24753  erdsze2lem2  24892  zprod  25265  trpredrec  25518  poseq  25530  soseq  25531  sltval2  25613  sltres  25621  nodenselem7  25644  nodenselem8  25645  nodense  25646  nobndup  25657  nobnddown  25658  nofulllem5  25663  dfrdg4  25797  altopthsn  25808  brbtwn  25840  brcgr  25841  axcgrid  25857  axeuclidlem  25903  axeuclid  25904  btwncomim  25949  btwnexch3  25956  btwnexch2  25959  endofsegid  26021  onsuct0  26193  ordcmp  26199  nndivsub  26209  ltflcei  26241  mblfinlem1  26245  mblfinlem2  26246  mblfinlem3  26247  mblfinlem4  26248  mbfresfi  26255  cnambfre  26257  ftc1anc  26290  dvreasin  26292  areacirclem1  26294  areacirclem4  26297  areacirc  26299  opnrebl2  26326  nn0prpwlem  26327  comppfsc  26389  brabg2  26419  fzmul  26446  fdc  26451  incsequz2  26455  isbnd2  26494  divrngidl  26640  rexrabdioph  26856  fphpdo  26880  icodiamlt  26885  irrapxlem3  26889  rmxypairf1o  26976  rmxycomplete  26982  zindbi  27011  lermxnn0  27017  ltrmy  27019  rmyeq0  27020  rmyeq  27021  lermy  27022  acongsym  27043  acongneg2  27044  wepwsolem  27118  expgrowthi  27529  ordpss  27632  climinf  27710  stoweidlem7  27734  stoweidlem62  27789  2reu3  27944  ralbinrald  27955  funressnfv  27970  afv0fv0  27991  afv0nbfvbi  27993  afvfv0bi  27994  fnbrafvb  27996  afvres  28014  tz6.12-afv  28015  afvco2  28018  ndmaovcl  28045  elovmpt3rab  28096  elfzmlbm  28117  ubmelm1fzo  28138  subsubelfzo0  28146  fzofzim  28147  2ffzoeq  28151  elovmptnn0wrd  28202  swrdnd  28204  swrdtrcfv0  28217  swdeq  28218  swrdccatin2  28232  swrdccat  28238  swrdccat3a  28239  swrdccat3blem  28240  modprm0  28250  2cshw1lem1  28270  2cshw1lem2  28271  2cshw2lem3  28276  2cshwmod  28279  swrdtrcfvl  28287  cshweqrep  28296  cshw1  28297  cshwssizelem1a  28301  cshwssizesame  28310  iswlkg  28326  wlkcompim  28328  usg2wlkeq  28330  usgra2wlkspthlem2  28333  usgra2pth  28337  wwlknimp  28357  el2spthonot  28390  usg2wotspth  28404  usg2spthonot  28408  usg2spthonot0  28409  rgraprop  28431  rusgraprop  28432  frgranbnb  28472  frgrancvvdeqlem3  28483  frgrancvvdeqlem4  28484  frgrancvvdeqlem7  28487  frgrawopreglem2  28496  frgrawopreg  28500  frgregordn0  28521  bi23impib  28630  bi23imp13  28636  bitr3  28655  rspsbc2  28680  tratrb  28682  sbcim2g  28685  truniALT  28688  3impcombi  28991  tpid3gVD  29016  orbi1rVD  29022  sbc3orgVD  29025  rspsbc2VD  29029  tratrbVD  29035  sbcim2gVD  29049  sbcbiVD  29050  truniALTVD  29052  trintALTVD  29054  trintALT  29055  csbingVD  29058  csbsngVD  29067  csbxpgVD  29068  csbresgVD  29069  csbrngVD  29070  csbima12gALTVD  29071  csbunigVD  29072  csbfv12gALTVD  29073  relopabVD  29075  isosctrlem1ALT  29108  bnj517  29318  dvelimvNEW7  29524  dral1NEW7  29555  cbvalwwAUX7  29581  sbequiNEW7  29641  chvarNEW7  29682  spvNEW7  29685  ax7w15AUX7  29730  ax7w14AUX7  29732  cbvalOLD7  29787  lsatn0  29859  l1cvpat  29914  leat2  30154  atnle  30177  cvlcvr1  30199  cvrexchlem  30278  cvratlem  30280  cvrat  30281  atcvrj0  30287  atle  30295  snatpsubN  30609  linepsubN  30611  pmapsub  30627  lneq2at  30637  lncvrelatN  30640  2llnma3r  30647  cdlemblem  30652  paddasslem5  30683  poml4N  30812  lhpmcvr4N  30885  trlval2  31022  cdlemd6  31062  cdleme7ga  31107  cdleme25b  31213  cdleme29b  31234  cdleme35fnpq  31308  cdleme50f1  31402  cdlemf1  31420  cdlemg27b  31555  cdlemk28-3  31767  tendospcanN  31883  diaf11N  31909  dia2dimlem1  31924  dibf11N  32021  dihf11  32127  dihmeetlem1N  32150  dochvalr  32217  dochnel2  32252  dvh4dimlem  32303  dochsat0  32317  mapd1o  32508  hdmapf1oN  32728  hgmapval0  32755  hgmapf1oN  32766  hlhilhillem  32823
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 179
  Copyright terms: Public domain W3C validator