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  2485  reubida  2672  rmobida  2677  mpteq12f  4098  reuhypd  4486  funbrfv2b  5576  dffn5im  5577  eqfnfv2  5630  fndmin  5639  fniniseg  5652  rexsupp  5656  fmptco  5698  dff13  5785  riotabidva  5863  mpoeq123dva  5952  mpoeq3dva  5955  mpoxopovel  6260  qliftfun  6635  erovlem  6645  xpcomco  6844  elfi2  6989  ctssdccl  7128  ltexpi  7354  dfplpq2  7371  axprecex  7897  zrevaddcl  9321  qrevaddcl  9662  icoshft  10008  fznn  10107  shftdm  10849  2shfti  10858  sumeq2  11385  fsum3  11413  fsum2dlemstep  11460  prodeq2  11583  fprodseq  11609  gcdaddm  12003  grpidpropdg  12816  ismgmid  12819  mhmpropd  12884  issubm2  12891  eqgid  13131  eqgabl  13228  rngpropd  13270  iscrng2  13330  ringpropd  13353  crngpropd  13354  crngunit  13422  dvdsrpropdg  13458  issubrg3  13555  lsslss  13658  lsspropdg  13708  bastop2  13981  restopn2  14080  iscnp3  14100  lmbr2  14111  txlm  14176  ismet2  14251  xblpnfps  14295  xblpnf  14296  blininf  14321  blres  14331  elmopn2  14346  neibl  14388  metrest  14403  metcnp3  14408  metcnp  14409  metcnp2  14410  metcn  14411  txmetcn  14416  cnbl0  14431  cnblcld  14432  bl2ioo  14439  elcncf2  14458  cncfmet  14476  cnlimc  14538