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  4461  trin2  5182  xp11m  5229  funss  5399  fun  5564  dff13  5977  f1eqcocnv  6000  isores3  6024  isosolem  6033  f1o2ndf1  6468  tposfn2  6541  tposf1o2  6545  nndifsnid  6784  nnaordex  6805  supmoti  7340  isotilem  7353  recexprlemss1l  8009  recexprlemss1u  8010  caucvgsrlemoffres  8174  suplocsrlem  8182  nnindnn  8267  eqord1  8819  lemul12b  9200  lt2msq  9225  lbreu  9284  cju  9300  nnind  9330  uz11  9962  xrre2  10241  ico0  10714  ioc0  10715  expcan  11177  swrdccatin2  11524  gcdaddm  12787  bezoutlemaz  12806  bezoutlembz  12807  isprm3  12922  prmdiveq  13044  mulgpropdg  14027  imasabl  14231  subrgdvds  14653  epttop  15328  cnptopresti  15476  cnptoprest  15477  txcnp  15509  addcncntoplem  15799  mulcncflem  15845  umgrvad2edg  16669  wlk1walkdom  16817  bj-stand  16993  exmidsbthrlem  17285