Theorem anim12d 333

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 293	1 |- ( ph -> ( ( ps /\ th ) -> ( ch /\ ta ) ) )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  anim1d  334  anim2d  335  anim12  342  im2anan9  588  anim12dan  590  3anim123d  1309  hband  1477  hbbid  1563  spsbim  1831  moim  2078  moimv  2080  2euswapdc  2105  rspcimedv  2832  soss  4292  trin2  4995  xp11m  5042  funss  5207  fun  5360  dff13  5736  f1eqcocnv  5759  isores3  5783  isosolem  5792  f1o2ndf1  6196  tposfn2  6234  tposf1o2  6238  nndifsnid  6475  nnaordex  6495  supmoti  6958  isotilem  6971  recexprlemss1l  7576  recexprlemss1u  7577  caucvgsrlemoffres  7741  suplocsrlem  7749  nnindnn  7834  eqord1  8381  lemul12b  8756  lt2msq  8781  lbreu  8840  cju  8856  nnind  8873  uz11  9488  xrre2  9757  ico0  10197  ioc0  10198  expcan  10629  gcdaddm  11917  bezoutlemaz  11936  bezoutlembz  11937  isprm3  12050  prmdiveq  12168  epttop  12730  cnptopresti  12878  cnptoprest  12879  txcnp  12911  addcncntoplem  13191  mulcncflem  13230  bj-stand  13629  exmidsbthrlem  13901