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  1330  hband  1500  hbbid  1586  spsbim  1854  moim  2106  moimv  2108  2euswapdc  2133  rspcimedv  2866  soss  4345  trin2  5057  xp11m  5104  funss  5273  fun  5426  dff13  5811  f1eqcocnv  5834  isores3  5858  isosolem  5867  f1o2ndf1  6281  tposfn2  6319  tposf1o2  6323  nndifsnid  6560  nnaordex  6581  supmoti  7052  isotilem  7065  recexprlemss1l  7695  recexprlemss1u  7696  caucvgsrlemoffres  7860  suplocsrlem  7868  nnindnn  7953  eqord1  8502  lemul12b  8880  lt2msq  8905  lbreu  8964  cju  8980  nnind  8998  uz11  9615  xrre2  9887  ico0  10330  ioc0  10331  expcan  10787  gcdaddm  12121  bezoutlemaz  12140  bezoutlembz  12141  isprm3  12256  prmdiveq  12374  mulgpropdg  13234  imasabl  13406  subrgdvds  13731  epttop  14258  cnptopresti  14406  cnptoprest  14407  txcnp  14439  addcncntoplem  14719  mulcncflem  14761  bj-stand  15240  exmidsbthrlem  15512