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  606  anim12dan  608  3anim123d  1360  hband  1542  hbbid  1628  spsbim  1896  moim  2151  moimv  2153  2euswapdc  2178  rspcimedv  2931  soss  4454  trin2  5174  xp11m  5221  funss  5391  fun  5556  dff13  5964  f1eqcocnv  5987  isores3  6011  isosolem  6020  f1o2ndf1  6454  tposfn2  6527  tposf1o2  6531  nndifsnid  6770  nnaordex  6791  supmoti  7323  isotilem  7336  recexprlemss1l  7992  recexprlemss1u  7993  caucvgsrlemoffres  8157  suplocsrlem  8165  nnindnn  8250  eqord1  8801  lemul12b  9181  lt2msq  9206  lbreu  9265  cju  9281  nnind  9299  uz11  9924  xrre2  10202  ico0  10674  ioc0  10675  expcan  11132  swrdccatin2  11479  gcdaddm  12739  bezoutlemaz  12758  bezoutlembz  12759  isprm3  12874  prmdiveq  12992  mulgpropdg  13944  imasabl  14117  subrgdvds  14516  epttop  15114  cnptopresti  15262  cnptoprest  15263  txcnp  15295  addcncntoplem  15585  mulcncflem  15631  umgrvad2edg  16366  wlk1walkdom  16514  bj-stand  16690  exmidsbthrlem  16972