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  4437  trin2  5156  xp11m  5203  funss  5373  fun  5538  dff13  5943  f1eqcocnv  5966  isores3  5990  isosolem  5999  f1o2ndf1  6426  tposfn2  6499  tposf1o2  6503  nndifsnid  6742  nnaordex  6763  supmoti  7286  isotilem  7299  recexprlemss1l  7955  recexprlemss1u  7956  caucvgsrlemoffres  8120  suplocsrlem  8128  nnindnn  8213  eqord1  8762  lemul12b  9140  lt2msq  9165  lbreu  9224  cju  9240  nnind  9258  uz11  9883  xrre2  10160  ico0  10628  ioc0  10629  expcan  11086  swrdccatin2  11429  gcdaddm  12688  bezoutlemaz  12707  bezoutlembz  12708  isprm3  12823  prmdiveq  12941  mulgpropdg  13902  imasabl  14074  subrgdvds  14403  epttop  15004  cnptopresti  15152  cnptoprest  15153  txcnp  15185  addcncntoplem  15475  mulcncflem  15521  umgrvad2edg  16255  wlk1walkdom  16403  bj-stand  16569  exmidsbthrlem  16851