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  600  anim12dan  602  3anim123d  1353  hband  1535  hbbid  1621  spsbim  1889  moim  2142  moimv  2144  2euswapdc  2169  rspcimedv  2909  soss  4404  trin2  5119  xp11m  5166  funss  5336  fun  5496  dff13  5891  f1eqcocnv  5914  isores3  5938  isosolem  5947  f1o2ndf1  6372  tposfn2  6410  tposf1o2  6414  nndifsnid  6651  nnaordex  6672  supmoti  7156  isotilem  7169  recexprlemss1l  7818  recexprlemss1u  7819  caucvgsrlemoffres  7983  suplocsrlem  7991  nnindnn  8076  eqord1  8626  lemul12b  9004  lt2msq  9029  lbreu  9088  cju  9104  nnind  9122  uz11  9741  xrre2  10013  ico0  10476  ioc0  10477  expcan  10933  swrdccatin2  11256  gcdaddm  12500  bezoutlemaz  12519  bezoutlembz  12520  isprm3  12635  prmdiveq  12753  mulgpropdg  13696  imasabl  13868  subrgdvds  14193  epttop  14758  cnptopresti  14906  cnptoprest  14907  txcnp  14939  addcncntoplem  15229  mulcncflem  15275  umgrvad2edg  16003  bj-stand  16070  exmidsbthrlem  16349