Theorem anim12dan 600

Description: Conjoin antecedents and consequents in a deduction. (Contributed by Mario Carneiro, 12-May-2014.)

Hypotheses

Ref	Expression
anim12dan.1	|- ( ( ph /\ ps ) -> ch )
anim12dan.2	|- ( ( ph /\ th ) -> ta )

Assertion

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

Proof of Theorem anim12dan

Step	Hyp	Ref	Expression
1		anim12dan.1	. . . 4 |- ( ( ph /\ ps ) -> ch )
2	1	ex 115	. . 3 |- ( ph -> ( ps -> ch ) )
3		anim12dan.2	. . . 4 |- ( ( ph /\ th ) -> ta )
4	3	ex 115	. . 3 |- ( ph -> ( th -> ta ) )
5	2, 4	anim12d 335	. 2 |- ( ph -> ( ( ps /\ th ) -> ( ch /\ ta ) ) )
6	5	imp 124	1 |- ( ( ph /\ ( ps /\ th ) ) -> ( ch /\ ta ) )

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  xpexr2m  5123  isocnv  5879  f1oiso  5894  f1oiso2  5895  f1o2ndf1  6313  xpf1o  6940  pc11  12596  imasaddfnlemg  13088  imasaddflemg  13090  mhmpropd  13240  ghmsub  13529  invrpropdg  13853  znidom  14361  tgclb  14479  innei  14577  txcn  14689  plymullem1  15162  lgsdir2  15452