MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm5.32da 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
Assertion
Ref Expression
pm5.32da

Proof of Theorem pm5.32da
StepHypRef Expression
1 pm5.32da.1 . . 3
21ex 434 . 2
32pm5.32d 639 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369
This theorem is referenced by:  rexbida  2963  rexbidva  2965  reubida  3040  rmobida  3045  mpteq12f  4528  reuhypd  4679  xpdifid  5440  funbrfv2b  5917  dffn5  5918  eqfnfv2  5982  fmptco  6064  dff13  6166  riotabidva  6274  mpt2eq123dva  6358  mpt2eq3dva  6361  opiota  6859  fnwelem  6915  suppssr  6950  mpt2xopovel  6967  mpt2curryd  7017  oeeui  7270  omabs  7315  qliftfun  7415  erovlem  7426  xpcomco  7627  pw2f1olem  7641  elfi2  7894  cardval2  8393  dfac2  8532  cflim3  8663  iundom2g  8936  fpwwe2lem8  9036  fpwwe2lem12  9040  ltexpi  9301  ordpipq  9341  axrrecex  9561  nnunb  10816  zrevaddcl  10934  qrevaddcl  11233  icoshft  11671  fznn  11776  fznnfl  11989  fz1isolem  12510  swrdeq  12671  wrdeqswrdlsw  12674  2swrdeqwrdeq  12678  2swrd1eqwrdeq  12679  2swrd2eqwrdeq  12891  2shfti  12913  limsupgle  13300  ello12  13339  elo12  13350  isercoll  13490  sumeq2ii  13515  fsum2dlem  13585  prodeq2ii  13720  bitsmod  14086  bitscmp  14088  pwsle  14889  imasleval  14938  acsfiel  15051  ismon2  15129  isepi2  15136  oppcsect  15168  subsubc  15222  funcpropd  15269  fullpropd  15289  fucsect  15341  setcsect  15416  pltval3  15597  grpidpropd  15888  ismgmid  15891  gsumpropd2lem  15900  mhmpropd  15972  issubm2  15979  subgacs  16236  eqgid  16253  pgpfi2  16626  eqgabl  16843  iscyggen2  16884  cyggenod  16887  eldprd  17035  eldprdOLD  17037  subgdmdprd  17081  dprd2d2  17093  ringpropd  17230  crngunit  17311  dvdsrpropd  17345  drngpropd  17423  issubrg3  17457  lsslss  17607  lsspropd  17663  lmhmpropd  17719  lbspropd  17745  aspval2  17996  znleval  18593  znunithash  18603  pjdm2  18742  islinds2  18848  bastop2  19496  elcls2  19575  neiptopreu  19634  maxlp  19648  restopn2  19678  iscnp3  19745  subbascn  19755  lmbr2  19760  kgencn  20057  kgencn2  20058  hauseqlcld  20147  txlm  20149  txkgen  20153  xkoptsub  20155  idqtop  20207  tgqtop  20213  qtopcld  20214  elmptrab  20328  flimopn  20476  fbflim  20477  fbflim2  20478  flimrest  20484  flffbas  20496  flftg  20497  cnflf  20503  cnflf2  20504  txflf  20507  isfcls  20510  fclsopn  20515  fclsbas  20522  fclsrest  20525  fcfnei  20536  cnfcf  20543  ptcmplem2  20553  tgphaus  20615  tsmssubm  20644  isucn2  20782  ismet2  20836  xblpnfps  20898  xblpnf  20899  blin  20924  blres  20934  elmopn2  20948  imasf1obl  20991  imasf1oxms  20992  prdsbl  20994  neibl  21004  metrest  21027  metcnp3  21043  metcnp  21044  metcnp2  21045  metcn  21046  txmetcnp  21050  txmetcn  21051  metuel2  21082  metucnOLD  21091  metucn  21092  ngppropd  21151  cnbl0  21281  cnblcld  21282  bl2ioo  21297  xrtgioo  21311  elcncf2  21394  cncfmet  21412  nmhmcn  21603  lmmbr  21697  lmmbr2  21698  iscfil2  21705  iscau2  21716  iscau3  21717  lmclim  21741  shft2rab  21919  sca2rab  21923  mbfeqalem  22049  mbfmulc2lem  22054  mbfmax  22056  mbfposr  22059  mbfimaopnlem  22062  mbfaddlem  22067  mbfsup  22071  mbfinf  22072  i1fmullem  22101  i1fmulclem  22109  i1fres  22112  itg1climres  22121  mbfi1fseqlem4  22125  ibllem  22171  ellimc2  22281  ellimc3  22283  limcflf  22285  cnplimc  22291  cnlimc  22292  dvreslem  22313  ply1remlem  22563  fta1glem2  22567  ofmulrt  22678  plyremlem  22700  ulm2  22780  mcubic  23178  cubic2  23179  dvdsflsumcom  23464  fsumvma  23488  fsumvma2  23489  vmasum  23491  logfaclbnd  23497  dchrelbas2  23512  dchrelbas3  23513  dchrelbas4  23518  lgsquadlem1  23629  lgsquadlem2  23630  nbgrael  24426  nbcusgra  24463  clwwlkn2  24775  el2wlkonotot1  24874  usg2spthonot0  24889  eupath2  24980  isblo2  25698  ubthlem1  25786  h2hlm  25897  pjpreeq  26316  elnlfn  26847  reuxfr4d  27389  feqmptdf  27501  fmptcof2  27502  funcnvmpt  27510  fpwrelmapffslem  27555  nndiffz1  27596  ismntop  28004  itgeq12dv  28268  eulerpartlemgvv  28315  orvcgteel  28406  dfrdg2  29228  preduz  29280  predfz  29283  broutsideof3  29776  heicant  30049  cnambfre  30063  itg2gt0cn  30070  ftc1anclem5  30094  areacirclem5  30111  isfne4b  30159  filnetlem4  30199  isdrngo3  30362  isidlc  30412  prter3  30623  ellz1  30700  rmydioph  30956  rmxdioph  30958  expdiophlem1  30963  expdioph  30965  pw2f1ocnv  30979  dnwech  30994  sdrgacs  31150  pm14.123b  31333  rfcnpre1  31394  rfcnpre2  31406  rfcnpre3  31408  rfcnpre4  31409  climreeq  31619  funbrafv2b  32244  dfafn5a  32245  mgmhmpropd  32473  issubmgm2  32478  isrnghmmul  32699  rngcsect  32788  rngcsectOLD  32800  ringcsect  32839  ringcsectOLD  32863  islshpsm  34705  islshpat  34742  lkrsc  34822  lfl1dim  34846  ldual1dim  34891  isat3  35032  glbconxN  35102  islln2  35235  islpln2  35260  islvol2  35304  cdlemg2cex  36317  diaglbN  36782  diblsmopel  36898  dihopelvalcpre  36975  xihopellsmN  36981  dihopellsm  36982  dihglbcpreN  37027  mapdval4N  37359  hdmapoc  37661
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
  Copyright terms: Public domain W3C validator