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  2525  reubida  2713  rmobida  2719  mpteq12f  4163  reuhypd  4561  funbrfv2b  5677  dffn5im  5678  eqfnfv2  5732  fndmin  5741  fniniseg  5754  rexsupp  5758  fmptco  5800  dff13  5891  riotabidva  5971  mpoeq123dva  6064  mpoeq3dva  6067  mpoxopovel  6385  qliftfun  6762  erovlem  6772  xpcomco  6981  pw2f1odclem  6991  elfi2  7135  ctssdccl  7274  ltexpi  7520  dfplpq2  7537  axprecex  8063  zrevaddcl  9493  qrevaddcl  9835  icoshft  10182  fznn  10281  pfxeq  11223  pfxsuffeqwrdeq  11225  pfxsuff1eqwrdeq  11226  shftdm  11328  2shfti  11337  sumeq2  11865  fsum3  11893  fsum2dlemstep  11940  prodeq2  12063  fprodseq  12089  bitsmod  12462  bitscmp  12464  gcdaddm  12500  grpidpropdg  13402  ismgmid  13405  gsumpropd2  13421  mhmpropd  13494  issubm2  13501  eqgid  13758  eqgabl  13862  rngpropd  13913  iscrng2  13973  ringpropd  13996  crngpropd  13997  crngunit  14069  dvdsrpropdg  14105  issubrg3  14205  lsslss  14339  lsspropdg  14389  znleval  14611  bastop2  14752  restopn2  14851  iscnp3  14871  lmbr2  14882  txlm  14947  ismet2  15022  xblpnfps  15066  xblpnf  15067  blininf  15092  blres  15102  elmopn2  15117  neibl  15159  metrest  15174  metcnp3  15179  metcnp  15180  metcnp2  15181  metcn  15182  txmetcn  15187  cnbl0  15202  cnblcld  15203  bl2ioo  15218  elcncf2  15242  cncfmet  15260  cnlimc  15340  lgsquadlem1  15750  lgsquadlem2  15751  2lgslem1a  15761