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  1500  hbbid  1586  spsbim  1854  moim  2102  moimv  2104  2euswapdc  2129  rspcimedv  2858  soss  4329  trin2  5035  xp11m  5082  funss  5250  fun  5403  dff13  5785  f1eqcocnv  5808  isores3  5832  isosolem  5841  f1o2ndf1  6247  tposfn2  6285  tposf1o2  6289  nndifsnid  6526  nnaordex  6547  supmoti  7010  isotilem  7023  recexprlemss1l  7652  recexprlemss1u  7653  caucvgsrlemoffres  7817  suplocsrlem  7825  nnindnn  7910  eqord1  8458  lemul12b  8836  lt2msq  8861  lbreu  8920  cju  8936  nnind  8953  uz11  9568  xrre2  9839  ico0  10280  ioc0  10281  expcan  10714  gcdaddm  12003  bezoutlemaz  12022  bezoutlembz  12023  isprm3  12136  prmdiveq  12254  mulgpropdg  13070  imasabl  13234  subrgdvds  13543  epttop  13974  cnptopresti  14122  cnptoprest  14123  txcnp  14155  addcncntoplem  14435  mulcncflem  14474  bj-stand  14884  exmidsbthrlem  15155