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  1331  hband  1511  hbbid  1597  spsbim  1865  moim  2117  moimv  2119  2euswapdc  2144  rspcimedv  2878  soss  4360  trin2  5073  xp11m  5120  funss  5289  fun  5447  dff13  5836  f1eqcocnv  5859  isores3  5883  isosolem  5892  f1o2ndf1  6313  tposfn2  6351  tposf1o2  6355  nndifsnid  6592  nnaordex  6613  supmoti  7094  isotilem  7107  recexprlemss1l  7747  recexprlemss1u  7748  caucvgsrlemoffres  7912  suplocsrlem  7920  nnindnn  8005  eqord1  8555  lemul12b  8933  lt2msq  8958  lbreu  9017  cju  9033  nnind  9051  uz11  9670  xrre2  9942  ico0  10402  ioc0  10403  expcan  10859  gcdaddm  12247  bezoutlemaz  12266  bezoutlembz  12267  isprm3  12382  prmdiveq  12500  mulgpropdg  13442  imasabl  13614  subrgdvds  13939  epttop  14504  cnptopresti  14652  cnptoprest  14653  txcnp  14685  addcncntoplem  14975  mulcncflem  15021  bj-stand  15617  exmidsbthrlem  15894