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  1332  hband  1513  hbbid  1599  spsbim  1867  moim  2119  moimv  2121  2euswapdc  2146  rspcimedv  2883  soss  4369  trin2  5083  xp11m  5130  funss  5299  fun  5459  dff13  5850  f1eqcocnv  5873  isores3  5897  isosolem  5906  f1o2ndf1  6327  tposfn2  6365  tposf1o2  6369  nndifsnid  6606  nnaordex  6627  supmoti  7110  isotilem  7123  recexprlemss1l  7768  recexprlemss1u  7769  caucvgsrlemoffres  7933  suplocsrlem  7941  nnindnn  8026  eqord1  8576  lemul12b  8954  lt2msq  8979  lbreu  9038  cju  9054  nnind  9072  uz11  9691  xrre2  9963  ico0  10426  ioc0  10427  expcan  10883  gcdaddm  12380  bezoutlemaz  12399  bezoutlembz  12400  isprm3  12515  prmdiveq  12633  mulgpropdg  13575  imasabl  13747  subrgdvds  14072  epttop  14637  cnptopresti  14785  cnptoprest  14786  txcnp  14818  addcncntoplem  15108  mulcncflem  15154  bj-stand  15823  exmidsbthrlem  16102