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  1892  moim  2145  moimv  2147  2euswapdc  2172  rspcimedv  2923  soss  4435  trin2  5154  xp11m  5201  funss  5371  fun  5536  dff13  5941  f1eqcocnv  5964  isores3  5988  isosolem  5997  f1o2ndf1  6424  tposfn2  6497  tposf1o2  6501  nndifsnid  6740  nnaordex  6761  supmoti  7284  isotilem  7297  recexprlemss1l  7950  recexprlemss1u  7951  caucvgsrlemoffres  8115  suplocsrlem  8123  nnindnn  8208  eqord1  8757  lemul12b  9135  lt2msq  9160  lbreu  9219  cju  9235  nnind  9253  uz11  9877  xrre2  10154  ico0  10621  ioc0  10622  expcan  11078  swrdccatin2  11421  gcdaddm  12680  bezoutlemaz  12699  bezoutlembz  12700  isprm3  12815  prmdiveq  12933  mulgpropdg  13881  imasabl  14053  subrgdvds  14380  epttop  14955  cnptopresti  15103  cnptoprest  15104  txcnp  15136  addcncntoplem  15426  mulcncflem  15472  umgrvad2edg  16206  wlk1walkdom  16354  bj-stand  16520  exmidsbthrlem  16802