Theorem pm5.32da 440

Description: Distribution of implication over biconditional (deduction rule). (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  2364  reubida  2536  rmobida  2541  mpteq12f  3866  reuhypd  4229  funbrfv2b  5250  dffn5im  5251  eqfnfv2  5298  fndmin  5306  fniniseg  5319  rexsupp  5323  fmptco  5362  dff13  5439  riotabidva  5515  mpt2eq123dva  5597  mpt2eq3dva  5600  mpt2xopovel  5890  qliftfun  6254  erovlem  6264  xpcomco  6370  ltexpi  6589  dfplpq2  6606  axprecex  7108  zrevaddcl  8482  qrevaddcl  8810  icoshft  9088  fznn  9182  shftdm  9848  2shfti  9857  sumeq2d  10334  sumeq2  10335  gcdaddm  10519