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  1891  moim  2144  moimv  2146  2euswapdc  2171  rspcimedv  2913  soss  4417  trin2  5135  xp11m  5182  funss  5352  fun  5516  dff13  5919  f1eqcocnv  5942  isores3  5966  isosolem  5975  f1o2ndf1  6402  tposfn2  6475  tposf1o2  6479  nndifsnid  6718  nnaordex  6739  supmoti  7235  isotilem  7248  recexprlemss1l  7898  recexprlemss1u  7899  caucvgsrlemoffres  8063  suplocsrlem  8071  nnindnn  8156  eqord1  8705  lemul12b  9083  lt2msq  9108  lbreu  9167  cju  9183  nnind  9201  uz11  9823  xrre2  10100  ico0  10567  ioc0  10568  expcan  11024  swrdccatin2  11359  gcdaddm  12618  bezoutlemaz  12637  bezoutlembz  12638  isprm3  12753  prmdiveq  12871  mulgpropdg  13814  imasabl  13986  subrgdvds  14313  epttop  14884  cnptopresti  15032  cnptoprest  15033  txcnp  15065  addcncntoplem  15355  mulcncflem  15401  umgrvad2edg  16135  wlk1walkdom  16283  bj-stand  16449  exmidsbthrlem  16733