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  2478  2ax6elem  2501  mopick2  2664  ssrexf  4001  rabss2  4028  ssdif  4094  ssrin  4190  reupick  4278  disjss1  5080  copsexgwOLD  5471  copsexg  5472  propeqop  5488  po3nr  5582  frss  5623  coss2  5840  ordsssuc2  6455  fununi  6612  dffv2  6977  oprabidw  7447  poseq  8159  extmptsuppeq  8189  onfununi  8333  oaass  8551  ssnnfi  9167  fiint  9299  fiss  9397  wemapsolem  9525  elirrvOLD  9573  tcss  9724  ac6s  10489  reclem2pr  11060  qbtwnxr  13254  ico0  13446  icoshft  13528  2ffzeq  13706  clsslem  15059  r19.2uz  15441  isprm7  16803  prmdvdsncoprmbd  16822  infpn2  17009  prmgaplem4  17150  fthres2  18027  chndss  18708  ablfacrplem  20198  rnglidlmmgm  21446  psdmul  22398  monmat2matmon  23053  neiss  23338  uptx  23855  txcn  23856  nrmr0reg  23979  cnpflfi  24229  cnextcn  24297  caussi  25529  ovolsslem  25716  tgtrisegint  28842  inagswap  29240  subgrtrl  30174  subgrcycl  30265  shorth  31777  ac6mapd  33098  mptssALT  33149  uzssico  33257  zarclsint  34384  ordtconnlem1  34436  omsmon  34811  omssubadd  34813  r1filimi  35613  acycgrsubgr  35739  mclsax  36150  trisegint  36610  segcon2  36687  opnrebl2  36942  bj-19.42t  37500  bj-axreprepsep  37822  wl-dfcleq  38270  poimirlem30  38401  itg2addnclem  38422  itg2addnclem2  38423  fdc1  38498  totbndss  38529  ablo4pnp  38632  keridl  38784  dib2dim  42118  dih2dimbALTN  42120  dvh1dim  42317  mapdpglem2  42548  pell14qrss1234  43699  pell1qrss14  43711  rmxycomplete  43760  lnr2i  43959  fzunt  44297  fzuntd  44298  fzunt1d  44299  fzuntgd  44300  rp-fakeanorass  44355  rfcnnnub  45872  or2expropbi  47924  2ffzoeq  48218  ich2exprop  48373  nnsum4primes4  48707  nnsum4primesprm  48709  nnsum4primesgbe  48711  nnsum4primesle9  48713  opnneir  49835