Theorem anim12d 335

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 295	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:  anim1d  336  anim2d  337  anim12  344  im2anan9  602  anim12dan  604  3anim123d  1356  hband  1538  hbbid  1624  spsbim  1892  moim  2147  moimv  2149  2euswapdc  2174  rspcimedv  2925  soss  4440  trin2  5159  xp11m  5206  funss  5376  fun  5541  dff13  5947  f1eqcocnv  5970  isores3  5994  isosolem  6003  f1o2ndf1  6437  tposfn2  6510  tposf1o2  6514  nndifsnid  6753  nnaordex  6774  supmoti  7297  isotilem  7310  recexprlemss1l  7966  recexprlemss1u  7967  caucvgsrlemoffres  8131  suplocsrlem  8139  nnindnn  8224  eqord1  8774  lemul12b  9152  lt2msq  9177  lbreu  9236  cju  9252  nnind  9270  uz11  9895  xrre2  10173  ico0  10645  ioc0  10646  expcan  11103  swrdccatin2  11446  gcdaddm  12705  bezoutlemaz  12724  bezoutlembz  12725  isprm3  12840  prmdiveq  12958  mulgpropdg  13917  imasabl  14089  subrgdvds  14481  epttop  15081  cnptopresti  15229  cnptoprest  15230  txcnp  15262  addcncntoplem  15552  mulcncflem  15598  umgrvad2edg  16332  wlk1walkdom  16480  bj-stand  16646  exmidsbthrlem  16928