Theorem pm5.32da 448

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 114	. 2 |- ( ph -> ( ps -> ( ch <-> th ) ) )
3	2	pm5.32d 446	1 |- ( ph -> ( ( ps /\ ch ) <-> ( ps /\ th ) ) )

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  rexbida  2461  reubida  2647  rmobida  2652  mpteq12f  4062  reuhypd  4449  funbrfv2b  5531  dffn5im  5532  eqfnfv2  5584  fndmin  5592  fniniseg  5605  rexsupp  5609  fmptco  5651  dff13  5736  riotabidva  5814  mpoeq123dva  5903  mpoeq3dva  5906  mpoxopovel  6209  qliftfun  6583  erovlem  6593  xpcomco  6792  elfi2  6937  ctssdccl  7076  ltexpi  7278  dfplpq2  7295  axprecex  7821  zrevaddcl  9241  qrevaddcl  9582  icoshft  9926  fznn  10024  shftdm  10764  2shfti  10773  sumeq2  11300  fsum3  11328  fsum2dlemstep  11375  prodeq2  11498  fprodseq  11524  gcdaddm  11917  grpidpropdg  12605  ismgmid  12608  bastop2  12724  restopn2  12823  iscnp3  12843  lmbr2  12854  txlm  12919  ismet2  12994  xblpnfps  13038  xblpnf  13039  blininf  13064  blres  13074  elmopn2  13089  neibl  13131  metrest  13146  metcnp3  13151  metcnp  13152  metcnp2  13153  metcn  13154  txmetcn  13159  cnbl0  13174  cnblcld  13175  bl2ioo  13182  elcncf2  13201  cncfmet  13219  cnlimc  13281