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

Theorem biimpd 210
Description: Deduce an implication from a logical equivalence. Deduction associated with biimp 196 and biimpi 197. (Contributed by NM, 11-Jan-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 biimp 196 . 2  |-  ( ( ps  <->  ch )  ->  ( ps  ->  ch ) )
31, 2syl 17 1  |-  ( ph  ->  ( ps  ->  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 188
This theorem is referenced by:  mpbid  213  sylibd  217  sylbid  218  mpbidi  219  syl5ib  222  syl6bi  231  ibi  244  con4bid  294  mtbird  302  mtbiri  304  imbi1d  318  pm5.21im  350  biimpa  486  alexbii  1699  exintr  1750  spfw  1860  cbvalw  1862  alcomiw  1865  19.9dOLD  1951  19.23tOLD  1969  spimt  2063  spv  2069  chvar  2071  cbval  2079  nfsb4t  2187  2eu3  2354  eqrdav  2420  eqrdavOLD  2421  cleqhOLD  2533  rgen2a  2849  ralcom2  2990  raleleq  3040  ceqsalgALT  3107  vtoclf  3132  vtocl2  3134  vtocl3  3135  spcdv  3164  rspcdv  3185  rexraleqim  3197  elabgt  3214  sbcn1  3345  sbcim1  3346  sbcbi1  3347  sbeqalb  3352  sbcel21v  3360  eqrd  3482  elpwunsn  4040  rabsnifsb  4068  ssunsn2  4159  euotd  4721  sotr2  4803  relop  5004  elres  5159  restidsing  5180  elimasni  5214  sotri2  5248  relcnvtr  5374  onmindif  5531  iotaval  5576  dffv2  5955  mpteqb  5981  elfvmptrab  5988  chfnrn  6009  elpreima  6018  iinpreima  6026  exfo  6056  ffnfv  6065  f1elima  6180  f1eqcocnv  6215  fliftfun  6221  soisores  6234  isotr  6243  isomin  6244  ovmpt2dv2  6445  difsnexi  6614  onint  6637  oneqmin  6647  ordunisuc2  6686  tfindsg  6702  findsg  6735  f1oweALT  6792  ressuppss  6946  funsssuppss  6953  imacosupp  6967  smoiso  7093  seqomlem2  7180  oaordi  7259  oawordri  7263  oaordex  7271  oalimcl  7273  omwordi  7284  oewordi  7304  oelim2  7308  nnmwordi  7348  xpider  7446  iiner  7447  undifixp  7570  mptelixpg  7571  dom2lem  7620  nneneq  7765  fineqvlem  7796  pssnn  7800  dif1en  7814  findcard2s  7822  unfilem2  7846  xpfi  7852  domunfican  7854  f1dmvrnfibi  7868  fsuppimp  7899  dffi2  7947  wemaplem2  8072  suc11reg  8134  noinfep  8174  cantnflem1  8203  r1fin  8253  tcrank  8364  cardlim  8415  pr2nelem  8444  fseqenlem1  8463  alephnbtwn  8510  alephord2i  8516  alephf1  8524  cardaleph  8528  alephiso  8537  dfac12lem2  8582  ackbij1lem16  8673  cflm  8688  cfcoflem  8710  sornom  8715  fin23lem27  8766  isf32lem7  8797  fin17  8832  fin1a2lem2  8839  fin1a2lem4  8841  fin1a2lem6  8843  fin1a2lem9  8846  axdc3lem2  8889  zorn2lem7  8940  uniimadom  8977  inar1  9208  grothomex  9262  addcanpi  9332  mulcanpi  9333  enqer  9354  genpcd  9439  genpnmax  9440  ltexprlem4  9472  reclem3pr  9482  reclem4pr  9483  suplem2pr  9486  axpre-ltadd  9599  axpre-sup  9601  ltletr  9733  00id  9816  mul0or  10260  prodgt02  10459  prodge02  10461  lemul1a  10467  mulgt1  10472  divgt0  10481  divge0  10482  ledivp1i  10540  ltdivp1i  10541  cju  10613  nnsub  10656  nominpos  10857  nn0n0n1ge2  10940  btwnnz  11020  suprfinzcl  11058  ublbneg  11256  zmax  11269  cnref1o  11305  ltsubrp  11343  ltaddrp  11344  xrltletr  11462  qbtwnre  11500  xltnegi  11517  iccsupr  11735  icoshft  11762  difreicc  11772  iccshftri  11775  iccshftli  11777  iccdili  11779  icccntri  11781  fzen  11824  elfzmlbmOLD  11909  fzofzim  11970  eluzgtdifelfzo  11983  injresinjlem  12031  injresinj  12032  flval2  12056  flval3  12057  modaddmodup  12160  fseqsupubi  12198  ssnn0fi  12204  mptnn0fsuppr  12218  sq01  12401  hashf1rn  12542  hashle00  12584  hashgt12el  12600  hashgt12el2  12601  hash2pr  12635  hash2exprb  12637  hashge2el2difr  12643  hashtpg  12646  hash3tr  12652  lswlgt0cl  12721  2swrd1eqwrdeq  12813  ccatopth2  12830  reuccats1lem  12839  swrdccatin2  12846  swrdccat  12852  swrdccat3a  12853  swrdccat3blem  12854  repsdf2  12884  repswsymball  12885  repswrevw  12892  cshweqrep  12923  cshw1  12924  2cshwcshw  12927  scshwfzeqfzo  12928  cshwcsh2id  12930  swrdco  12937  swrd2lsw  13028  2swrd2eqwrdeq  13029  wwlktovfo  13034  cjre  13203  o1lo1  13601  o1of2  13676  o1rlimmul  13682  zsum  13784  modfsummods  13853  zprod  13991  reeff1  14174  dvds2lem  14315  muldvds1  14327  dvdscmulr  14331  dvdsmulcr  14332  divalglem8  14380  ndvdsadd  14389  gcdmultiple  14518  absproddvds  14587  lcmftp  14609  prmn2uzge3  14644  isprm5  14651  divgcdodd  14653  isprm6  14666  prmdvdsexpr  14669  phiprmpw  14724  modprm0  14756  pythagtriplem4  14769  pcz  14830  1arith  14871  prmgaplem5  15025  prmgaplem6  15026  cshwrepswhash1  15073  divsfval  15453  catsubcat  15744  fthmon  15832  isinitoi  15898  istermoi  15899  iszeroi  15904  setcmon  15982  setcepi  15983  funcestrcsetclem8  16032  fthestrcsetc  16035  funcsetcestrclem8  16047  fthsetcestrc  16050  pltnle  16212  pltval3  16213  lublecllem  16234  latasym  16301  odupos  16381  mrelatglb  16430  mrelatlub  16432  cnvpsb  16459  isgrpid2  16702  ghmf1  16911  orbsta  16967  resscntz  16985  gsmsymgrfixlem1  17068  gsmsymgreqlem2  17072  mndodcongi  17192  odf1  17213  lsmss1  17316  lsmss2  17318  efgredeu  17402  cntzcmnss  17481  lt6abl  17529  ablfaclem3  17720  kerf1hrm  17971  lspsneq  18345  lspsneu  18346  lsmcv  18364  lidldvgen  18479  0ringnnzr  18493  domnmuln0  18522  opprdomn  18525  ply1scln0  18884  gsummoncoe1  18898  domnchr  19102  znf1o  19121  zntoslem  19126  znfld  19130  cygznlem2a  19137  cygznlem3  19139  islindf4  19395  uvcendim  19404  matvscl  19455  scmataddcl  19540  scmatsubcl  19541  scmatfo  19554  scmatghm  19557  maducoeval2  19664  slesolinv  19704  cramerimplem2  19708  cpmatelimp  19735  cpmatelimp2  19737  cpmatacl  19739  cpmatinvcl  19740  pm2mpf1  19822  cayhamlem1  19889  cayleyhamilton1  19915  0ntr  20086  islpi  20164  lmss  20313  cmpcld  20416  cmpfi  20422  1stcelcls  20475  comppfsc  20546  ptcnplem  20635  qtophmeo  20831  fbdmn0  20848  fbasrn  20898  elfm3  20964  fmfnfmlem4  20971  fclscf  21039  cnpfcf  21055  alexsubALTlem3  21063  tsmsres  21157  blval2  21576  nmoleub  21735  nmoleubOLD  21751  nmhmcn  22133  iscau4  22248  caussi  22266  cniccbdd  22411  ovoliunnul  22459  mbfinf  22620  mbfinfOLD  22621  itg2splitlem  22705  dvcn  22874  c1lip1  22948  c1lip3  22950  dvcnvrelem1  22968  ply1divex  23086  quotcan  23261  aannenlem1  23283  taylf  23315  ulmcaulem  23348  ulmcau  23349  reeff1o  23401  logccv  23607  logreclem  23698  isosctrlem2  23747  xrlimcnp  23893  rlimcxp  23898  ftalem7  24004  vmappw  24042  fsumvma  24140  dchreq  24185  dchrptlem1  24191  dchrsum  24196  bposlem7  24217  lgsqrlem2  24269  lgsdchr  24275  lgseisenlem2  24277  lgsquad2  24287  2sqlem6  24296  tgcgrcomimp  24520  isperp2  24759  xmstrkgc  24915  brbtwn  24928  brcgr  24929  axcgrid  24945  axeuclidlem  24991  axeuclid  24992  uhgraeq12d  25033  usgrac  25077  usgraeq12d  25088  usgranloopv  25104  nbgraf1olem5  25172  iscusgra0  25184  cusgrasize2inds  25204  cusgrafilem3  25208  usgramaxsize  25214  iswlkg  25251  wlkcompim  25253  wlkcpr  25256  wlkonprop  25262  trlonprop  25271  0wlkon  25276  usgrwlknloop  25292  pthonprop  25306  spthonprp  25314  redwlk  25335  wlkdvspthlem  25336  usgra2wlkspthlem2  25347  fargshiftfv  25362  wwlknimp  25414  vfwlkniswwlkn  25433  usg2wlkeq  25435  wwlknred  25450  wwlknext  25451  wwlknextbi  25452  wwlkextwrd  25455  wwlkextinj  25457  wwlkextsur  25458  wwlkm1edg  25462  isclwlkg  25482  clwlkcompim  25491  0clwlk  25492  clwwlkn2  25502  clwlkisclwwlklem2a1  25506  clwlkisclwwlklem2a4  25511  clwlkisclwwlklem2a  25512  clwlkisclwwlklem1  25514  clwwlkf  25521  wwlkext2clwwlk  25530  clwwisshclwwlem1  25532  wlklenvclwlk  25566  clwlkfclwwlk  25571  el2spthonot  25597  usg2wotspth  25611  usg2spthonot  25615  usg2spthonot0  25616  rgraprop  25655  rusgraprop  25656  rusgraprop3  25670  frgranbnb  25747  frgrancvvdeqlem3  25759  frgrancvvdeqlem4  25760  frgrancvvdeqlem7  25763  frgrawopreglem2  25772  frgrawopreg  25776  frgregordn0  25797  clwwlkextfrlem1  25803  extwwlkfablem2  25805  numclwwlkun  25806  numclwwlkovf2ex  25813  numclwlk1lem2foa  25818  numclwlk1lem2f1  25821  numclwwlk8  25842  gxid  26000  opidonOLD  26049  opidon2OLD  26051  grpomndo  26073  elghomlem2OLD  26089  rngoueqz  26157  dvrunz  26160  rngoridfz  26162  hlipgt0  26565  ocin  26948  ocnel  26950  shmodsi  27041  pjmf1  27368  unopf1o  27568  staddi  27898  stadd3i  27900  mdi  27947  dmdmd  27952  dmdi  27954  dmdbr2  27955  dmdbr3  27957  dmdbr4  27958  dmdi4  27959  mdsl1i  27973  superpos  28006  cvbr4i  28019  atssma  28030  atcv1  28032  atomli  28034  chirredlem1  28042  addltmulALT  28098  bian1d  28099  ifeqeqx  28161  disjxpin  28201  suppss3  28319  fpwrelmap  28325  xrge0infssOLD  28348  ogrpaddlt  28489  metider  28706  tpr2rico  28727  xrge0iifiso  28750  qqhcn  28804  qqhucn  28805  esumlub  28890  esumpinfval  28903  esumpinfsum  28907  ballotlemfc0  29334  ballotlemfcc  29335  bnj517  29705  erdsze2lem2  29936  trpredrec  30487  poseq  30499  soseq  30500  sltval2  30551  sltres  30559  nodenselem7  30582  nodenselem8  30583  nodense  30584  nobndup  30595  nobnddown  30596  nofulllem5  30601  dfrdg4  30724  altopthsn  30734  btwncomim  30786  btwnexch3  30793  btwnexch2  30796  endofsegid  30858  opnrebl2  30983  nn0prpwlem  30984  onsuct0  31107  ordcmp  31113  nndivsub  31123  bj-cbvexw  31236  bj-cbv3tb  31272  bj-spimtv  31279  bj-spvv  31285  bj-chvarv  31287  bj-cbvalv  31297  bj-cleqh  31358  bj-equsal  31399  bj-ax8  31465  bj-vtoclf  31485  bj-snsetex  31526  bj-inftyexpiinj  31616  bj-finsumval0  31667  bj-bary1lem1  31681  bj-bary1  31682  f1omptsnlem  31703  iooelexlt  31730  relowlpssretop  31732  rdgeqoa  31738  finxpsuclem  31754  wl-equsal1i  31841  wl-ax11-lem10  31889  ltflcei  31898  sin2h  31900  cos2h  31901  tan2h  31902  poimirlem3  31908  poimirlem4  31909  poimirlem18  31923  poimirlem20  31925  poimirlem21  31926  poimirlem22  31927  poimirlem24  31929  poimirlem25  31930  poimirlem26  31931  poimirlem27  31932  poimirlem28  31933  poimirlem31  31936  poimir  31938  heicant  31940  mblfinlem1  31942  mblfinlem2  31943  mblfinlem3  31944  mblfinlem4  31945  mbfresfi  31952  cnambfre  31954  dvtanlemOLD  31956  ftc1anc  31990  dvasin  31993  areacirclem1  31997  areacirclem4  32000  areacirc  32002  brabg2  32007  fzmul  32034  fdc  32039  incsequz2  32043  isbnd2  32080  divrngidl  32226  dral1-o  32444  lsatn0  32535  l1cvpat  32590  leat2  32830  atnle  32853  cvlcvr1  32875  cvrexchlem  32954  cvratlem  32956  cvrat  32957  atcvrj0  32963  atle  32971  snatpsubN  33285  linepsubN  33287  pmapsub  33303  lneq2at  33313  lncvrelatN  33316  2llnma3r  33323  cdlemblem  33328  paddasslem5  33359  poml4N  33488  lhpmcvr4N  33561  trlval2  33699  cdlemd6  33739  cdleme7ga  33784  cdleme25b  33891  cdleme29b  33912  cdleme35fnpq  33986  cdleme50f1  34080  cdlemf1  34098  cdlemg27b  34233  cdlemk28-3  34445  tendospcanN  34561  diaf11N  34587  dia2dimlem1  34602  dibf11N  34699  dihf11  34805  dihmeetlem1N  34828  dochvalr  34895  dochnel2  34930  dvh4dimlem  34981  dochsat0  34995  mapd1o  35186  hdmapf1oN  35406  hgmapval0  35433  hgmapf1oN  35444  hlhilhillem  35501  rexrabdioph  35607  fphpdo  35630  icodiamlt  35635  irrapxlem3  35639  rmxypairf1o  35730  rmxycomplete  35736  zindbi  35765  lermxnn0  35771  ltrmy  35773  rmyeq0  35774  rmyeq  35775  lermy  35776  acongsym  35797  acongneg2  35798  wepwsolem  35871  intabssd  36187  ss2iundf  36222  frege129d  36326  frege133d  36328  axfrege52a  36423  axfrege52c  36454  suprleubrd  36580  suprlubrd  36584  radcnvrat  36634  nzss  36637  expgrowthi  36653  ordpss  36775  bi23impib  36812  bi23imp13  36818  bitr3  36838  rspsbc2  36866  tratrb  36868  sbcim2g  36870  truniALT  36873  3impcombi  37178  tpid3gVD  37212  orbi1rVD  37218  sbc3orgVD  37221  rspsbc2VD  37225  tratrbVD  37232  sbcim2gVD  37246  sbcbiVD  37247  truniALTVD  37249  trintALTVD  37251  trintALT  37252  csbingVD  37255  csbsngVD  37264  csbxpgVD  37265  csbresgVD  37266  csbrngVD  37267  csbima12gALTVD  37268  csbunigVD  37269  csbfv12gALTVD  37270  relopabVD  37272  isosctrlem1ALT  37305  fzisoeu  37473  climinf  37625  climinfOLD  37626  stoweidlem7  37808  stoweidlem62  37864  stoweidlem62OLD  37865  sge0gerpmpt  38153  carageniuncllem2  38252  2reu3  38481  ralbinrald  38492  funressnfv  38501  afv0fv0  38522  afv0nbfvbi  38524  afvfv0bi  38525  fnbrafvb  38527  afvres  38545  tz6.12-afv  38546  afvco2  38549  ndmaovcl  38576  nltle2tri  38587  mod2eq1n2dvds  38596  iccpartres  38603  iccpartiltu  38607  evennodd  38644  oddneven  38645  oexpnegALTV  38677  oexpnegnz  38678  gboge7  38735  gbege6  38737  bgoldbwt  38749  bgoldbst  38750  nnsum3primesle9  38760  bgoldbtbndlem2  38772  pfxfv  38811  pfxsuff1eqwrdeq  38819  reuccatpfxs1lem  38845  propeqop  38866  zm1nn  38904  subsubelfzo0  38917  usgredgaleord  39113  uhgr0v0e  39117  subgrprop  39140  fusgrfisbase  39188  nbumgrvtx  39208  edgnbusgreu  39235  nbusgredgeu0  39236  cusgredg  39278  nbcplgr  39287  cusgrsize2inds  39300  cusgrsize  39301  usgredgsscusgredg  39306  fusgrmaxsize  39311  usgra2pth  39317  usgpredgv  39360  usgpredgvALT  39361  usgfis  39407  usgfisALT  39411  mgmpropd  39424  clintop  39493  isassintop  39495  lidldomn1  39570  uzlidlring  39578  2zrngnmlid2  39600  rngccatidALTV  39640  ringccatidALTV  39703  srhmsubc  39727  srhmsubcALTV  39746  ztprmneprm  39779  pgrpgt2nabl  39802  lindslinindimp2lem4  39905  lincresunit3  39925  fldivexpfllog2  40027  digexp  40069
  Copyright terms: Public domain W3C validator