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  1699  spwOLD  1703  cbvalw  1710  cbvalvwOLD  1712  alcomiw  1714  19.9d  1792  19.23t  1814  spimt  1953  spv  1963  dvelimvOLD  1994  dral1OLD  2023  cbval  2037  chvar  2039  sbequi  2108  dral1-o  2204  2eu3  2336  eqrdav  2403  cleqh  2501  ralcom2  2832  ceqsalg  2940  vtoclf  2965  vtocl2  2967  vtocl3  2968  spcdv  2994  rspcdv  3015  elabgt  3039  sbeqalb  3173  eqrd  3326  ssunsn2  3918  euotd  4417  sotr2  4492  onmindif  4630  elpwunsn  4716  onint  4734  oneqmin  4744  ordunisuc2  4783  tfindsg  4799  findsg  4831  relop  4982  elres  5140  elimasni  5190  sotri2  5222  relcnvtr  5348  iotaval  5388  dffv2  5755  mpteqb  5778  chfnrn  5800  elpreima  5809  iinpreima  5819  exfo  5846  ffnfv  5853  f1elima  5968  f1eqcocnv  5987  fliftfun  5993  soisores  6006  isotr  6015  isomin  6016  f1oweALT  6033  ovmpt2dv2  6166  smoiso  6583  seqomlem2  6667  oaordi  6748  oawordri  6752  oaordex  6760  oalimcl  6762  omwordi  6773  oewordi  6793  oelim2  6797  nnmwordi  6837  xpider  6934  iiner  6935  undifixp  7057  mptelixpg  7058  dom2lem  7106  nneneq  7249  fineqvlem  7282  pssnn  7286  dif1enOLD  7299  dif1en  7300  findcard2s  7308  unfilem2  7331  xpfi  7337  domunfican  7338  dffi2  7386  wemaplem2  7472  suc11reg  7530  noinfep  7570  cantnflem1  7601  r1fin  7655  tcrank  7764  cardlim  7815  pr2nelem  7844  fseqenlem1  7861  alephnbtwn  7908  alephord2i  7914  alephf1  7922  cardaleph  7926  alephiso  7935  dfac12lem2  7980  ackbij1lem16  8071  cflm  8086  cfcoflem  8108  sornom  8113  fin23lem27  8164  isf32lem7  8195  fin17  8230  fin1a2lem2  8237  fin1a2lem4  8239  fin1a2lem6  8241  fin1a2lem9  8244  axdc3lem2  8287  zorn2lem7  8338  uniimadom  8375  inar1  8606  grothomex  8660  addcanpi  8732  mulcanpi  8733  enqer  8754  genpcd  8839  genpnmax  8840  ltexprlem4  8872  reclem3pr  8882  reclem4pr  8883  suplem2pr  8886  axpre-ltadd  8998  axpre-sup  9000  ltletr  9122  00id  9197  mul0or  9618  prodgt02  9812  prodge02  9814  lemul1a  9820  mulgt1  9825  divgt0  9834  divge0  9835  ledivp1i  9892  ltdivp1i  9893  cju  9952  nnsub  9994  nominpos  10160  nn0n0n1ge2  10236  btwnnz  10302  uzindOLD  10320  ublbneg  10516  zmax  10527  cnref1o  10563  ltsubrp  10599  ltaddrp  10600  xrltletr  10703  qbtwnre  10741  xltnegi  10758  iccsupr  10953  icoshft  10975  difreicc  10984  iccshftri  10987  iccshftli  10989  iccdili  10991  icccntri  10993  fzen  11028  fzm1  11082  injresinjlem  11154  injresinj  11155  flval2  11176  flval3  11177  fseqsupubi  11272  sq01  11456  hashf1rn  11591  hashle00  11624  hashgt12el  11637  hashgt12el2  11638  hash2pr  11642  hash2prb  11644  hashtpg  11646  ccatopth2  11732  cjre  11899  o1lo1  12286  o1of2  12361  o1rlimmul  12367  zsum  12467  reeff1  12676  dvds2lem  12817  muldvds1  12829  dvdscmulr  12833  dvdsmulcr  12834  divalglem8  12875  ndvdsadd  12883  gcdmultiple  13005  isprm6  13064  isprm5  13067  prmdvdsexpr  13071  divgcdodd  13074  phiprmpw  13120  pythagtriplem4  13148  pcz  13209  1arith  13250  divsfval  13727  fthmon  14079  setcmon  14197  setcepi  14198  pltnle  14378  pltval3  14379  lubid  14394  latasym  14439  odupos  14517  mrelatglb  14565  mrelatlub  14567  cnvpsb  14600  isgrpid2  14796  ghmf1  14989  orbsta  15045  resscntz  15085  mndodcongi  15136  odf1  15153  lsmss1  15253  lsmss2  15255  efgredeu  15339  lt6abl  15459  ablfaclem3  15600  lspsneq  16149  lspsneu  16150  lsmcv  16168  lidldvgen  16281  domnmuln0  16313  opprdomn  16316  ply1scln0  16637  domnchr  16768  znf1o  16787  zntoslem  16792  znfld  16796  cygznlem2a  16803  cygznlem3  16805  0ntr  17090  islpi  17167  lmss  17316  cmpcld  17419  cmpfi  17425  1stcelcls  17477  ptcnplem  17606  qtophmeo  17802  fbdmn0  17819  fbasrn  17869  elfm3  17935  fmfnfmlem4  17942  fclscf  18010  cnpfcf  18026  alexsubALTlem3  18033  tsmsres  18126  blval2  18558  nmoleub  18718  nmhmcn  19081  iscau4  19185  caussi  19203  cniccbdd  19311  ovoliunnul  19356  mbfinf  19510  itg2splitlem  19593  dvcn  19760  c1lip1  19834  c1lip3  19836  dvcnvrelem1  19854  ply1divex  20012  quotcan  20179  aannenlem1  20198  taylf  20230  ulmcaulem  20263  ulmcau  20264  reeff1o  20316  logccv  20507  logreclem  20613  isosctrlem2  20616  xrlimcnp  20760  rlimcxp  20765  ftalem7  20814  vmappw  20852  fsumvma  20950  dchreq  20995  dchrptlem1  21001  dchrsum  21006  bposlem7  21027  lgsqrlem2  21079  lgsdchr  21085  lgseisenlem2  21087  lgsquad2  21097  2sqlem6  21106  uhgraeq12d  21295  usgraeq12d  21338  usgranloopv  21351  nbgraf1olem5  21408  iscusgra0  21419  cusgrasize2inds  21439  cusgrafilem3  21443  usgramaxsize  21449  wlkonprop  21485  trlonprop  21495  0wlkon  21500  usgrnloop  21516  pthonprop  21530  spthonprp  21538  redwlk  21559  wlkdvspthlem  21560  fargshiftfv  21575  gxid  21814  opidon  21863  opidon2  21865  grpomndo  21887  elghomlem2  21903  rngoueqz  21971  dvrunz  21974  rngoridfz  21976  hlipgt0  22369  ocin  22751  ocnel  22753  shmodsi  22844  pjmf1  23171  unopf1o  23372  staddi  23702  stadd3i  23704  mdi  23751  dmdmd  23756  dmdi  23758  dmdbr2  23759  dmdbr3  23761  dmdbr4  23762  dmdi4  23763  mdsl1i  23777  superpos  23810  cvbr4i  23823  atssma  23834  atcv1  23836  atomli  23838  chirredlem1  23846  addltmulALT  23902  bian1d  23903  ifeqeqx  23954  disjxpin  23981  metider  24242  tpr2rico  24263  xrge0iifiso  24274  qqhcn  24328  qqhucn  24329  esumlub  24405  esumpinfval  24416  esumpinfsum  24420  ballotlemfc0  24703  ballotlemfcc  24704  erdsze2lem2  24843  zprod  25216  trpredrec  25455  poseq  25467  soseq  25468  sltval2  25524  sltres  25532  nodenselem7  25555  nodenselem8  25556  nodense  25557  nobndup  25568  nobnddown  25569  nofulllem5  25574  dfrdg4  25703  altopthsn  25710  brbtwn  25742  brcgr  25743  axcgrid  25759  axeuclidlem  25805  axeuclid  25806  btwncomim  25851  btwnexch3  25858  btwnexch2  25861  endofsegid  25923  onsuct0  26095  ordcmp  26101  nndivsub  26111  ltflcei  26140  mblfinlem  26143  mblfinlem2  26144  mblfinlem3  26145  mbfresfi  26152  cnambfre  26154  dvreasin  26179  areacirclem2  26181  areacirclem3  26182  areacirclem5  26185  areacirc  26187  opnrebl2  26214  nn0prpwlem  26215  comppfsc  26277  brabg2  26307  fzmul  26334  fdc  26339  incsequz2  26343  isbnd2  26382  divrngidl  26528  rexrabdioph  26744  fphpdo  26768  icodiamlt  26773  irrapxlem3  26777  rmxypairf1o  26864  rmxycomplete  26870  zindbi  26899  lermxnn0  26905  ltrmy  26907  rmyeq0  26908  rmyeq  26909  lermy  26910  acongsym  26931  acongneg2  26932  wepwsolem  27006  expgrowthi  27418  ordpss  27521  climinf  27599  stoweidlem7  27623  stoweidlem62  27678  2reu3  27833  ralbinrald  27844  funressnfv  27859  afv0fv0  27880  afv0nbfvbi  27882  afvfv0bi  27883  fnbrafvb  27885  afvres  27903  tz6.12-afv  27904  afvco2  27907  ndmaovcl  27934  elfzmlbm  27977  ubmelm1fzo  27987  swrdnd  28001  swrdccatin2  28018  swrdccatin12lem3b  28022  swrdccatin12b  28027  swrdccatin12c  28028  swrdccat3  28029  swrdccat3a  28030  swrdccat3b  28031  usgra2wlkspthlem2  28037  usgra2pth  28041  el2spthonot  28067  usg2wotspth  28081  usg2spthonot  28085  usg2spthonot0  28086  frgranbnb  28124  frgrancvvdeqlem3  28135  frgrancvvdeqlem4  28136  frgrancvvdeqlem7  28139  frgrawopreglem2  28148  frgrawopreg  28152  frgregordn0  28173  bi23impib  28282  bi23imp13  28288  bitr3  28304  rspsbc2  28329  tratrb  28331  sbcim2g  28334  truniALT  28337  3impcombi  28638  tpid3gVD  28663  orbi1rVD  28669  sbc3orgVD  28672  rspsbc2VD  28676  tratrbVD  28682  sbcim2gVD  28696  sbcbiVD  28697  truniALTVD  28699  trintALTVD  28701  trintALT  28702  csbingVD  28705  csbsngVD  28714  csbxpgVD  28715  csbresgVD  28716  csbrngVD  28717  csbima12gALTVD  28718  csbunigVD  28719  csbfv12gALTVD  28720  relopabVD  28722  bnj517  28962  dvelimvNEW7  29168  dral1NEW7  29199  cbvalwwAUX7  29223  sbequiNEW7  29282  chvarNEW7  29321  spvNEW7  29324  cbvalOLD7  29409  lsatn0  29482  l1cvpat  29537  leat2  29777  atnle  29800  cvlcvr1  29822  cvrexchlem  29901  cvratlem  29903  cvrat  29904  atcvrj0  29910  atle  29918  snatpsubN  30232  linepsubN  30234  pmapsub  30250  lneq2at  30260  lncvrelatN  30263  2llnma3r  30270  cdlemblem  30275  paddasslem5  30306  poml4N  30435  lhpmcvr4N  30508  trlval2  30645  cdlemd6  30685  cdleme7ga  30730  cdleme25b  30836  cdleme29b  30857  cdleme35fnpq  30931  cdleme50f1  31025  cdlemf1  31043  cdlemg27b  31178  cdlemk28-3  31390  tendospcanN  31506  diaf11N  31532  dia2dimlem1  31547  dibf11N  31644  dihf11  31750  dihmeetlem1N  31773  dochvalr  31840  dochnel2  31875  dvh4dimlem  31926  dochsat0  31940  mapd1o  32131  hdmapf1oN  32351  hgmapval0  32378  hgmapf1oN  32389  hlhilhillem  32446
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