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  602  anim12dan  604  3anim123d  1355  hband  1537  hbbid  1623  spsbim  1891  moim  2144  moimv  2146  2euswapdc  2171  rspcimedv  2912  soss  4411  trin2  5128  xp11m  5175  funss  5345  fun  5508  dff13  5909  f1eqcocnv  5932  isores3  5956  isosolem  5965  f1o2ndf1  6393  tposfn2  6432  tposf1o2  6436  nndifsnid  6675  nnaordex  6696  supmoti  7192  isotilem  7205  recexprlemss1l  7855  recexprlemss1u  7856  caucvgsrlemoffres  8020  suplocsrlem  8028  nnindnn  8113  eqord1  8663  lemul12b  9041  lt2msq  9066  lbreu  9125  cju  9141  nnind  9159  uz11  9779  xrre2  10056  ico0  10522  ioc0  10523  expcan  10979  swrdccatin2  11311  gcdaddm  12557  bezoutlemaz  12576  bezoutlembz  12577  isprm3  12692  prmdiveq  12810  mulgpropdg  13753  imasabl  13925  subrgdvds  14252  epttop  14817  cnptopresti  14965  cnptoprest  14966  txcnp  14998  addcncntoplem  15288  mulcncflem  15334  umgrvad2edg  16065  wlk1walkdom  16213  bj-stand  16365  exmidsbthrlem  16647