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

Theorem biimpd 212
Description: Deduce an implication from a logical equivalence. Deduction associated with biimp 198 and biimpi 199. (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 198 . 2  |-  ( ( ps  <->  ch )  ->  ( ps  ->  ch ) )
31, 2syl 17 1  |-  ( ph  ->  ( ps  ->  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189
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 190
This theorem is referenced by:  mpbid  215  sylibd  222  sylbid  223  mpbidi  224  syl5ib  227  syl6bi  236  ibi  249  con4bid  299  mtbird  307  mtbiri  309  imbi1d  323  pm5.21im  355  biimpa  491  alexbii  1709  exintr  1760  spfw  1879  cbvalw  1881  alcomiw  1884  19.9dOLD  1979  19.23tOLD  1997  cbvalv1  2069  spimt  2098  spv  2105  chvar  2107  cbval  2115  nfsb4t  2219  2eu3  2385  eqrdav  2451  rgen2a  2801  ralcom2  2923  raleleq  2973  ceqsalgALT  3041  vtoclf  3067  vtocl  3068  vtocl2  3070  vtocl3  3071  spcdv  3100  rspcdv  3121  rexraleqim  3133  elabgt  3150  sbcn1  3281  sbcim1  3282  sbcbi1  3283  sbeqalb  3288  sbcel21v  3296  eqrd  3418  elpwunsn  3980  rabsnifsb  4009  ssunsn2  4100  preqr1g  4123  euotd  4675  sotr2  4762  relop  4963  elres  5118  restidsing  5139  elimasni  5173  sotri2  5207  relcnvtr  5334  onmindif  5491  iotaval  5536  dffv2  5922  mpteqb  5948  elfvmptrab  5955  chfnrn  5977  elpreima  5986  iinpreima  5994  exfo  6024  ffnfv  6033  f1elima  6150  f1eqcocnv  6185  fliftfun  6191  soisores  6204  isotr  6213  isomin  6214  ovmpt2dv2  6418  difsnexi  6587  onint  6610  oneqmin  6620  ordunisuc2  6659  tfindsg  6675  findsg  6708  f1oweALT  6765  ressuppss  6922  funsssuppss  6929  imacosupp  6943  smoiso  7068  seqomlem2  7155  oaordi  7234  oawordri  7238  oaordex  7246  oalimcl  7248  omwordi  7259  oewordi  7279  oelim2  7283  nnmwordi  7323  xpider  7421  iiner  7422  undifixp  7545  mptelixpg  7546  dom2lem  7596  nneneq  7742  fineqvlem  7773  pssnn  7777  dif1en  7791  findcard2s  7799  unfilem2  7823  xpfi  7829  domunfican  7831  f1dmvrnfibi  7845  fsuppimp  7876  dffi2  7924  wemaplem2  8049  suc11reg  8111  noinfep  8152  cantnflem1  8181  r1fin  8231  tcrank  8342  cardlim  8393  pr2nelem  8422  fseqenlem1  8442  alephnbtwn  8489  alephord2i  8495  alephf1  8503  cardaleph  8507  alephiso  8516  dfac12lem2  8561  ackbij1lem16  8652  cflm  8667  cfcoflem  8689  sornom  8694  fin23lem27  8745  isf32lem7  8776  fin17  8811  fin1a2lem2  8818  fin1a2lem4  8820  fin1a2lem6  8822  fin1a2lem9  8825  axdc3lem2  8868  zorn2lem7  8919  uniimadom  8956  inar1  9187  grothomex  9241  addcanpi  9311  mulcanpi  9312  enqer  9333  genpcd  9418  genpnmax  9419  ltexprlem4  9451  reclem3pr  9461  reclem4pr  9462  suplem2pr  9465  axpre-ltadd  9578  axpre-sup  9580  ltletr  9712  00id  9795  addn0nid  10029  mul0or  10241  prodgt02  10440  prodge02  10442  lemul1a  10448  mulgt1  10453  divgt0  10462  divge0  10463  ledivp1i  10521  ltdivp1i  10522  cju  10594  nnsub  10637  nominpos  10839  nn0n0n1ge2  10922  btwnnz  11002  suprfinzcl  11040  ublbneg  11238  zmax  11251  cnref1o  11287  ltsubrp  11325  ltaddrp  11326  xrltletr  11444  qbtwnre  11482  xltnegi  11499  iccsupr  11717  icoshft  11745  difreicc  11755  iccshftri  11758  iccshftli  11760  iccdili  11762  icccntri  11764  fzen  11807  elfzmlbmOLD  11893  fzofzim  11955  eluzgtdifelfzo  11969  injresinjlem  12018  injresinj  12019  flval2  12043  flval3  12044  modaddmodup  12147  fseqsupubi  12185  ssnn0fi  12191  mptnn0fsuppr  12205  sq01  12388  hashf1rn  12529  hashle00  12571  hashgt12el  12590  hashgt12el2  12591  hash2pr  12625  hash2exprb  12627  hashge2el2difr  12633  hashtpg  12636  hash3tr  12642  lswlgt0cl  12714  2swrd1eqwrdeq  12809  ccatopth2  12826  reuccats1lem  12835  swrdccatin2  12842  swrdccat  12848  swrdccat3a  12849  swrdccat3blem  12850  repsdf2  12880  repswsymball  12881  repswrevw  12888  cshweqrep  12919  cshw1  12920  2cshwcshw  12923  scshwfzeqfzo  12924  cshwcsh2id  12926  swrdco  12933  swrd2lsw  13038  2swrd2eqwrdeq  13039  wwlktovfo  13044  cjre  13213  icodiamlt  13508  o1lo1  13612  o1of2  13687  o1rlimmul  13693  zsum  13795  modfsummods  13864  zprod  14002  reeff1  14185  dvds2lem  14326  muldvds1  14338  dvdscmulr  14342  dvdsmulcr  14343  divalglem8  14391  ndvdsadd  14400  gcdmultiple  14529  absproddvds  14598  lcmftp  14620  prmn2uzge3  14655  isprm5  14662  divgcdodd  14664  isprm6  14677  prmdvdsexpr  14680  phiprmpw  14735  modprm0  14767  pythagtriplem4  14780  pcz  14841  1arith  14882  prmgaplem5  15036  prmgaplem6  15037  cshwrepswhash1  15084  divsfval  15464  catsubcat  15755  fthmon  15843  isinitoi  15909  istermoi  15910  iszeroi  15915  setcmon  15993  setcepi  15994  funcestrcsetclem8  16043  fthestrcsetc  16046  funcsetcestrclem8  16058  fthsetcestrc  16061  pltnle  16223  pltval3  16224  lublecllem  16245  latasym  16312  odupos  16392  mrelatglb  16441  mrelatlub  16443  cnvpsb  16470  isgrpid2  16713  ghmf1  16922  orbsta  16978  resscntz  16996  gsmsymgrfixlem1  17079  gsmsymgreqlem2  17083  mndodcongi  17203  odf1  17224  lsmss1  17327  lsmss2  17329  efgredeu  17413  cntzcmnss  17492  lt6abl  17540  ablfaclem3  17731  kerf1hrm  17982  lspsneq  18356  lspsneu  18357  lsmcv  18375  lidldvgen  18490  0ringnnzr  18504  domnmuln0  18533  opprdomn  18536  ply1scln0  18895  gsummoncoe1  18909  domnchr  19114  znf1o  19133  zntoslem  19138  znfld  19142  cygznlem2a  19149  cygznlem3  19151  islindf4  19407  uvcendim  19416  matvscl  19467  scmataddcl  19552  scmatsubcl  19553  scmatfo  19566  scmatghm  19569  maducoeval2  19676  slesolinv  19716  cramerimplem2  19720  cpmatelimp  19747  cpmatelimp2  19749  cpmatacl  19751  cpmatinvcl  19752  pm2mpf1  19834  cayhamlem1  19901  cayleyhamilton1  19927  0ntr  20098  islpi  20176  lmss  20325  cmpcld  20428  cmpfi  20434  1stcelcls  20487  comppfsc  20558  ptcnplem  20647  qtophmeo  20843  fbdmn0  20860  fbasrn  20910  elfm3  20976  fmfnfmlem4  20983  fclscf  21051  cnpfcf  21067  alexsubALTlem3  21075  tsmsres  21169  blval2  21588  nmoleub  21747  nmoleubOLD  21763  nmhmcn  22145  iscau4  22260  caussi  22278  cniccbdd  22423  ovoliunnul  22471  mbfinf  22633  mbfinfOLD  22634  itg2splitlem  22718  dvcn  22887  c1lip1  22961  c1lip3  22963  dvcnvrelem1  22981  ply1divex  23099  quotcan  23274  aannenlem1  23296  taylf  23328  ulmcaulem  23361  ulmcau  23362  reeff1o  23414  logccv  23620  logreclem  23711  isosctrlem2  23760  xrlimcnp  23906  rlimcxp  23911  ftalem7  24017  vmappw  24055  fsumvma  24153  dchreq  24198  dchrptlem1  24204  dchrsum  24209  bposlem7  24230  lgsqrlem2  24282  lgsdchr  24288  lgseisenlem2  24290  lgsquad2  24300  2sqlem6  24309  tgcgrcomimp  24533  isperp2  24772  xmstrkgc  24928  brbtwn  24941  brcgr  24942  axcgrid  24958  axeuclidlem  25004  axeuclid  25005  uhgraeq12d  25046  usgrac  25090  usgraeq12d  25101  usgranloopv  25117  nbgraf1olem5  25185  iscusgra0  25197  cusgrasize2inds  25217  cusgrafilem3  25221  usgramaxsize  25227  iswlkg  25264  wlkcompim  25266  wlkcpr  25269  wlkonprop  25275  trlonprop  25284  0wlkon  25289  usgrwlknloop  25305  pthonprop  25319  spthonprp  25327  redwlk  25348  wlkdvspthlem  25349  usgra2wlkspthlem2  25360  fargshiftfv  25375  wwlknimp  25427  vfwlkniswwlkn  25446  usg2wlkeq  25448  wwlknred  25463  wwlknext  25464  wwlknextbi  25465  wwlkextwrd  25468  wwlkextinj  25470  wwlkextsur  25471  wwlkm1edg  25475  isclwlkg  25495  clwlkcompim  25504  0clwlk  25505  clwwlkn2  25515  clwlkisclwwlklem2a1  25519  clwlkisclwwlklem2a4  25524  clwlkisclwwlklem2a  25525  clwlkisclwwlklem1  25527  clwwlkf  25534  wwlkext2clwwlk  25543  clwwisshclwwlem1  25545  wlklenvclwlk  25579  clwlkfclwwlk  25584  el2spthonot  25610  usg2wotspth  25624  usg2spthonot  25628  usg2spthonot0  25629  rgraprop  25668  rusgraprop  25669  rusgraprop3  25683  frgranbnb  25760  frgrancvvdeqlem3  25772  frgrancvvdeqlem4  25773  frgrancvvdeqlem7  25776  frgrawopreglem2  25785  frgrawopreg  25789  frgregordn0  25810  clwwlkextfrlem1  25816  extwwlkfablem2  25818  numclwwlkun  25819  numclwwlkovf2ex  25826  numclwlk1lem2foa  25831  numclwlk1lem2f1  25834  numclwwlk8  25855  gxid  26013  opidonOLD  26062  opidon2OLD  26064  grpomndo  26086  elghomlem2OLD  26102  rngoueqz  26170  dvrunz  26173  rngoridfz  26175  hlipgt0  26578  ocin  26961  ocnel  26963  shmodsi  27054  pjmf1  27381  unopf1o  27581  staddi  27911  stadd3i  27913  mdi  27960  dmdmd  27965  dmdi  27967  dmdbr2  27968  dmdbr3  27970  dmdbr4  27971  dmdi4  27972  mdsl1i  27986  superpos  28019  cvbr4i  28032  atssma  28043  atcv1  28045  atomli  28047  chirredlem1  28055  addltmulALT  28111  bian1d  28112  ifeqeqx  28169  disjxpin  28208  suppss3  28320  fpwrelmap  28326  xrge0infssOLD  28349  ogrpaddlt  28488  metider  28704  tpr2rico  28725  xrge0iifiso  28748  qqhcn  28802  qqhucn  28803  esumlub  28888  esumpinfval  28901  esumpinfsum  28905  ballotlemfc0  29331  ballotlemfcc  29332  bnj517  29702  erdsze2lem2  29933  trpredrec  30485  poseq  30497  soseq  30498  sltval2  30549  sltres  30557  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  31275  bj-cbv3tb  31314  bj-spimtv  31321  bj-spvv  31326  bj-chvarv  31328  bj-equsal  31430  bj-ax8  31497  bj-vtoclf  31517  bj-snsetex  31559  bj-inftyexpiinj  31653  bj-finsumval0  31704  bj-bary1lem1  31718  bj-bary1  31719  f1omptsnlem  31740  iooelexlt  31767  relowlpssretop  31769  rdgeqoa  31775  finxpsuclem  31791  wl-equsal1i  31878  wl-ax11-lem10  31926  ltflcei  31935  sin2h  31937  cos2h  31938  tan2h  31939  poimirlem3  31945  poimirlem4  31946  poimirlem18  31960  poimirlem20  31962  poimirlem21  31963  poimirlem22  31964  poimirlem24  31966  poimirlem25  31967  poimirlem26  31968  poimirlem27  31969  poimirlem28  31970  poimirlem31  31973  poimir  31975  heicant  31977  mblfinlem1  31979  mblfinlem2  31980  mblfinlem3  31981  mblfinlem4  31982  mbfresfi  31989  cnambfre  31991  dvtanlemOLD  31993  ftc1anc  32027  dvasin  32030  areacirclem1  32034  areacirclem4  32037  areacirc  32039  brabg2  32044  fzmul  32071  fdc  32076  incsequz2  32080  isbnd2  32117  divrngidl  32263  dral1-o  32476  lsatn0  32567  l1cvpat  32622  leat2  32862  atnle  32885  cvlcvr1  32907  cvrexchlem  32986  cvratlem  32988  cvrat  32989  atcvrj0  32995  atle  33003  snatpsubN  33317  linepsubN  33319  pmapsub  33335  lneq2at  33345  lncvrelatN  33348  2llnma3r  33355  cdlemblem  33360  paddasslem5  33391  poml4N  33520  lhpmcvr4N  33593  trlval2  33731  cdlemd6  33771  cdleme7ga  33816  cdleme25b  33923  cdleme29b  33944  cdleme35fnpq  34018  cdleme50f1  34112  cdlemf1  34130  cdlemg27b  34265  cdlemk28-3  34477  tendospcanN  34593  diaf11N  34619  dia2dimlem1  34634  dibf11N  34731  dihf11  34837  dihmeetlem1N  34860  dochvalr  34927  dochnel2  34962  dvh4dimlem  35013  dochsat0  35027  mapd1o  35218  hdmapf1oN  35438  hgmapval0  35465  hgmapf1oN  35476  hlhilhillem  35533  rexrabdioph  35639  fphpdo  35662  irrapxlem3  35670  rmxypairf1o  35761  rmxycomplete  35767  zindbi  35796  lermxnn0  35802  ltrmy  35804  rmyeq0  35805  rmyeq  35806  lermy  35807  acongsym  35828  acongneg2  35829  wepwsolem  35902  intabssd  36218  ss2iundf  36253  frege129d  36357  frege133d  36359  axfrege52a  36454  axfrege52c  36485  suprleubrd  36611  suprlubrd  36615  radcnvrat  36664  nzss  36667  expgrowthi  36683  ordpss  36805  bi23impib  36842  bi23imp13  36848  bitr3  36868  rspsbc2  36896  tratrb  36898  sbcim2g  36900  truniALT  36903  3impcombi  37201  tpid3gVD  37235  orbi1rVD  37241  sbc3orgVD  37244  rspsbc2VD  37248  tratrbVD  37255  sbcim2gVD  37269  sbcbiVD  37270  truniALTVD  37272  trintALTVD  37274  trintALT  37275  csbingVD  37278  csbsngVD  37287  csbxpgVD  37288  csbresgVD  37289  csbrngVD  37290  csbima12gALTVD  37291  csbunigVD  37292  csbfv12gALTVD  37293  relopabVD  37295  isosctrlem1ALT  37328  fzisoeu  37549  climinf  37726  climinfOLD  37727  stoweidlem7  37924  stoweidlem62  37980  stoweidlem62OLD  37981  sge0gerpmpt  38303  carageniuncllem2  38407  2reu3  38700  ralbinrald  38711  funressnfv  38720  afv0fv0  38742  afv0nbfvbi  38744  afvfv0bi  38745  fnbrafvb  38747  afvres  38765  tz6.12-afv  38766  afvco2  38769  ndmaovcl  38796  nltle2tri  38807  mod2eq1n2dvds  38816  iccpartres  38823  iccpartiltu  38827  evennodd  38864  oddneven  38865  oexpnegALTV  38897  oexpnegnz  38898  gboge7  38955  gbege6  38957  bgoldbwt  38969  bgoldbst  38970  nnsum3primesle9  38980  bgoldbtbndlem2  38992  pfxfv  39033  pfxsuff1eqwrdeq  39041  reuccatpfxs1lem  39067  propeqop  39092  zm1nn  39143  subsubelfzo0  39156  xnn0xadd0  39186  lpvtx  39257  upgrex  39283  upgredgpr  39332  usgredgaleordALT  39413  uhgr0v0e  39416  subgrprop  39447  fusgrfisbase  39496  edgnbusgreu  39543  nbusgredgeu0  39544  cusgredg  39594  nbcplgr  39603  cusgrsize2inds  39616  cusgrsize  39617  usgredgsscusgredg  39622  fusgrmaxsize  39627  umgr2v2e  39664  rgrprop  39680  rusgrprop  39682  0uhgrrusgr  39696  rusgrpropedg  39702  ewlkprop  39722  upgrewlkle2  39725  wlk1wlk  39751  wlkOnprop  39761  red1wlk  39769  1wlkvtxeledg  39773  1wlkdlem2  39778  1wlksonproplem  39792  usgr2wlkspthlem2  39842  pthdlem1  39844  isclWlkb  39852  crctprop  39867  cyclprop  39868  umgr2wlk  39950  usgra2pth  39993  usgpredgv  40036  usgpredgvALT  40037  usgfis  40083  usgfisALT  40087  mgmpropd  40100  clintop  40169  isassintop  40171  lidldomn1  40246  uzlidlring  40254  2zrngnmlid2  40276  rngccatidALTV  40316  ringccatidALTV  40379  srhmsubc  40403  srhmsubcALTV  40422  ztprmneprm  40453  pgrpgt2nabl  40476  lindslinindimp2lem4  40579  lincresunit3  40599  fldivexpfllog2  40701  digexp  40743
  Copyright terms: Public domain W3C validator