Theorem pm5.32da 440

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

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

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  rexbida  2375  reubida  2548  rmobida  2553  mpteq12f  3918  reuhypd  4293  funbrfv2b  5349  dffn5im  5350  eqfnfv2  5398  fndmin  5406  fniniseg  5419  rexsupp  5423  fmptco  5464  dff13  5547  riotabidva  5624  mpt2eq123dva  5710  mpt2eq3dva  5713  mpt2xopovel  6006  qliftfun  6374  erovlem  6384  xpcomco  6542  ltexpi  6896  dfplpq2  6913  axprecex  7415  zrevaddcl  8800  qrevaddcl  9129  icoshft  9407  fznn  9503  shftdm  10256  2shfti  10265  sumeq2  10748  fisum  10778  fsum2dlemstep  10828  gcdaddm  11253  elcncf2  11630