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  2910  soss  4409  trin2  5126  xp11m  5173  funss  5343  fun  5505  dff13  5904  f1eqcocnv  5927  isores3  5951  isosolem  5960  f1o2ndf1  6388  tposfn2  6427  tposf1o2  6431  nndifsnid  6670  nnaordex  6691  supmoti  7186  isotilem  7199  recexprlemss1l  7848  recexprlemss1u  7849  caucvgsrlemoffres  8013  suplocsrlem  8021  nnindnn  8106  eqord1  8656  lemul12b  9034  lt2msq  9059  lbreu  9118  cju  9134  nnind  9152  uz11  9772  xrre2  10049  ico0  10514  ioc0  10515  expcan  10971  swrdccatin2  11303  gcdaddm  12548  bezoutlemaz  12567  bezoutlembz  12568  isprm3  12683  prmdiveq  12801  mulgpropdg  13744  imasabl  13916  subrgdvds  14242  epttop  14807  cnptopresti  14955  cnptoprest  14956  txcnp  14988  addcncntoplem  15278  mulcncflem  15324  umgrvad2edg  16055  wlk1walkdom  16170  bj-stand  16294  exmidsbthrlem  16576