Theorem anim12d 328

Description: Conjoin antecedents and consequents in a deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 18-Dec-2013.)

Hypotheses

Ref	Expression
anim12d.1	|- ( ph -> ( ps -> ch ) )
anim12d.2	|- ( ph -> ( th -> ta ) )

Assertion

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

Proof of Theorem anim12d

Step	Hyp	Ref	Expression
1		anim12d.1	. 2 |- ( ph -> ( ps -> ch ) )
2		anim12d.2	. 2 |- ( ph -> ( th -> ta ) )
3		idd 21	. 2 |- ( ph -> ( ( ch /\ ta ) -> ( ch /\ ta ) ) )
4	1, 2, 3	syl2and 289	1 |- ( ph -> ( ( ps /\ th ) -> ( ch /\ ta ) ) )

Syntax hints:   -> wi 4   /\ wa 102

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:  anim1d  329  anim2d  330  prth  336  im2anan9  563  anim12dan  565  3anim123d  1251  hband  1419  hbbid  1508  spsbim  1766  moim  2007  moimv  2009  2euswapdc  2034  rspcimedv  2712  soss  4097  trin2  4766  xp11m  4809  funss  4970  fun  5114  dff13  5459  f1eqcocnv  5482  isores3  5506  isosolem  5514  f1o2ndf1  5900  tposfn2  5935  tposf1o2  5939  nndifsnid  6167  nnaordex  6187  supmoti  6500  isotilem  6513  recexprlemss1l  6939  recexprlemss1u  6940  caucvgsrlemoffres  7090  nnindnn  7173  lemul12b  8058  lt2msq  8083  lbreu  8142  cju  8157  nnind  8174  uz11  8774  xrre2  9016  ico0  9400  ioc0  9401  expcan  9793  gcdaddm  10582  bezoutlemaz  10599  bezoutlembz  10600  isprm3  10707