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

Theorem pm5.32da 641
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 434 . 2  |-  ( ph  ->  ( ps  ->  ( ch 
<->  th ) ) )
32pm5.32d 639 1  |-  ( ph  ->  ( ( ps  /\  ch )  <->  ( ps  /\  th ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  rexbida  2864  rexbidva  2865  reubida  3009  rmobida  3014  mpteq12f  4477  reuhypd  4628  xpdifid  5375  funbrfv2b  5846  dffn5  5847  eqfnfv2  5908  fmptco  5986  dff13  6081  riotabidva  6179  mpt2eq123dva  6257  mpt2eq3dva  6260  opiota  6744  fnwelem  6798  suppssr  6831  mpt2xopovel  6848  mpt2curryd  6899  oeeui  7152  omabs  7197  qliftfun  7296  erovlem  7307  xpcomco  7512  pw2f1olem  7526  elfi2  7776  cardval2  8273  dfac2  8412  cflim3  8543  iundom2g  8816  fpwwe2lem8  8916  fpwwe2lem12  8920  ltexpi  9183  ordpipq  9223  axrrecex  9442  nnunb  10687  zrevaddcl  10802  qrevaddcl  11087  icoshft  11525  fznn  11644  fznnfl  11819  fz1isolem  12333  swrdeq  12459  wrdeqswrdlsw  12462  2swrdeqwrdeq  12466  2swrd1eqwrdeq  12467  2swrd2eqwrdeq  12672  2shfti  12688  limsupgle  13074  ello12  13113  elo12  13124  isercoll  13264  sumeq2ii  13289  fsum2dlem  13356  bitsmod  13751  bitscmp  13753  pwsle  14550  imasleval  14599  acsfiel  14712  ismon2  14793  isepi2  14800  oppcsect  14832  subsubc  14883  funcpropd  14930  fullpropd  14950  fucsect  15002  setcsect  15077  pltval3  15257  ismgmid  15555  grpidpropd  15567  mhmpropd  15590  issubm2  15596  gsumpropd2lem  15625  subgacs  15836  eqgid  15853  pgpfi2  16227  eqgabl  16441  iscyggen2  16480  cyggenod  16483  eldprd  16609  eldprdOLD  16611  subgdmdprd  16654  dprd2d2  16666  rngpropd  16800  crngunit  16878  dvdsrpropd  16912  drngpropd  16983  issubrg3  17017  lsslss  17166  lsspropd  17222  lmhmpropd  17278  lbspropd  17304  aspval2  17541  znleval  18113  znunithash  18123  pjdm2  18262  islinds2  18368  bastop2  18732  elcls2  18811  neiptopreu  18870  maxlp  18884  restopn2  18914  iscnp3  18981  subbascn  18991  lmbr2  18996  kgencn  19262  kgencn2  19263  hauseqlcld  19352  txlm  19354  txkgen  19358  xkoptsub  19360  idqtop  19412  tgqtop  19418  qtopcld  19419  elmptrab  19533  flimopn  19681  fbflim  19682  fbflim2  19683  flimrest  19689  flffbas  19701  flftg  19702  cnflf  19708  cnflf2  19709  txflf  19712  isfcls  19715  fclsopn  19720  fclsbas  19727  fclsrest  19730  fcfnei  19741  cnfcf  19748  ptcmplem2  19758  tgphaus  19820  tsmssubm  19849  isucn2  19987  ismet2  20041  xblpnfps  20103  xblpnf  20104  blin  20129  blres  20139  elmopn2  20153  imasf1obl  20196  imasf1oxms  20197  prdsbl  20199  neibl  20209  metrest  20232  metcnp3  20248  metcnp  20249  metcnp2  20250  metcn  20251  txmetcnp  20255  txmetcn  20256  metuel2  20287  metucnOLD  20296  metucn  20297  ngppropd  20356  cnbl0  20486  cnblcld  20487  bl2ioo  20502  xrtgioo  20516  elcncf2  20599  cncfmet  20617  nmhmcn  20808  lmmbr  20902  lmmbr2  20903  iscfil2  20910  iscau2  20921  iscau3  20922  lmclim  20946  shft2rab  21124  sca2rab  21128  mbfeqalem  21254  mbfmulc2lem  21259  mbfmax  21261  mbfposr  21264  mbfimaopnlem  21267  mbfaddlem  21272  mbfsup  21276  mbfinf  21277  i1fmullem  21306  i1fmulclem  21314  i1fres  21317  itg1climres  21326  mbfi1fseqlem4  21330  ibllem  21376  ellimc2  21486  ellimc3  21488  limcflf  21490  cnplimc  21496  cnlimc  21497  dvreslem  21518  ply1remlem  21768  fta1glem2  21772  ofmulrt  21882  plyremlem  21904  ulm2  21984  mcubic  22376  cubic2  22377  dvdsflsumcom  22662  fsumvma  22686  fsumvma2  22687  vmasum  22689  logfaclbnd  22695  dchrelbas2  22710  dchrelbas3  22711  dchrelbas4  22716  lgsquadlem1  22827  lgsquadlem2  22828  nbgrael  23490  nbcusgra  23524  eupath2  23754  isblo2  24336  ubthlem1  24424  h2hlm  24535  pjpreeq  24954  elnlfn  25485  reuxfr4d  26027  feqmptdf  26130  fmptcof2  26131  funcnvmpt  26139  fpwrelmapffslem  26184  nndiffz1  26221  itgeq12dv  26857  eulerpartlemgvv  26904  orvcgteel  26995  prodeq2ii  27571  dfrdg2  27754  preduz  27806  predfz  27809  broutsideof3  28302  heicant  28575  cnambfre  28589  itg2gt0cn  28596  ftc1anclem5  28620  areacirclem5  28637  isfne4b  28691  filnetlem4  28751  isdrngo3  28914  isidlc  28964  prter3  29176  ellz1  29254  rmydioph  29512  rmxdioph  29514  expdiophlem1  29519  expdioph  29521  pw2f1ocnv  29535  dnwech  29550  sdrgacs  29707  pm14.123b  29829  rfcnpre1  29890  rfcnpre2  29902  rfcnpre3  29904  rfcnpre4  29905  climreeq  29935  funbrafv2b  30214  dfafn5a  30215  el2wlkonotot1  30542  usg2spthonot0  30557  clwwlkn2  30587  islshpsm  32964  islshpat  33001  lkrsc  33081  lfl1dim  33105  ldual1dim  33150  isat3  33291  glbconxN  33361  islln2  33494  islpln2  33519  islvol2  33563  cdlemg2cex  34574  diaglbN  35039  diblsmopel  35155  dihopelvalcpre  35232  xihopellsmN  35238  dihopellsm  35239  dihglbcpreN  35284  mapdval4N  35616  hdmapoc  35918
  Copyright terms: Public domain W3C validator