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  4350  trin2  5062  xp11m  5109  funss  5278  fun  5431  dff13  5816  f1eqcocnv  5839  isores3  5863  isosolem  5872  f1o2ndf1  6288  tposfn2  6326  tposf1o2  6330  nndifsnid  6567  nnaordex  6588  supmoti  7061  isotilem  7074  recexprlemss1l  7705  recexprlemss1u  7706  caucvgsrlemoffres  7870  suplocsrlem  7878  nnindnn  7963  eqord1  8513  lemul12b  8891  lt2msq  8916  lbreu  8975  cju  8991  nnind  9009  uz11  9627  xrre2  9899  ico0  10354  ioc0  10355  expcan  10811  gcdaddm  12162  bezoutlemaz  12181  bezoutlembz  12182  isprm3  12297  prmdiveq  12415  mulgpropdg  13320  imasabl  13492  subrgdvds  13817  epttop  14352  cnptopresti  14500  cnptoprest  14501  txcnp  14533  addcncntoplem  14823  mulcncflem  14869  bj-stand  15420  exmidsbthrlem  15695