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  1334  hband  1515  hbbid  1601  spsbim  1869  moim  2122  moimv  2124  2euswapdc  2149  rspcimedv  2889  soss  4382  trin2  5096  xp11m  5143  funss  5313  fun  5473  dff13  5865  f1eqcocnv  5888  isores3  5912  isosolem  5921  f1o2ndf1  6344  tposfn2  6382  tposf1o2  6386  nndifsnid  6623  nnaordex  6644  supmoti  7128  isotilem  7141  recexprlemss1l  7790  recexprlemss1u  7791  caucvgsrlemoffres  7955  suplocsrlem  7963  nnindnn  8048  eqord1  8598  lemul12b  8976  lt2msq  9001  lbreu  9060  cju  9076  nnind  9094  uz11  9713  xrre2  9985  ico0  10448  ioc0  10449  expcan  10905  swrdccatin2  11227  gcdaddm  12471  bezoutlemaz  12490  bezoutlembz  12491  isprm3  12606  prmdiveq  12724  mulgpropdg  13667  imasabl  13839  subrgdvds  14164  epttop  14729  cnptopresti  14877  cnptoprest  14878  txcnp  14910  addcncntoplem  15200  mulcncflem  15246  umgrvad2edg  15974  bj-stand  16022  exmidsbthrlem  16301