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

Theorem pm5.32da 623
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 424 . 2  |-  ( ph  ->  ( ps  ->  ( ch 
<->  th ) ) )
32pm5.32d 621 1  |-  ( ph  ->  ( ( ps  /\  ch )  <->  ( ps  /\  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  rexbida  2664  reubida  2833  rmobida  2838  mpteq12f  4226  reuhypd  4690  funbrfv2b  5710  dffn5  5711  eqfnfv2  5767  fmptco  5840  dff13  5943  mpt2eq123dva  6074  mpt2eq3dva  6077  fnwelem  6397  mpt2xopovel  6407  opiota  6471  riotabidva  6502  oeeui  6781  omabs  6826  qliftfun  6925  erovlem  6936  xpcomco  7134  pw2f1olem  7148  elfi2  7354  cardval2  7811  dfac2  7944  cflim3  8075  iundom2g  8348  fpwwe2lem8  8445  fpwwe2lem12  8449  ltexpi  8712  ordpipq  8752  axrrecex  8971  nnunb  10149  zrevaddcl  10253  qrevaddcl  10528  icoshft  10951  fznn  11045  fznnfl  11170  fz1isolem  11637  2shfti  11822  limsupgle  12198  ello12  12237  elo12  12248  isercoll  12388  sumeq2ii  12414  fsum2dlem  12481  bitsmod  12875  bitscmp  12877  pwsle  13641  imasleval  13693  acsfiel  13806  ismon2  13887  isepi2  13894  oppcsect  13926  subsubc  13977  funcpropd  14024  fullpropd  14044  fucsect  14096  setcsect  14171  pltval3  14351  ismgmid  14637  grpidpropd  14649  mhmpropd  14671  issubm2  14676  subgacs  14902  eqgid  14919  pgpfi2  15167  eqgabl  15381  iscyggen2  15418  cyggenod  15421  eldprd  15489  subgdmdprd  15519  dprd2d2  15529  rngpropd  15622  crngunit  15694  dvdsrpropd  15728  drngpropd  15789  issubrg3  15823  lsslss  15964  lsspropd  16020  lmhmpropd  16072  lbspropd  16098  aspval2  16332  znleval  16758  znunithash  16768  pjdm2  16861  bastop2  16982  elcls2  17061  neiptopreu  17120  maxlp  17133  restopn2  17163  iscnp3  17230  subbascn  17240  lmbr2  17245  kgencn  17509  kgencn2  17510  hauseqlcld  17599  txlm  17601  txkgen  17605  xkoptsub  17607  idqtop  17659  tgqtop  17665  qtopcld  17666  elmptrab  17780  flimopn  17928  fbflim  17929  fbflim2  17930  flimrest  17936  flffbas  17948  flftg  17949  cnflf  17955  cnflf2  17956  txflf  17959  isfcls  17962  fclsopn  17967  fclsbas  17974  fclsrest  17977  fcfnei  17988  cnfcf  17995  ptcmplem2  18005  tgphaus  18067  tsmssubm  18093  isucn2  18230  ismet2  18272  xblpnf  18327  blin  18344  blres  18351  elmopn2  18365  imasf1obl  18408  imasf1oxms  18409  prdsbl  18411  neibl  18421  metrest  18444  metcnp3  18460  metcnp  18461  metcnp2  18462  metcn  18463  txmetcnp  18467  txmetcn  18468  metuel2  18485  metucn  18490  ngppropd  18549  cnbl0  18679  cnblcld  18680  bl2ioo  18694  xrtgioo  18708  elcncf2  18791  cncfmet  18809  nmhmcn  18999  lmmbr  19082  lmmbr2  19083  iscfil2  19090  iscau2  19101  iscau3  19102  lmclim  19126  shft2rab  19271  sca2rab  19275  mbfeqalem  19401  mbfmulc2lem  19406  mbfmax  19408  mbfposr  19411  mbfimaopnlem  19414  mbfaddlem  19419  mbfsup  19423  mbfinf  19424  i1fmullem  19453  i1fmulclem  19461  i1fres  19464  itg1climres  19473  mbfi1fseqlem4  19477  ibllem  19523  ellimc2  19631  ellimc3  19633  limcflf  19635  cnplimc  19641  cnlimc  19642  dvreslem  19663  ply1remlem  19952  fta1glem2  19956  ofmulrt  20066  plyremlem  20088  ulm2  20168  mcubic  20554  cubic2  20555  dvdsflsumcom  20840  fsumvma  20864  fsumvma2  20865  vmasum  20867  logfaclbnd  20873  dchrelbas2  20888  dchrelbas3  20889  dchrelbas4  20894  lgsquadlem1  21005  lgsquadlem2  21006  nbgrael  21304  nbcusgra  21338  eupath2  21550  isblo2  22132  ubthlem1  22220  h2hlm  22331  pjpreeq  22748  elnlfn  23279  reuxfr4d  23821  feqmptdf  23917  fmptcof2  23918  funcnvmpt  23924  gsumpropd2lem  24049  itgeq12dv  24435  orvcgteel  24504  prodeq2ii  25018  dfrdg2  25176  preduz  25224  predfz  25227  broutsideof3  25774  itg2gt0cn  25960  areacirclem6  25987  isfne4b  26041  filnetlem4  26101  isdrngo3  26266  isidlc  26316  prter3  26422  ellz1  26516  rmydioph  26776  rmxdioph  26778  expdiophlem1  26783  expdioph  26785  pw2f1ocnv  26799  dnwech  26814  islinds2  26952  sdrgacs  27178  pm14.123b  27295  rfcnpre1  27358  rfcnpre2  27370  rfcnpre3  27372  rfcnpre4  27373  climreeq  27407  funbrafv2b  27692  dfafn5a  27693  islshpsm  29095  islshpat  29132  lkrsc  29212  lfl1dim  29236  ldual1dim  29281  isat3  29422  glbconxN  29492  islln2  29625  islpln2  29650  islvol2  29694  cdlemg2cex  30705  diaglbN  31170  diblsmopel  31286  dihopelvalcpre  31363  xihopellsmN  31369  dihopellsm  31370  dihglbcpreN  31415  mapdval4N  31747  hdmapoc  32049
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator