Theorem pm5.32da 452

Description: Distribution of implication over biconditional (deduction form). (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 115	. 2 |- ( ph -> ( ps -> ( ch <-> th ) ) )
3	2	pm5.32d 450	1 |- ( ph -> ( ( ps /\ ch ) <-> ( ps /\ th ) ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  rexbida  2489  reubida  2676  rmobida  2681  mpteq12f  4110  reuhypd  4503  funbrfv2b  5602  dffn5im  5603  eqfnfv2  5657  fndmin  5666  fniniseg  5679  rexsupp  5683  fmptco  5725  dff13  5812  riotabidva  5891  mpoeq123dva  5980  mpoeq3dva  5983  mpoxopovel  6296  qliftfun  6673  erovlem  6683  xpcomco  6882  pw2f1odclem  6892  elfi2  7033  ctssdccl  7172  ltexpi  7399  dfplpq2  7416  axprecex  7942  zrevaddcl  9370  qrevaddcl  9712  icoshft  10059  fznn  10158  shftdm  10969  2shfti  10978  sumeq2  11505  fsum3  11533  fsum2dlemstep  11580  prodeq2  11703  fprodseq  11729  gcdaddm  12124  grpidpropdg  12960  ismgmid  12963  gsumpropd2  12979  mhmpropd  13041  issubm2  13048  eqgid  13299  eqgabl  13403  rngpropd  13454  iscrng2  13514  ringpropd  13537  crngpropd  13538  crngunit  13610  dvdsrpropdg  13646  issubrg3  13746  lsslss  13880  lsspropdg  13930  znleval  14152  bastop2  14263  restopn2  14362  iscnp3  14382  lmbr2  14393  txlm  14458  ismet2  14533  xblpnfps  14577  xblpnf  14578  blininf  14603  blres  14613  elmopn2  14628  neibl  14670  metrest  14685  metcnp3  14690  metcnp  14691  metcnp2  14692  metcn  14693  txmetcn  14698  cnbl0  14713  cnblcld  14714  bl2ioo  14729  elcncf2  14753  cncfmet  14771  cnlimc  14851  lgsquadlem1  15234  lgsquadlem2  15235  2lgslem1a  15245