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  2968  rexbidva  2970  reubida  3044  rmobida  3049  mpteq12f  4523  reuhypd  4674  xpdifid  5433  funbrfv2b  5910  dffn5  5911  eqfnfv2  5974  fmptco  6052  dff13  6152  riotabidva  6260  mpt2eq123dva  6340  mpt2eq3dva  6343  opiota  6840  fnwelem  6895  suppssr  6928  mpt2xopovel  6945  mpt2curryd  6995  oeeui  7248  omabs  7293  qliftfun  7393  erovlem  7404  xpcomco  7604  pw2f1olem  7618  elfi2  7870  cardval2  8368  dfac2  8507  cflim3  8638  iundom2g  8911  fpwwe2lem8  9011  fpwwe2lem12  9015  ltexpi  9276  ordpipq  9316  axrrecex  9536  nnunb  10787  zrevaddcl  10904  qrevaddcl  11200  icoshft  11638  fznn  11743  fznnfl  11953  fz1isolem  12472  swrdeq  12630  wrdeqswrdlsw  12633  2swrdeqwrdeq  12637  2swrd1eqwrdeq  12638  2swrd2eqwrdeq  12850  2shfti  12872  limsupgle  13259  ello12  13298  elo12  13309  isercoll  13449  sumeq2ii  13474  fsum2dlem  13544  bitsmod  13941  bitscmp  13943  pwsle  14743  imasleval  14792  acsfiel  14905  ismon2  14986  isepi2  14993  oppcsect  15025  subsubc  15076  funcpropd  15123  fullpropd  15143  fucsect  15195  setcsect  15270  pltval3  15450  ismgmid  15748  grpidpropd  15760  mhmpropd  15783  issubm2  15789  gsumpropd2lem  15818  subgacs  16031  eqgid  16048  pgpfi2  16422  eqgabl  16636  iscyggen2  16675  cyggenod  16678  eldprd  16826  eldprdOLD  16828  subgdmdprd  16871  dprd2d2  16883  rngpropd  17017  crngunit  17095  dvdsrpropd  17129  drngpropd  17206  issubrg3  17240  lsslss  17390  lsspropd  17446  lmhmpropd  17502  lbspropd  17528  aspval2  17767  znleval  18360  znunithash  18370  pjdm2  18509  islinds2  18615  bastop2  19262  elcls2  19341  neiptopreu  19400  maxlp  19414  restopn2  19444  iscnp3  19511  subbascn  19521  lmbr2  19526  kgencn  19792  kgencn2  19793  hauseqlcld  19882  txlm  19884  txkgen  19888  xkoptsub  19890  idqtop  19942  tgqtop  19948  qtopcld  19949  elmptrab  20063  flimopn  20211  fbflim  20212  fbflim2  20213  flimrest  20219  flffbas  20231  flftg  20232  cnflf  20238  cnflf2  20239  txflf  20242  isfcls  20245  fclsopn  20250  fclsbas  20257  fclsrest  20260  fcfnei  20271  cnfcf  20278  ptcmplem2  20288  tgphaus  20350  tsmssubm  20379  isucn2  20517  ismet2  20571  xblpnfps  20633  xblpnf  20634  blin  20659  blres  20669  elmopn2  20683  imasf1obl  20726  imasf1oxms  20727  prdsbl  20729  neibl  20739  metrest  20762  metcnp3  20778  metcnp  20779  metcnp2  20780  metcn  20781  txmetcnp  20785  txmetcn  20786  metuel2  20817  metucnOLD  20826  metucn  20827  ngppropd  20886  cnbl0  21016  cnblcld  21017  bl2ioo  21032  xrtgioo  21046  elcncf2  21129  cncfmet  21147  nmhmcn  21338  lmmbr  21432  lmmbr2  21433  iscfil2  21440  iscau2  21451  iscau3  21452  lmclim  21476  shft2rab  21654  sca2rab  21658  mbfeqalem  21784  mbfmulc2lem  21789  mbfmax  21791  mbfposr  21794  mbfimaopnlem  21797  mbfaddlem  21802  mbfsup  21806  mbfinf  21807  i1fmullem  21836  i1fmulclem  21844  i1fres  21847  itg1climres  21856  mbfi1fseqlem4  21860  ibllem  21906  ellimc2  22016  ellimc3  22018  limcflf  22020  cnplimc  22026  cnlimc  22027  dvreslem  22048  ply1remlem  22298  fta1glem2  22302  ofmulrt  22412  plyremlem  22434  ulm2  22514  mcubic  22906  cubic2  22907  dvdsflsumcom  23192  fsumvma  23216  fsumvma2  23217  vmasum  23219  logfaclbnd  23225  dchrelbas2  23240  dchrelbas3  23241  dchrelbas4  23246  lgsquadlem1  23357  lgsquadlem2  23358  nbgrael  24102  nbcusgra  24139  clwwlkn2  24451  el2wlkonotot1  24550  usg2spthonot0  24565  eupath2  24656  isblo2  25374  ubthlem1  25462  h2hlm  25573  pjpreeq  25992  elnlfn  26523  reuxfr4d  27065  feqmptdf  27173  fmptcof2  27174  funcnvmpt  27182  fpwrelmapffslem  27227  nndiffz1  27264  ismntop  27644  itgeq12dv  27908  eulerpartlemgvv  27955  orvcgteel  28046  prodeq2ii  28622  dfrdg2  28805  preduz  28857  predfz  28860  broutsideof3  29353  heicant  29626  cnambfre  29640  itg2gt0cn  29647  ftc1anclem5  29671  areacirclem5  29688  isfne4b  29742  filnetlem4  29802  isdrngo3  29965  isidlc  30015  prter3  30227  ellz1  30304  rmydioph  30560  rmxdioph  30562  expdiophlem1  30567  expdioph  30569  pw2f1ocnv  30583  dnwech  30598  sdrgacs  30755  pm14.123b  30911  rfcnpre1  30972  rfcnpre2  30984  rfcnpre3  30986  rfcnpre4  30987  climreeq  31155  funbrafv2b  31711  dfafn5a  31712  islshpsm  33777  islshpat  33814  lkrsc  33894  lfl1dim  33918  ldual1dim  33963  isat3  34104  glbconxN  34174  islln2  34307  islpln2  34332  islvol2  34376  cdlemg2cex  35387  diaglbN  35852  diblsmopel  35968  dihopelvalcpre  36045  xihopellsmN  36051  dihopellsm  36052  dihglbcpreN  36097  mapdval4N  36429  hdmapoc  36731
  Copyright terms: Public domain W3C validator