Theorem anim1d 609

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 607	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  pm3.45  620  exdistrf  2441  2ax6elem  2464  mopick2  2626  ssrexf  4045  ssrexvOLD  4052  ssdif  4136  ssrin  4232  reupick  4318  disjss1  5116  copsexgw  5486  copsexg  5487  propeqop  5503  po3nr  5599  frss  5639  coss2  5853  ordsssuc2  6456  fununi  6623  dffv2  6986  oprabidw  7444  poseq  8161  extmptsuppeq  8191  onfununi  8360  oaass  8580  ssnnfi  9196  ssnnfiOLD  9197  fiint  9358  fiintOLD  9359  fiss  9457  wemapsolem  9583  tcss  9777  ac6s  10515  reclem2pr  11079  qbtwnxr  13224  ico0  13415  icoshft  13495  2ffzeq  13667  clsslem  14981  r19.2uz  15348  isprm7  16701  prmdvdsncoprmbd  16721  infpn2  16907  prmgaplem4  17048  fthres2  17946  ablfacrplem  20058  rnglidlmmgm  21227  psdmul  22153  monmat2matmon  22811  neiss  23098  uptx  23614  txcn  23615  nrmr0reg  23738  cnpflfi  23988  cnextcn  24056  caussi  25310  ovolsslem  25498  tgtrisegint  28420  inagswap  28762  shorth  31222  mptssALT  32589  uzssico  32686  zarclsint  33697  ordtconnlem1  33749  omsmon  34142  omssubadd  34144  subgrtrl  34971  subgrcycl  34973  acycgrsubgr  34996  mclsax  35407  trisegint  35862  segcon2  35939  opnrebl2  36043  bj-19.42t  36488  poimirlem30  37361  itg2addnclem  37382  itg2addnclem2  37383  fdc1  37457  totbndss  37488  ablo4pnp  37591  keridl  37743  dib2dim  40952  dih2dimbALTN  40954  dvh1dim  41151  mapdpglem2  41382  pell14qrss1234  42547  pell1qrss14  42559  rmxycomplete  42609  lnr2i  42811  fzunt  43156  fzuntd  43157  fzunt1d  43158  fzuntgd  43159  rp-fakeanorass  43214  rfcnnnub  44669  or2expropbi  46682  2ffzoeq  46973  ich2exprop  47076  nnsum4primes4  47394  nnsum4primesprm  47396  nnsum4primesgbe  47398  nnsum4primesle9  47400  opnneir  48273