Theorem anim12d 328

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 289	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜏)))

Syntax hints:   → wi 4   ∧ wa 102

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  anim1d  329  anim2d  330  prth  336  im2anan9  562  anim12dan  564  3anim123d  1250  hband  1418  hbbid  1507  spsbim  1764  moim  2005  moimv  2007  2euswapdc  2032  rspcimedv  2703  soss  4069  trin2  4736  xp11m  4779  funss  4940  fun  5083  dff13  5428  f1eqcocnv  5451  isores3  5475  isosolem  5483  f1o2ndf1  5869  tposfn2  5904  tposf1o2  5908  nnaordex  6123  supmoti  6406  isotilem  6419  recexprlemss1l  6825  recexprlemss1u  6826  caucvgsrlemoffres  6976  nnindnn  7059  lemul12b  7939  lt2msq  7964  lbreu  8023  cju  8038  nnind  8055  uz11  8641  xrre2  8888  ico0  9270  ioc0  9271  expcan  9644  gcdaddm  10375  bezoutlemaz  10392  bezoutlembz  10393  isprm3  10500