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  2145  moimv  2147  2euswapdc  2172  rspcimedv  2922  soss  4434  trin2  5153  xp11m  5200  funss  5370  fun  5535  dff13  5940  f1eqcocnv  5963  isores3  5987  isosolem  5996  f1o2ndf1  6423  tposfn2  6496  tposf1o2  6500  nndifsnid  6739  nnaordex  6760  supmoti  7283  isotilem  7296  recexprlemss1l  7946  recexprlemss1u  7947  caucvgsrlemoffres  8111  suplocsrlem  8119  nnindnn  8204  eqord1  8753  lemul12b  9131  lt2msq  9156  lbreu  9215  cju  9231  nnind  9249  uz11  9873  xrre2  10150  ico0  10617  ioc0  10618  expcan  11074  swrdccatin2  11414  gcdaddm  12673  bezoutlemaz  12692  bezoutlembz  12693  isprm3  12808  prmdiveq  12926  mulgpropdg  13870  imasabl  14042  subrgdvds  14369  epttop  14942  cnptopresti  15090  cnptoprest  15091  txcnp  15123  addcncntoplem  15413  mulcncflem  15459  umgrvad2edg  16193  wlk1walkdom  16341  bj-stand  16507  exmidsbthrlem  16789