Theorem anim12d 333

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 293	1 |- ( ph -> ( ( ps /\ th ) -> ( ch /\ ta ) ) )

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  anim1d  334  anim2d  335  anim12  342  im2anan9  588  anim12dan  590  3anim123d  1298  hband  1466  hbbid  1555  spsbim  1816  moim  2064  moimv  2066  2euswapdc  2091  rspcimedv  2795  soss  4244  trin2  4938  xp11m  4985  funss  5150  fun  5303  dff13  5677  f1eqcocnv  5700  isores3  5724  isosolem  5733  f1o2ndf1  6133  tposfn2  6171  tposf1o2  6175  nndifsnid  6411  nnaordex  6431  supmoti  6888  isotilem  6901  recexprlemss1l  7467  recexprlemss1u  7468  caucvgsrlemoffres  7632  suplocsrlem  7640  nnindnn  7725  eqord1  8269  lemul12b  8643  lt2msq  8668  lbreu  8727  cju  8743  nnind  8760  uz11  9372  xrre2  9634  ico0  10070  ioc0  10071  expcan  10494  gcdaddm  11708  bezoutlemaz  11727  bezoutlembz  11728  isprm3  11835  epttop  12298  cnptopresti  12446  cnptoprest  12447  txcnp  12479  addcncntoplem  12759  mulcncflem  12798  bj-stand  13127  exmidsbthrlem  13392