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  600  anim12dan  602  3anim123d  1353  hband  1535  hbbid  1621  spsbim  1889  moim  2142  moimv  2144  2euswapdc  2169  rspcimedv  2909  soss  4405  trin2  5120  xp11m  5167  funss  5337  fun  5499  dff13  5898  f1eqcocnv  5921  isores3  5945  isosolem  5954  f1o2ndf1  6380  tposfn2  6418  tposf1o2  6422  nndifsnid  6661  nnaordex  6682  supmoti  7168  isotilem  7181  recexprlemss1l  7830  recexprlemss1u  7831  caucvgsrlemoffres  7995  suplocsrlem  8003  nnindnn  8088  eqord1  8638  lemul12b  9016  lt2msq  9041  lbreu  9100  cju  9116  nnind  9134  uz11  9753  xrre2  10025  ico0  10489  ioc0  10490  expcan  10946  swrdccatin2  11269  gcdaddm  12513  bezoutlemaz  12532  bezoutlembz  12533  isprm3  12648  prmdiveq  12766  mulgpropdg  13709  imasabl  13881  subrgdvds  14207  epttop  14772  cnptopresti  14920  cnptoprest  14921  txcnp  14953  addcncntoplem  15243  mulcncflem  15289  umgrvad2edg  16017  wlk1walkdom  16080  bj-stand  16136  exmidsbthrlem  16420