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  606  anim12dan  608  3anim123d  1360  hband  1542  hbbid  1628  spsbim  1896  moim  2151  moimv  2153  2euswapdc  2178  rspcimedv  2931  soss  4457  trin2  5177  xp11m  5224  funss  5394  fun  5559  dff13  5968  f1eqcocnv  5991  isores3  6015  isosolem  6024  f1o2ndf1  6458  tposfn2  6531  tposf1o2  6535  nndifsnid  6774  nnaordex  6795  supmoti  7327  isotilem  7340  recexprlemss1l  7996  recexprlemss1u  7997  caucvgsrlemoffres  8161  suplocsrlem  8169  nnindnn  8254  eqord1  8805  lemul12b  9185  lt2msq  9210  lbreu  9269  cju  9285  nnind  9303  uz11  9928  xrre2  10206  ico0  10679  ioc0  10680  expcan  11137  swrdccatin2  11484  gcdaddm  12744  bezoutlemaz  12763  bezoutlembz  12764  isprm3  12879  prmdiveq  12997  mulgpropdg  13950  imasabl  14123  subrgdvds  14526  epttop  15174  cnptopresti  15322  cnptoprest  15323  txcnp  15355  addcncntoplem  15645  mulcncflem  15691  umgrvad2edg  16435  wlk1walkdom  16583  bj-stand  16759  exmidsbthrlem  17041