Theorem anim1d 623

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 25	. 2 ⊢ (𝜑 → (𝜃 → 𝜃))
3	1, 2	anim12d 621	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜃)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  pm3.45  634  exdistrf  2477  2ax6elem  2500  mopick2  2663  ssrexf  3998  rabss2  4025  ssdif  4091  ssrin  4187  reupick  4275  disjss1  5076  copsexgwOLD  5461  copsexg  5462  propeqop  5479  po3nr  5574  frss  5615  coss2  5834  ordsssuc2  6449  fununi  6607  dffv2  6972  oprabidw  7443  poseq  8159  extmptsuppeq  8189  onfununi  8333  oaass  8553  ssnnfi  9169  fiint  9302  fiss  9400  wemapsolem  9528  elirrvOLD  9576  tcss  9727  r1filimi  9884  ac6s  10543  reclem2pr  11114  qbtwnxr  13311  ico0  13503  icoshft  13585  2ffzeq  13763  clsslem  15117  r19.2uz  15499  isprm7  16864  prmdvdsncoprmbd  16883  infpn2  17071  prmgaplem4  17212  fthres2  18089  chndss  18770  ablfacrplem  20261  rnglidlmmgm  21513  psdmul  22467  monmat2matmon  23122  neiss  23407  uptx  23924  txcn  23925  nrmr0reg  24048  cnpflfi  24298  cnextcn  24366  caussi  25598  ovolsslem  25785  fltoprmlem1  27975  tgtrisegint  28944  inagswap  29342  subgrtrl  30276  subgrcycl  30367  shorth  31879  ac6mapd  33199  mptssALT  33250  uzssico  33358  zarclsint  34486  ordtconnlem1  34538  omsmon  34913  omssubadd  34915  acycgrsubgr  35892  mclsax  36303  trisegint  36763  segcon2  36840  opnrebl2  37079  bj-19.42t  37637  bj-axreprepsep  37959  wl-dfcleq  38405  poimirlem30  38536  itg2addnclem  38557  itg2addnclem2  38558  fdc1  38648  totbndss  38679  ablo4pnp  38782  keridl  38934  dib2dim  42268  dih2dimbALTN  42270  dvh1dim  42467  mapdpglem2  42698  pell14qrss1234  43816  pell1qrss14  43828  rmxycomplete  43877  lnr2i  44076  fzunt  44414  fzuntd  44415  fzunt1d  44416  fzuntgd  44417  rp-fakeanorass  44472  rfcnnnub  45996  or2expropbi  48048  2ffzoeq  48342  ich2exprop  48497  nnsum4primes4  48831  nnsum4primesprm  48833  nnsum4primesgbe  48835  nnsum4primesle9  48837  opnneir  49959