Theorem anim12d 329

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

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  anim1d  330  anim2d  331  prth  337  im2anan9  566  anim12dan  568  3anim123d  1256  hband  1424  hbbid  1513  spsbim  1772  moim  2013  moimv  2015  2euswapdc  2040  rspcimedv  2725  soss  4150  trin2  4836  xp11m  4882  funss  5047  fun  5196  dff13  5561  f1eqcocnv  5584  isores3  5608  isosolem  5617  f1o2ndf1  6007  tposfn2  6045  tposf1o2  6049  nndifsnid  6280  nnaordex  6300  supmoti  6742  isotilem  6755  recexprlemss1l  7255  recexprlemss1u  7256  caucvgsrlemoffres  7406  nnindnn  7489  eqord1  8022  lemul12b  8383  lt2msq  8408  lbreu  8467  cju  8482  nnind  8499  uz11  9102  xrre2  9344  ico0  9734  ioc0  9735  expcan  10186  gcdaddm  11314  bezoutlemaz  11331  bezoutlembz  11332  isprm3  11439  epttop  11851  exmidsbthrlem  12184