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  598  anim12dan  600  3anim123d  1332  hband  1513  hbbid  1599  spsbim  1867  moim  2119  moimv  2121  2euswapdc  2146  rspcimedv  2880  soss  4365  trin2  5079  xp11m  5126  funss  5295  fun  5454  dff13  5844  f1eqcocnv  5867  isores3  5891  isosolem  5900  f1o2ndf1  6321  tposfn2  6359  tposf1o2  6363  nndifsnid  6600  nnaordex  6621  supmoti  7102  isotilem  7115  recexprlemss1l  7755  recexprlemss1u  7756  caucvgsrlemoffres  7920  suplocsrlem  7928  nnindnn  8013  eqord1  8563  lemul12b  8941  lt2msq  8966  lbreu  9025  cju  9041  nnind  9059  uz11  9678  xrre2  9950  ico0  10411  ioc0  10412  expcan  10868  gcdaddm  12349  bezoutlemaz  12368  bezoutlembz  12369  isprm3  12484  prmdiveq  12602  mulgpropdg  13544  imasabl  13716  subrgdvds  14041  epttop  14606  cnptopresti  14754  cnptoprest  14755  txcnp  14787  addcncntoplem  15077  mulcncflem  15123  bj-stand  15758  exmidsbthrlem  16035