Theorem imdistanda 729

Description: Distribution of implication with conjunction (deduction version with conjoined antecedent). (Contributed by Jeff Madsen, 19-Jun-2011.)

Hypothesis

Ref	Expression
imdistanda.1	|- ( ( ph /\ ps ) -> ( ch -> th ) )

Assertion

Ref	Expression
imdistanda	|- ( ph -> ( ( ps /\ ch ) -> ( ps /\ th ) ) )

Proof of Theorem imdistanda

Step	Hyp	Ref	Expression
1		imdistanda.1	. . 3 |- ( ( ph /\ ps ) -> ( ch -> th ) )
2	1	ex 450	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	imdistand 728	1 |- ( ph -> ( ( ps /\ ch ) -> ( ps /\ th ) ) )

Syntax hints:   -> wi 4   /\ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  cfub  9071  cflm  9072  fzind  11475  uzss  11708  cau3lem  14094  supcvg  14588  eulerthlem2  15487  pgpfac1lem3  18476  iscnp4  21067  cncls2  21077  cncls  21078  cnntr  21079  1stcelcls  21264  cnpflf  21805  fclsnei  21823  cnpfcf  21845  alexsublem  21848  iscau4  23077  caussi  23095  equivcfil  23097  ismbf3d  23421  i1fmullem  23461  abelth  24195  ocsh  28142  fpwrelmap  29508  locfinreflem  29907  nosupbnd1lem5  31858  matunitlindf  33407  isdrngo3  33758  keridl  33831  pmapjat1  35139