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	⊢ (𝜑 → (𝜓 → 𝜒))
anim12d.2	⊢ (𝜑 → (𝜃 → 𝜏))

Assertion

Ref	Expression
anim12d	⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜏)))

Proof of Theorem anim12d

Step	Hyp	Ref	Expression
1		anim12d.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		anim12d.2	. 2 ⊢ (𝜑 → (𝜃 → 𝜏))
3		idd 21	. 2 ⊢ (𝜑 → ((𝜒 ∧ 𝜏) → (𝜒 ∧ 𝜏)))
4	1, 2, 3	syl2and 293	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜏)))

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  341  im2anan9  587  anim12dan  589  3anim123d  1297  hband  1465  hbbid  1554  spsbim  1815  moim  2061  moimv  2063  2euswapdc  2088  rspcimedv  2786  soss  4231  trin2  4925  xp11m  4972  funss  5137  fun  5290  dff13  5662  f1eqcocnv  5685  isores3  5709  isosolem  5718  f1o2ndf1  6118  tposfn2  6156  tposf1o2  6160  nndifsnid  6396  nnaordex  6416  supmoti  6873  isotilem  6886  recexprlemss1l  7436  recexprlemss1u  7437  caucvgsrlemoffres  7601  suplocsrlem  7609  nnindnn  7694  eqord1  8238  lemul12b  8612  lt2msq  8637  lbreu  8696  cju  8712  nnind  8729  uz11  9341  xrre2  9597  ico0  10032  ioc0  10033  expcan  10456  gcdaddm  11661  bezoutlemaz  11680  bezoutlembz  11681  isprm3  11788  epttop  12248  cnptopresti  12396  cnptoprest  12397  txcnp  12429  addcncntoplem  12709  mulcncflem  12748  bj-stand  12945  exmidsbthrlem  13206