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

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  602  anim12dan  604  3anim123d  1356  hband  1538  hbbid  1624  spsbim  1892  moim  2147  moimv  2149  2euswapdc  2174  rspcimedv  2925  soss  4440  trin2  5159  xp11m  5206  funss  5376  fun  5541  dff13  5947  f1eqcocnv  5970  isores3  5994  isosolem  6003  f1o2ndf1  6437  tposfn2  6510  tposf1o2  6514  nndifsnid  6753  nnaordex  6774  supmoti  7297  isotilem  7310  recexprlemss1l  7966  recexprlemss1u  7967  caucvgsrlemoffres  8131  suplocsrlem  8139  nnindnn  8224  eqord1  8775  lemul12b  9155  lt2msq  9180  lbreu  9239  cju  9255  nnind  9273  uz11  9898  xrre2  10176  ico0  10648  ioc0  10649  expcan  11106  swrdccatin2  11449  gcdaddm  12708  bezoutlemaz  12727  bezoutlembz  12728  isprm3  12843  prmdiveq  12961  mulgpropdg  13920  imasabl  14092  subrgdvds  14484  epttop  15084  cnptopresti  15232  cnptoprest  15233  txcnp  15265  addcncntoplem  15555  mulcncflem  15601  umgrvad2edg  16335  wlk1walkdom  16483  bj-stand  16659  exmidsbthrlem  16941