Theorem pm5.32da 447

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 445	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  2430  reubida  2610  rmobida  2615  mpteq12f  4003  reuhypd  4387  funbrfv2b  5459  dffn5im  5460  eqfnfv2  5512  fndmin  5520  fniniseg  5533  rexsupp  5537  fmptco  5579  dff13  5662  riotabidva  5739  mpoeq123dva  5825  mpoeq3dva  5828  mpoxopovel  6131  qliftfun  6504  erovlem  6514  xpcomco  6713  elfi2  6853  ctssdccl  6989  ltexpi  7138  dfplpq2  7155  axprecex  7681  zrevaddcl  9097  qrevaddcl  9429  icoshft  9766  fznn  9862  shftdm  10587  2shfti  10596  sumeq2  11121  fsum3  11149  fsum2dlemstep  11196  prodeq2  11319  gcdaddm  11661  bastop2  12242  restopn2  12341  iscnp3  12361  lmbr2  12372  txlm  12437  ismet2  12512  xblpnfps  12556  xblpnf  12557  blininf  12582  blres  12592  elmopn2  12607  neibl  12649  metrest  12664  metcnp3  12669  metcnp  12670  metcnp2  12671  metcn  12672  txmetcn  12677  cnbl0  12692  cnblcld  12693  bl2ioo  12700  elcncf2  12719  cncfmet  12737  cnlimc  12799