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 ) ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used 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  4461  trin2  5182  xp11m  5229  funss  5399  fun  5564  dff13  5977  f1eqcocnv  6000  isores3  6024  isosolem  6033  f1o2ndf1  6468  tposfn2  6542  tposf1o2  6546  nndifsnid  6785  nnaordex  6806  supmoti  7339  isotilem  7352  recexprlemss1l  8008  recexprlemss1u  8009  caucvgsrlemoffres  8173  suplocsrlem  8181  nnindnn  8266  eqord1  8818  lemul12b  9199  lt2msq  9224  lbreu  9283  cju  9299  nnind  9329  uz11  9960  xrre2  10239  ico0  10712  ioc0  10713  expcan  11175  swrdccatin2  11522  gcdaddm  12785  bezoutlemaz  12804  bezoutlembz  12805  isprm3  12920  prmdiveq  13042  mulgpropdg  14025  imasabl  14229  subrgdvds  14651  epttop  15333  cnptopresti  15481  cnptoprest  15482  txcnp  15514  addcncntoplem  15804  mulcncflem  15850  umgrvad2edg  16674  wlk1walkdom  16822  bj-stand  16998  exmidsbthrlem  17290