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  2725  reubida  2898  rmobida  2903  mpteq12f  4363  reuhypd  4514  xpdifid  5261  funbrfv2b  5731  dffn5  5732  eqfnfv2  5793  fmptco  5871  dff13  5966  riotabidva  6064  mpt2eq123dva  6142  mpt2eq3dva  6145  opiota  6628  fnwelem  6682  suppssr  6715  mpt2xopovel  6732  oeeui  7033  omabs  7078  qliftfun  7177  erovlem  7188  xpcomco  7393  pw2f1olem  7407  elfi2  7656  cardval2  8153  dfac2  8292  cflim3  8423  iundom2g  8696  fpwwe2lem8  8796  fpwwe2lem12  8800  ltexpi  9063  ordpipq  9103  axrrecex  9322  nnunb  10567  zrevaddcl  10682  qrevaddcl  10967  icoshft  11399  fznn  11518  fznnfl  11693  fz1isolem  12206  swrdeq  12332  wrdeqswrdlsw  12335  2swrdeqwrdeq  12339  2swrd1eqwrdeq  12340  2swrd2eqwrdeq  12545  2shfti  12561  limsupgle  12947  ello12  12986  elo12  12997  isercoll  13137  sumeq2ii  13162  fsum2dlem  13229  bitsmod  13624  bitscmp  13626  pwsle  14422  imasleval  14471  acsfiel  14584  ismon2  14665  isepi2  14672  oppcsect  14704  subsubc  14755  funcpropd  14802  fullpropd  14822  fucsect  14874  setcsect  14949  pltval3  15129  ismgmid  15427  grpidpropd  15439  mhmpropd  15462  issubm2  15467  gsumpropd2lem  15496  subgacs  15707  eqgid  15724  pgpfi2  16096  eqgabl  16310  iscyggen2  16349  cyggenod  16352  eldprd  16474  eldprdOLD  16476  subgdmdprd  16519  dprd2d2  16531  rngpropd  16664  crngunit  16742  dvdsrpropd  16776  drngpropd  16837  issubrg3  16871  lsslss  17019  lsspropd  17075  lmhmpropd  17131  lbspropd  17157  aspval2  17394  znleval  17962  znunithash  17972  pjdm2  18111  islinds2  18217  bastop2  18574  elcls2  18653  neiptopreu  18712  maxlp  18726  restopn2  18756  iscnp3  18823  subbascn  18833  lmbr2  18838  kgencn  19104  kgencn2  19105  hauseqlcld  19194  txlm  19196  txkgen  19200  xkoptsub  19202  idqtop  19254  tgqtop  19260  qtopcld  19261  elmptrab  19375  flimopn  19523  fbflim  19524  fbflim2  19525  flimrest  19531  flffbas  19543  flftg  19544  cnflf  19550  cnflf2  19551  txflf  19554  isfcls  19557  fclsopn  19562  fclsbas  19569  fclsrest  19572  fcfnei  19583  cnfcf  19590  ptcmplem2  19600  tgphaus  19662  tsmssubm  19691  isucn2  19829  ismet2  19883  xblpnfps  19945  xblpnf  19946  blin  19971  blres  19981  elmopn2  19995  imasf1obl  20038  imasf1oxms  20039  prdsbl  20041  neibl  20051  metrest  20074  metcnp3  20090  metcnp  20091  metcnp2  20092  metcn  20093  txmetcnp  20097  txmetcn  20098  metuel2  20129  metucnOLD  20138  metucn  20139  ngppropd  20198  cnbl0  20328  cnblcld  20329  bl2ioo  20344  xrtgioo  20358  elcncf2  20441  cncfmet  20459  nmhmcn  20650  lmmbr  20744  lmmbr2  20745  iscfil2  20752  iscau2  20763  iscau3  20764  lmclim  20788  shft2rab  20966  sca2rab  20970  mbfeqalem  21095  mbfmulc2lem  21100  mbfmax  21102  mbfposr  21105  mbfimaopnlem  21108  mbfaddlem  21113  mbfsup  21117  mbfinf  21118  i1fmullem  21147  i1fmulclem  21155  i1fres  21158  itg1climres  21167  mbfi1fseqlem4  21171  ibllem  21217  ellimc2  21327  ellimc3  21329  limcflf  21331  cnplimc  21337  cnlimc  21338  dvreslem  21359  ply1remlem  21609  fta1glem2  21613  ofmulrt  21723  plyremlem  21745  ulm2  21825  mcubic  22217  cubic2  22218  dvdsflsumcom  22503  fsumvma  22527  fsumvma2  22528  vmasum  22530  logfaclbnd  22536  dchrelbas2  22551  dchrelbas3  22552  dchrelbas4  22557  lgsquadlem1  22668  lgsquadlem2  22669  nbgrael  23288  nbcusgra  23322  eupath2  23552  isblo2  24134  ubthlem1  24222  h2hlm  24333  pjpreeq  24752  elnlfn  25283  reuxfr4d  25825  feqmptdf  25929  fmptcof2  25930  funcnvmpt  25938  fpwrelmapffslem  25983  nndiffz1  26026  itgeq12dv  26664  eulerpartlemgvv  26711  orvcgteel  26802  prodeq2ii  27377  dfrdg2  27560  preduz  27612  predfz  27615  broutsideof3  28108  heicant  28379  cnambfre  28393  itg2gt0cn  28400  ftc1anclem5  28424  areacirclem5  28441  isfne4b  28495  filnetlem4  28555  isdrngo3  28718  isidlc  28768  prter3  28980  ellz1  29058  rmydioph  29316  rmxdioph  29318  expdiophlem1  29323  expdioph  29325  pw2f1ocnv  29339  dnwech  29354  sdrgacs  29511  pm14.123b  29633  rfcnpre1  29694  rfcnpre2  29706  rfcnpre3  29708  rfcnpre4  29709  climreeq  29739  funbrafv2b  30018  dfafn5a  30019  el2wlkonotot1  30346  usg2spthonot0  30361  clwwlkn2  30391  islshpsm  32465  islshpat  32502  lkrsc  32582  lfl1dim  32606  ldual1dim  32651  isat3  32792  glbconxN  32862  islln2  32995  islpln2  33020  islvol2  33064  cdlemg2cex  34075  diaglbN  34540  diblsmopel  34656  dihopelvalcpre  34733  xihopellsmN  34739  dihopellsm  34740  dihglbcpreN  34785  mapdval4N  35117  hdmapoc  35419
  Copyright terms: Public domain W3C validator