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  598  anim12dan  600  3anim123d  1319  hband  1489  hbbid  1575  spsbim  1843  moim  2090  moimv  2092  2euswapdc  2117  rspcimedv  2845  soss  4316  trin2  5022  xp11m  5069  funss  5237  fun  5390  dff13  5771  f1eqcocnv  5794  isores3  5818  isosolem  5827  f1o2ndf1  6231  tposfn2  6269  tposf1o2  6273  nndifsnid  6510  nnaordex  6531  supmoti  6994  isotilem  7007  recexprlemss1l  7636  recexprlemss1u  7637  caucvgsrlemoffres  7801  suplocsrlem  7809  nnindnn  7894  eqord1  8442  lemul12b  8820  lt2msq  8845  lbreu  8904  cju  8920  nnind  8937  uz11  9552  xrre2  9823  ico0  10264  ioc0  10265  expcan  10698  gcdaddm  11987  bezoutlemaz  12006  bezoutlembz  12007  isprm3  12120  prmdiveq  12238  mulgpropdg  13030  subrgdvds  13361  epttop  13629  cnptopresti  13777  cnptoprest  13778  txcnp  13810  addcncntoplem  14090  mulcncflem  14129  bj-stand  14539  exmidsbthrlem  14809