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  600  anim12dan  602  3anim123d  1353  hband  1535  hbbid  1621  spsbim  1889  moim  2142  moimv  2144  2euswapdc  2169  rspcimedv  2909  soss  4406  trin2  5123  xp11m  5170  funss  5340  fun  5502  dff13  5901  f1eqcocnv  5924  isores3  5948  isosolem  5957  f1o2ndf1  6385  tposfn2  6423  tposf1o2  6427  nndifsnid  6666  nnaordex  6687  supmoti  7176  isotilem  7189  recexprlemss1l  7838  recexprlemss1u  7839  caucvgsrlemoffres  8003  suplocsrlem  8011  nnindnn  8096  eqord1  8646  lemul12b  9024  lt2msq  9049  lbreu  9108  cju  9124  nnind  9142  uz11  9762  xrre2  10034  ico0  10498  ioc0  10499  expcan  10955  swrdccatin2  11282  gcdaddm  12526  bezoutlemaz  12545  bezoutlembz  12546  isprm3  12661  prmdiveq  12779  mulgpropdg  13722  imasabl  13894  subrgdvds  14220  epttop  14785  cnptopresti  14933  cnptoprest  14934  txcnp  14966  addcncntoplem  15256  mulcncflem  15302  umgrvad2edg  16030  wlk1walkdom  16131  bj-stand  16221  exmidsbthrlem  16504