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 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜏)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  anim1d  336  anim2d  337  anim12  344  im2anan9  606  anim12dan  608  3anim123d  1360  hband  1542  hbbid  1628  spsbim  1896  moim  2151  moimv  2153  2euswapdc  2178  rspcimedv  2931  soss  4459  trin2  5179  xp11m  5226  funss  5396  fun  5561  dff13  5974  f1eqcocnv  5997  isores3  6021  isosolem  6030  f1o2ndf1  6464  tposfn2  6537  tposf1o2  6541  nndifsnid  6780  nnaordex  6801  supmoti  7333  isotilem  7346  recexprlemss1l  8002  recexprlemss1u  8003  caucvgsrlemoffres  8167  suplocsrlem  8175  nnindnn  8260  eqord1  8811  lemul12b  9192  lt2msq  9217  lbreu  9276  cju  9292  nnind  9321  uz11  9947  xrre2  10225  ico0  10698  ioc0  10699  expcan  11156  swrdccatin2  11503  gcdaddm  12763  bezoutlemaz  12782  bezoutlembz  12783  isprm3  12898  prmdiveq  13016  mulgpropdg  13969  imasabl  14142  subrgdvds  14545  epttop  15193  cnptopresti  15341  cnptoprest  15342  txcnp  15374  addcncntoplem  15664  mulcncflem  15710  umgrvad2edg  16464  wlk1walkdom  16612  bj-stand  16788  exmidsbthrlem  17079