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

Theorem pm5.32da 645
Description: Distribution of implication over biconditional (deduction rule). (Contributed by NM, 9-Dec-2006.)
Hypothesis
Ref Expression
pm5.32da.1  |-  ( (
ph  /\  ps )  ->  ( ch  <->  th )
)
Assertion
Ref Expression
pm5.32da  |-  ( ph  ->  ( ( ps  /\  ch )  <->  ( ps  /\  th ) ) )

Proof of Theorem pm5.32da
StepHypRef Expression
1 pm5.32da.1 . . 3  |-  ( (
ph  /\  ps )  ->  ( ch  <->  th )
)
21ex 435 . 2  |-  ( ph  ->  ( ps  ->  ( ch 
<->  th ) ) )
32pm5.32d 643 1  |-  ( ph  ->  ( ( ps  /\  ch )  <->  ( ps  /\  th ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370
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  df-an 372
This theorem is referenced by:  rexbida  2941  rexbidva  2943  reubida  3018  rmobida  3023  mpteq12f  4502  reuhypd  4649  xpdifid  5285  funbrfv2b  5925  dffn5  5926  eqfnfv2  5992  fmptco  6071  dff13  6174  riotabidva  6283  mpt2eq123dva  6366  mpt2eq3dva  6369  opiota  6866  fnwelem  6922  suppssr  6957  mpt2xopovel  6974  mpt2curryd  7024  oeeui  7311  omabs  7356  qliftfun  7456  erovlem  7467  xpcomco  7668  pw2f1olem  7682  elfi2  7934  cardval2  8424  dfac2  8559  cflim3  8690  iundom2g  8963  fpwwe2lem8  9061  fpwwe2lem12  9065  ltexpi  9326  ordpipq  9366  axrrecex  9586  nnunb  10865  zrevaddcl  10982  qrevaddcl  11286  icoshft  11752  fznn  11861  preduz  11909  predfz  11912  fznnfl  12086  fz1isolem  12619  swrdeq  12785  2swrdeqwrdeq  12794  2swrd1eqwrdeq  12795  2swrd2eqwrdeq  13007  2shfti  13122  limsupgle  13513  ello12  13558  elo12  13569  isercoll  13709  sumeq2ii  13737  fsum2dlem  13809  prodeq2ii  13945  bitsmod  14384  bitscmp  14386  pwsle  15349  imasleval  15398  acsfiel  15511  ismon2  15590  isepi2  15597  oppcsect  15634  subsubc  15709  funcpropd  15756  fullpropd  15776  fucsect  15828  setcsect  15935  pltval3  16164  grpidpropd  16455  ismgmid  16458  gsumpropd2lem  16467  mhmpropd  16539  issubm2  16546  subgacs  16803  eqgid  16820  pgpfi2  17193  eqgabl  17410  iscyggen2  17451  cyggenod  17454  eldprd  17571  subgdmdprd  17602  dprd2d2  17612  ringpropd  17747  crngunit  17825  dvdsrpropd  17859  drngpropd  17937  issubrg3  17971  lsslss  18119  lsspropd  18175  lmhmpropd  18231  lbspropd  18257  aspval2  18506  znleval  19056  znunithash  19066  pjdm2  19205  islinds2  19302  bastop2  19941  elcls2  20021  neiptopreu  20080  maxlp  20094  restopn2  20124  iscnp3  20191  subbascn  20201  lmbr2  20206  kgencn  20502  kgencn2  20503  hauseqlcld  20592  txlm  20594  txkgen  20598  xkoptsub  20600  idqtop  20652  tgqtop  20658  qtopcld  20659  elmptrab  20773  flimopn  20921  fbflim  20922  fbflim2  20923  flimrest  20929  flffbas  20941  flftg  20942  cnflf  20948  cnflf2  20949  txflf  20952  isfcls  20955  fclsopn  20960  fclsbas  20967  fclsrest  20970  fcfnei  20981  cnfcf  20988  ptcmplem2  20999  tgphaus  21062  tsmssubm  21088  isucn2  21225  ismet2  21279  xblpnfps  21341  xblpnf  21342  blin  21367  blres  21377  elmopn2  21391  imasf1obl  21434  imasf1oxms  21435  prdsbl  21437  neibl  21447  metrest  21470  metcnp3  21486  metcnp  21487  metcnp2  21488  metcn  21489  txmetcnp  21493  txmetcn  21494  metuel2  21511  metucn  21517  ngppropd  21576  cnbl0  21705  cnblcld  21706  bl2ioo  21721  xrtgioo  21735  elcncf2  21818  cncfmet  21836  nmhmcn  22027  lmmbr  22121  lmmbr2  22122  iscfil2  22129  iscau2  22140  iscau3  22141  lmclim  22165  shft2rab  22339  sca2rab  22343  mbfeqalem  22475  mbfmulc2lem  22480  mbfmax  22482  mbfposr  22485  mbfimaopnlem  22488  mbfaddlem  22493  mbfsup  22497  mbfinf  22498  mbfinfOLD  22499  i1fmullem  22529  i1fmulclem  22537  i1fres  22540  itg1climres  22549  mbfi1fseqlem4  22553  ibllem  22599  ellimc2  22709  ellimc3  22711  limcflf  22713  cnplimc  22719  cnlimc  22720  dvreslem  22741  ply1remlem  22988  fta1glem2  22992  ofmulrt  23103  plyremlem  23125  ulm2  23205  mcubic  23638  cubic2  23639  dvdsflsumcom  23980  fsumvma  24004  fsumvma2  24005  vmasum  24007  logfaclbnd  24013  dchrelbas2  24028  dchrelbas3  24029  dchrelbas4  24034  lgsquadlem1  24145  lgsquadlem2  24146  colopp  24667  colhp  24668  nbgrael  24999  nbcusgra  25036  clwwlkn2  25348  el2wlkonotot1  25447  usg2spthonot0  25462  eupath2  25553  isblo2  26269  ubthlem1  26357  h2hlm  26468  pjpreeq  26886  elnlfn  27416  reuxfr4d  27961  feqmptdf  28098  fmptcof2  28099  funcnvmpt  28111  fpwrelmapffslem  28160  nndiffz1  28202  smatrcl  28461  ismntop  28669  itgeq12dv  28987  eulerpartlemgvv  29035  orvcgteel  29126  dfrdg2  30229  broutsideof3  30678  isfne4b  30782  filnetlem4  30822  poimirlem23  31667  poimirlem26  31670  poimirlem27  31671  heicant  31679  cnambfre  31693  itg2gt0cn  31701  ftc1anclem5  31725  areacirclem5  31740  isdrngo3  31902  isidlc  31952  prter3  32162  islshpsm  32255  islshpat  32292  lkrsc  32372  lfl1dim  32396  ldual1dim  32441  isat3  32582  glbconxN  32652  islln2  32785  islpln2  32810  islvol2  32854  cdlemg2cex  33867  diaglbN  34332  diblsmopel  34448  dihopelvalcpre  34525  xihopellsmN  34531  dihopellsm  34532  dihglbcpreN  34577  mapdval4N  34909  hdmapoc  35211  ellz1  35318  rmydioph  35575  rmxdioph  35577  expdiophlem1  35582  expdioph  35584  pw2f1ocnv  35598  dnwech  35612  sdrgacs  35766  pm14.123b  36414  rfcnpre1  36980  rfcnpre2  36992  rfcnpre3  36994  rfcnpre4  36995  climreeq  37265  funbrafv2b  38051  dfafn5a  38052  pfxeq  38335  pfxsuffeqwrdeq  38337  pfxsuff1eqwrdeq  38338  mgmhmpropd  38543  issubmgm2  38548  isrnghmmul  38651  rngcsect  38740  rngcsectALTV  38752  ringcsect  38791  ringcsectALTV  38815  elbigo2  39124
  Copyright terms: Public domain W3C validator