Theorem pm5.32da 673

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

Step	Hyp	Ref	Expression
1		pm5.32da.1	. . 3 |- ( ( ph /\ ps ) -> ( ch <-> th ) )
2	1	ex 450	. 2 |- ( ph -> ( ps -> ( ch <-> th ) ) )
3	2	pm5.32d 671	1 |- ( ph -> ( ( ps /\ ch ) <-> ( ps /\ th ) ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  rexbida  3047  rexbidva  3049  reubida  3124  rmobida  3129  mpteq12f  4731  reuhypd  4895  xpdifid  5562  funbrfv2b  6240  dffn5  6241  feqmptdf  6251  eqfnfv2  6312  fmptco  6396  dff13  6512  riotabidva  6627  mpt2eq123dva  6716  mpt2eq3dva  6719  opiota  7229  fnwelem  7292  suppssr  7326  mpt2xopovel  7346  mpt2curryd  7395  oeeui  7682  omabs  7727  qliftfun  7832  erovlem  7843  xpcomco  8050  pw2f1olem  8064  elfi2  8320  cardval2  8817  dfac2  8953  cflim3  9084  iundom2g  9362  fpwwe2lem8  9459  fpwwe2lem12  9463  ltexpi  9724  ordpipq  9764  axrrecex  9984  nnunb  11288  zrevaddcl  11422  qrevaddcl  11810  icoshft  12294  fznn  12408  preduz  12461  predfz  12464  fznnfl  12661  fz1isolem  13245  swrdeq  13444  2swrdeqwrdeq  13453  2swrd1eqwrdeq  13454  2swrd2eqwrdeq  13696  eqwrds3  13704  2shfti  13820  limsupgle  14208  ello12  14247  elo12  14258  isercoll  14398  sumeq2ii  14423  fsum2dlem  14501  prodeq2ii  14643  bitsmod  15158  bitscmp  15160  pwsle  16152  imasleval  16201  acsfiel  16315  ismon2  16394  isepi2  16401  oppcsect  16438  subsubc  16513  funcpropd  16560  fullpropd  16580  fucsect  16632  setcsect  16739  pltval3  16967  grpidpropd  17261  ismgmid  17264  gsumpropd2lem  17273  mhmpropd  17341  issubm2  17348  subgacs  17629  eqgid  17646  pgpfi2  18021  eqgabl  18240  iscyggen2  18283  cyggenod  18286  eldprd  18403  subgdmdprd  18433  dprd2d2  18443  ringpropd  18582  crngunit  18662  dvdsrpropd  18696  drngpropd  18774  issubrg3  18808  lsslss  18961  lsspropd  19017  lmhmpropd  19073  lbspropd  19099  aspval2  19347  znleval  19903  znunithash  19913  pjdm2  20055  islinds2  20152  bastop2  20798  elcls2  20878  neiptopreu  20937  maxlp  20951  restopn2  20981  iscnp3  21048  subbascn  21058  lmbr2  21063  kgencn  21359  kgencn2  21360  hauseqlcld  21449  txlm  21451  txkgen  21455  xkoptsub  21457  idqtop  21509  tgqtop  21515  qtopcld  21516  elmptrab  21630  flimopn  21779  fbflim  21780  fbflim2  21781  flimrest  21787  flffbas  21799  flftg  21800  cnflf  21806  cnflf2  21807  txflf  21810  isfcls  21813  fclsopn  21818  fclsbas  21825  fclsrest  21828  fcfnei  21839  cnfcf  21846  ptcmplem2  21857  tgphaus  21920  tsmssubm  21946  isucn2  22083  ismet2  22138  xblpnfps  22200  xblpnf  22201  blin  22226  blres  22236  elmopn2  22250  imasf1obl  22293  imasf1oxms  22294  prdsbl  22296  neibl  22306  metrest  22329  metcnp3  22345  metcnp  22346  metcnp2  22347  metcn  22348  txmetcnp  22352  txmetcn  22353  metuel2  22370  metucn  22376  ngppropd  22441  cnbl0  22577  cnblcld  22578  bl2ioo  22595  xrtgioo  22609  elcncf2  22693  cncfmet  22711  nmhmcn  22920  lmmbr  23056  lmmbr2  23057  iscfil2  23064  iscau2  23075  iscau3  23076  lmclim  23101  shft2rab  23276  sca2rab  23280  mbfeqalem  23409  mbfmulc2lem  23414  mbfmax  23416  mbfposr  23419  mbfimaopnlem  23422  mbfaddlem  23427  mbfsup  23431  mbfinf  23432  i1fmullem  23461  i1fmulclem  23469  i1fres  23472  itg1climres  23481  mbfi1fseqlem4  23485  ibllem  23531  ellimc2  23641  ellimc3  23643  limcflf  23645  cnplimc  23651  cnlimc  23652  dvreslem  23673  ply1remlem  23922  fta1glem2  23926  ofmulrt  24037  plyremlem  24059  ulm2  24139  mcubic  24574  cubic2  24575  dvdsflsumcom  24914  fsumvma  24938  fsumvma2  24939  vmasum  24941  logfaclbnd  24947  dchrelbas2  24962  dchrelbas3  24963  dchrelbas4  24968  lgsquadlem1  25105  lgsquadlem2  25106  2lgslem1a  25116  colopp  25661  colhp  25662  nbgrel  26238  umgr2v2enb1  26422  upgriswlk  26537  wspthsnwspthsnon  26811  elwwlks2on  26852  elwwlks2  26861  elwspths2spth  26862  isclwwlksnx  26889  clwwlksn2  26910  eupth2lems  27098  fusgr2wsp2nb  27198  isblo2  27638  ubthlem1  27726  h2hlm  27837  pjpreeq  28257  elnlfn  28787  reuxfr4d  29330  fmptcof2  29457  funcnvmpt  29468  fpwrelmapffslem  29507  nndiffz1  29548  smatrcl  29862  ismntop  30070  itgeq12dv  30388  eulerpartlemgvv  30438  orvcgteel  30529  reprinrn  30696  reprdifc  30705  dfrdg2  31701  broutsideof3  32233  isfne4b  32336  filnetlem4  32376  uncf  33388  poimirlem23  33432  poimirlem26  33435  poimirlem27  33436  heicant  33444  cnambfre  33458  itg2gt0cn  33465  ftc1anclem5  33489  areacirclem5  33504  isdrngo3  33758  isidlc  33814  prter3  34167  islshpsm  34267  islshpat  34304  lkrsc  34384  lfl1dim  34408  ldual1dim  34453  isat3  34594  glbconxN  34664  islln2  34797  islpln2  34822  islvol2  34866  cdlemg2cex  35879  diaglbN  36344  diblsmopel  36460  dihopelvalcpre  36537  xihopellsmN  36543  dihopellsm  36544  dihglbcpreN  36589  mapdval4N  36921  hdmapoc  37223  ellz1  37330  rmydioph  37581  rmxdioph  37583  expdiophlem1  37588  expdioph  37590  pw2f1ocnv  37604  dnwech  37618  sdrgacs  37771  rfovcnvf1od  38298  k0004lem3  38447  pm14.123b  38627  rfcnpre1  39178  rfcnpre2  39190  rfcnpre3  39192  rfcnpre4  39193  climreeq  39845  funbrafv2b  41239  dfafn5a  41240  pfxeq  41404  pfxsuffeqwrdeq  41406  pfxsuff1eqwrdeq  41407  mgmhmpropd  41785  issubmgm2  41790  isrnghmmul  41893  rngcsect  41980  rngcsectALTV  41992  ringcsect  42031  ringcsectALTV  42055  elbigo2  42346