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  2452  2ax6elem  2475  mopick2  2637  ssrexf  4050  ssrexvOLD  4057  ssdif  4144  ssrin  4242  reupick  4329  disjss1  5116  copsexgw  5495  copsexg  5496  propeqop  5512  po3nr  5607  frss  5649  coss2  5867  ordsssuc2  6475  fununi  6641  dffv2  7004  oprabidw  7462  poseq  8183  extmptsuppeq  8213  onfununi  8381  oaass  8599  ssnnfi  9209  fiint  9366  fiintOLD  9367  fiss  9464  wemapsolem  9590  tcss  9784  ac6s  10524  reclem2pr  11088  qbtwnxr  13242  ico0  13433  icoshft  13513  2ffzeq  13689  clsslem  15023  r19.2uz  15390  isprm7  16745  prmdvdsncoprmbd  16764  infpn2  16951  prmgaplem4  17092  fthres2  17979  ablfacrplem  20085  rnglidlmmgm  21255  psdmul  22170  monmat2matmon  22830  neiss  23117  uptx  23633  txcn  23634  nrmr0reg  23757  cnpflfi  24007  cnextcn  24075  caussi  25331  ovolsslem  25519  tgtrisegint  28507  inagswap  28849  shorth  31314  ac6mapd  32635  mptssALT  32685  uzssico  32786  zarclsint  33871  ordtconnlem1  33923  omsmon  34300  omssubadd  34302  subgrtrl  35138  subgrcycl  35140  acycgrsubgr  35163  mclsax  35574  trisegint  36029  segcon2  36106  opnrebl2  36322  bj-19.42t  36774  poimirlem30  37657  itg2addnclem  37678  itg2addnclem2  37679  fdc1  37753  totbndss  37784  ablo4pnp  37887  keridl  38039  dib2dim  41245  dih2dimbALTN  41247  dvh1dim  41444  mapdpglem2  41675  pell14qrss1234  42867  pell1qrss14  42879  rmxycomplete  42929  lnr2i  43128  fzunt  43468  fzuntd  43469  fzunt1d  43470  fzuntgd  43471  rp-fakeanorass  43526  rfcnnnub  45041  or2expropbi  47046  2ffzoeq  47339  ich2exprop  47458  nnsum4primes4  47776  nnsum4primesprm  47778  nnsum4primesgbe  47780  nnsum4primesle9  47782  opnneir  48804