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  598  anim12dan  600  3anim123d  1330  hband  1503  hbbid  1589  spsbim  1857  moim  2109  moimv  2111  2euswapdc  2136  rspcimedv  2870  soss  4349  trin2  5061  xp11m  5108  funss  5277  fun  5430  dff13  5815  f1eqcocnv  5838  isores3  5862  isosolem  5871  f1o2ndf1  6286  tposfn2  6324  tposf1o2  6328  nndifsnid  6565  nnaordex  6586  supmoti  7059  isotilem  7072  recexprlemss1l  7702  recexprlemss1u  7703  caucvgsrlemoffres  7867  suplocsrlem  7875  nnindnn  7960  eqord1  8510  lemul12b  8888  lt2msq  8913  lbreu  8972  cju  8988  nnind  9006  uz11  9624  xrre2  9896  ico0  10351  ioc0  10352  expcan  10808  gcdaddm  12151  bezoutlemaz  12170  bezoutlembz  12171  isprm3  12286  prmdiveq  12404  mulgpropdg  13294  imasabl  13466  subrgdvds  13791  epttop  14326  cnptopresti  14474  cnptoprest  14475  txcnp  14507  addcncntoplem  14797  mulcncflem  14843  bj-stand  15394  exmidsbthrlem  15666