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  341  im2anan9  587  anim12dan  589  3anim123d  1297  hband  1465  hbbid  1554  spsbim  1815  moim  2063  moimv  2065  2euswapdc  2090  rspcimedv  2791  soss  4236  trin2  4930  xp11m  4977  funss  5142  fun  5295  dff13  5669  f1eqcocnv  5692  isores3  5716  isosolem  5725  f1o2ndf1  6125  tposfn2  6163  tposf1o2  6167  nndifsnid  6403  nnaordex  6423  supmoti  6880  isotilem  6893  recexprlemss1l  7443  recexprlemss1u  7444  caucvgsrlemoffres  7608  suplocsrlem  7616  nnindnn  7701  eqord1  8245  lemul12b  8619  lt2msq  8644  lbreu  8703  cju  8719  nnind  8736  uz11  9348  xrre2  9604  ico0  10039  ioc0  10040  expcan  10463  gcdaddm  11672  bezoutlemaz  11691  bezoutlembz  11692  isprm3  11799  epttop  12259  cnptopresti  12407  cnptoprest  12408  txcnp  12440  addcncntoplem  12720  mulcncflem  12759  bj-stand  12956  exmidsbthrlem  13217