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  1603  spfw  1659  spw  1662  cbvalw  1677  cbvalvw  1678  alcomiw  1680  19.9d  1786  dvelimv  1881  dral1  1907  cbval  1926  chvar  1928  spv  1940  sbequi  2001  dral1-o  2095  2eu3  2227  eqrdav  2284  cleqh  2382  ralcom2  2706  ceqsalg  2814  vtoclf  2839  vtocl2  2841  vtocl3  2842  spcdv  2868  rspcdv  2889  elabgt  2913  sbeqalb  3045  ssunsn2  3775  euotd  4269  sotr2  4345  onmindif  4484  elpwunsn  4570  onint  4588  oneqmin  4598  ordunisuc2  4637  tfindsg  4653  findsg  4685  relop  4836  elres  4992  elimasni  5042  sotri2  5074  relcnvtr  5194  iotaval  5232  tz6.12-1  5546  dffv2  5594  mpteqb  5616  chfnrn  5638  elpreima  5647  iinpreima  5657  exfo  5680  ffnfv  5687  f1elima  5789  f1eqcocnv  5807  fliftfun  5813  soisores  5826  isotr  5835  isomin  5836  f1oweALT  5853  ovmpt2dv2  5983  smoiso  6381  seqomlem2  6465  oaordi  6546  oawordri  6550  oaordex  6558  oalimcl  6560  omwordi  6571  oewordi  6591  oelim2  6595  nnmwordi  6635  xpider  6732  iiner  6733  undifixp  6854  mptelixpg  6855  dom2lem  6903  nneneq  7046  fineqvlem  7079  pssnn  7083  dif1enOLD  7092  dif1en  7093  findcard2s  7101  unfilem2  7124  xpfi  7130  domunfican  7131  dffi2  7178  wemaplem2  7264  suc11reg  7322  noinfep  7362  cantnflem1  7393  r1fin  7447  tcrank  7556  cardlim  7607  pr2nelem  7636  fseqenlem1  7653  alephnbtwn  7700  alephord2i  7706  alephf1  7714  cardaleph  7718  alephiso  7727  dfac12lem2  7772  ackbij1lem16  7863  cflm  7878  cfcoflem  7900  sornom  7905  fin23lem27  7956  isf32lem7  7987  fin17  8022  fin1a2lem2  8029  fin1a2lem4  8031  fin1a2lem6  8033  fin1a2lem9  8036  axdc3lem2  8079  zorn2lem7  8131  uniimadom  8168  inar1  8399  grothomex  8453  addcanpi  8525  mulcanpi  8526  enqer  8547  genpcd  8632  genpnmax  8633  ltexprlem4  8665  reclem3pr  8675  reclem4pr  8676  suplem2pr  8679  axpre-ltadd  8791  axpre-sup  8793  ltletr  8915  00id  8989  mul0or  9410  prodgt02  9604  prodge02  9606  lemul1a  9612  mulgt1  9617  divgt0  9626  divge0  9627  ledivp1i  9684  ltdivp1i  9685  cju  9744  nnsub  9786  nominpos  9950  btwnnz  10090  uzindOLD  10108  ublbneg  10304  zmax  10315  cnref1o  10351  ltsubrp  10387  ltaddrp  10388  xrltletr  10490  qbtwnre  10528  xltnegi  10545  iccsupr  10738  icoshft  10760  difreicc  10769  iccshftri  10772  iccshftli  10774  iccdili  10776  icccntri  10778  fzen  10813  fzm1  10864  flval2  10946  flval3  10947  fseqsupubi  11042  sq01  11225  ccatopth2  11465  cjre  11626  o1lo1  12013  o1of2  12088  o1rlimmul  12094  zsum  12193  reeff1  12402  dvds2lem  12543  muldvds1  12555  dvdscmulr  12559  dvdsmulcr  12560  divalglem8  12601  ndvdsadd  12609  gcdmultiple  12731  isprm6  12790  isprm5  12793  prmdvdsexpr  12797  divgcdodd  12800  phiprmpw  12846  pythagtriplem4  12874  pcz  12935  1arith  12976  divsfval  13451  fthmon  13803  setcmon  13921  setcepi  13922  pltnle  14102  pltval3  14103  lubid  14118  latasym  14163  odupos  14241  mrelatglb  14289  mrelatlub  14291  cnvpsb  14324  isgrpid2  14520  ghmf1  14713  orbsta  14769  resscntz  14809  mndodcongi  14860  odf1  14877  lsmss1  14977  lsmss2  14979  efgredeu  15063  lt6abl  15183  ablfaclem3  15324  lspsneq  15877  lspsneu  15878  lsmcv  15896  lidldvgen  16009  domnmuln0  16041  opprdomn  16044  ply1scln0  16368  domnchr  16488  znf1o  16507  zntoslem  16512  znfld  16516  cygznlem2a  16523  cygznlem3  16525  0ntr  16810  islpi  16882  lmss  17028  cmpcld  17131  cmpfi  17137  1stcelcls  17189  ptcnplem  17317  qtophmeo  17510  fbdmn0  17531  fbasrn  17581  elfm3  17647  fmfnfmlem4  17654  fclscf  17722  cnpfcf  17738  alexsubALTlem3  17745  tsmsres  17828  nmoleub  18242  nmhmcn  18603  iscau4  18707  caussi  18725  cniccbdd  18823  ovoliunnul  18868  mbfinf  19022  itg2splitlem  19105  dvcn  19272  c1lip1  19346  c1lip3  19348  dvcnvrelem1  19366  ply1divex  19524  quotcan  19691  aannenlem1  19710  taylf  19742  ulmcaulem  19773  ulmcau  19774  reeff1o  19825  logccv  20012  logreclem  20118  isosctrlem2  20121  xrlimcnp  20265  rlimcxp  20270  ftalem7  20318  vmappw  20356  fsumvma  20454  dchreq  20499  dchrptlem1  20505  dchrsum  20510  bposlem7  20531  lgsqrlem2  20583  lgsdchr  20589  lgseisenlem2  20591  lgsquad2  20601  2sqlem6  20610  gxid  20942  opidon  20991  opidon2  20993  grpomndo  21015  elghomlem2  21031  rngoueqz  21099  dvrunz  21102  hlipgt0  21495  ocin  21877  ocnel  21879  shmodsi  21970  pjmf1  22297  unopf1o  22498  staddi  22828  stadd3i  22830  mdi  22877  dmdmd  22882  dmdi  22884  dmdbr2  22885  dmdbr3  22887  dmdbr4  22888  dmdi4  22889  mdsl1i  22903  superpos  22936  cvbr4i  22949  atssma  22960  atcv1  22962  atomli  22964  chirredlem1  22972  addltmulALT  23028  ifeqeqx  23036  elabreximd  23041  ballotlemfc0  23053  ballotlemfcc  23054  ballotlemsgt1  23071  ballotlemsel1i  23073  ballotlemfrceq  23089  ballotlemfrcn0  23090  ballotlemirc  23092  bian1d  23124  eqrd  23128  cnre2csqlem  23296  tpr2rico  23298  xrsinvgval  23308  xrge0iifiso  23319  xrge0addass  23331  ctex  23338  disjdsct  23371  lmxrge0  23377  esumpinfval  23443  esumpinfsum  23447  esumpcvgval  23448  mbfmf  23562  mbfmcnt  23575  erdsze2lem2  23737  trpredrec  24243  poseq  24255  soseq  24256  sltval2  24312  sltres  24320  nodenselem7  24343  nodenselem8  24344  nodense  24345  nobndup  24356  nobnddown  24357  nofulllem5  24362  dfrdg4  24490  altopthsn  24497  brbtwn  24529  brcgr  24530  axcgrid  24546  axeuclidlem  24592  axeuclid  24593  btwncomim  24638  btwnexch3  24645  btwnexch2  24648  endofsegid  24710  onsuct0  24882  ordcmp  24888  nndivsub  24898  dvreasin  24925  ltflcei  24930  areacirclem2  24936  areacirclem3  24937  areacirclem5  24940  areacirc  24942  boxbid  25022  nxtbid  25023  diabid  25024  untbi12d  25033  domrngref  25071  restidsing  25087  fixpc  25105  reflincror  25123  eqfnung2  25129  prjpacp1  25138  prjpacp2  25139  injsurinj  25160  islatalg  25194  oriso  25225  ubpar  25272  inpc  25288  dominc  25291  rninc  25292  toplat  25301  clfsebsr  25360  trooo  25405  imtr  25409  rngoridfz  25448  svs2  25498  truni1  25516  truni3  25518  inttop4  25528  nsn  25541  intcont  25554  cmptdst  25579  limptlimpr2lem2  25586  flfnei2  25588  islimrs4  25593  bwt2  25603  dmse1  25614  iintlem1  25621  supnuf  25640  negveud  25679  negveudr  25680  icccon2  25711  icccon4  25713  rdmob  25759  eqidob  25806  ismonc  25825  cmpmon  25826  idmon  25828  iepiclem  25834  isepic  25835  propsrc  25879  domcatfun  25936  codcatfun  25945  cmp2morp  25969  setiscat  25990  clscnc  26021  lineval6a  26100  sgplpte21c  26146  bosser  26178  pdiveql  26179  abhp  26184  bhp3  26188  opnrebl2  26247  nn0prpwlem  26249  comppfsc  26318  brabg2  26377  enf1f1oOLD  26408  fzmul  26454  fdc  26466  incsequz2  26470  isbnd2  26518  divrngidl  26664  rexrabdioph  26886  fphpdo  26911  icodiamlt  26916  irrapxlem3  26920  rmxypairf1o  27007  rmxycomplete  27013  zindbi  27042  lermxnn0  27048  ltrmy  27050  rmyeq0  27051  rmyeq  27052  lermy  27053  acongsym  27074  acongneg2  27075  wepwsolem  27149  expgrowthi  27561  ordpss  27665  refsum2cnlem1  27719  climinf  27743  stoweidlem7  27767  stoweidlem34  27794  stoweidlem59  27819  stoweidlem62  27822  2reu3  27977  ralbinrald  27988  funressnfv  28002  afv0fv0  28023  afv0nbfvbi  28025  afvfv0bi  28026  fnbrafvb  28027  afvres  28045  tz6.12-afv  28046  afvco2  28048  ndmaovcl  28074  usgraeq12d  28122  usgranloop  28135  nbusgra  28154  iscusgra0  28165  bi23impib  28306  bi123impib  28308  bi123impia  28310  bitr3  28328  rspsbc2  28353  tratrb  28355  sbcim2g  28358  truniALT  28361  3impcombi  28663  tpid3gVD  28691  orbi1rVD  28697  sbc3orgVD  28700  rspsbc2VD  28704  tratrbVD  28710  sbcim2gVD  28724  sbcbiVD  28725  truniALTVD  28727  trintALTVD  28729  trintALT  28730  csbingVD  28733  csbsngVD  28742  csbxpgVD  28743  csbresgVD  28744  csbrngVD  28745  csbima12gALTVD  28746  csbunigVD  28747  csbfv12gALTVD  28748  relopabVD  28750  bnj517  28990  a12stdy2-x12  29185  ax10lem17ALT  29196  ax9lem17  29229  lsatn0  29262  l1cvpat  29317  leat2  29557  atnle  29580  cvlcvr1  29602  cvrexchlem  29681  cvratlem  29683  cvrat  29684  atcvrj0  29690  atle  29698  snatpsubN  30012  linepsubN  30014  pmapsub  30030  lneq2at  30040  lncvrelatN  30043  2llnma3r  30050  cdlemblem  30055  paddasslem5  30086  poml4N  30215  lhpmcvr4N  30288  trlval2  30425  cdlemd6  30465  cdleme7ga  30510  cdleme25b  30616  cdleme29b  30637  cdleme35fnpq  30711  cdleme50f1  30805  cdlemf1  30823  cdlemg27b  30958  cdlemk28-3  31170  tendospcanN  31286  diaf11N  31312  dia2dimlem1  31327  dibf11N  31424  dihf11  31530  dihmeetlem1N  31553  dochvalr  31620  dochnel2  31655  dvh4dimlem  31706  dochsat0  31720  mapd1o  31911  hdmapf1oN  32131  hgmapval0  32158  hgmapf1oN  32169  hlhilhillem  32226
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