Theorem anim1d 611

Description: Add a conjunct to right of antecedent and consequent in a deduction. (Contributed by NM, 3-Apr-1994.)

Hypothesis

Ref	Expression
anim1d.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
anim1d	⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜃)))

Proof of Theorem anim1d

Step	Hyp	Ref	Expression
1		anim1d.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		idd 24	. 2 ⊢ (𝜑 → (𝜃 → 𝜃))
3	1, 2	anim12d 609	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ∧ wa 395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  pm3.45  622  exdistrf  2449  2ax6elem  2472  mopick2  2634  ssrexf  3997  ssrexvOLD  4004  rabss2  4026  ssdif  4093  ssrin  4191  reupick  4278  disjss1  5066  copsexgw  5433  copsexg  5434  propeqop  5450  po3nr  5542  frss  5583  coss2  5800  ordsssuc2  6404  fununi  6561  dffv2  6923  oprabidw  7383  poseq  8094  extmptsuppeq  8124  onfununi  8267  oaass  8482  ssnnfi  9086  fiint  9218  fiss  9315  wemapsolem  9443  elirrv  9490  tcss  9639  ac6s  10382  reclem2pr  10946  qbtwnxr  13101  ico0  13293  icoshft  13375  2ffzeq  13551  clsslem  14893  r19.2uz  15261  isprm7  16621  prmdvdsncoprmbd  16640  infpn2  16827  prmgaplem4  16968  fthres2  17843  chndss  18524  ablfacrplem  19981  rnglidlmmgm  21184  psdmul  22082  monmat2matmon  22740  neiss  23025  uptx  23541  txcn  23542  nrmr0reg  23665  cnpflfi  23915  cnextcn  23983  caussi  25225  ovolsslem  25413  tgtrisegint  28478  inagswap  28820  shorth  31277  ac6mapd  32608  mptssALT  32659  uzssico  32771  zarclsint  33906  ordtconnlem1  33958  omsmon  34332  omssubadd  34334  r1filimi  35135  subgrtrl  35198  subgrcycl  35200  acycgrsubgr  35223  mclsax  35634  trisegint  36093  segcon2  36170  opnrebl2  36386  bj-19.42t  36838  poimirlem30  37710  itg2addnclem  37731  itg2addnclem2  37732  fdc1  37806  totbndss  37837  ablo4pnp  37940  keridl  38092  dib2dim  41362  dih2dimbALTN  41364  dvh1dim  41561  mapdpglem2  41792  pell14qrss1234  42973  pell1qrss14  42985  rmxycomplete  43034  lnr2i  43233  fzunt  43572  fzuntd  43573  fzunt1d  43574  fzuntgd  43575  rp-fakeanorass  43630  rfcnnnub  45157  or2expropbi  47158  2ffzoeq  47451  ich2exprop  47595  nnsum4primes4  47913  nnsum4primesprm  47915  nnsum4primesgbe  47917  nnsum4primesle9  47919  opnneir  49031