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  2451  2ax6elem  2474  mopick2  2636  ssrexf  4025  ssrexvOLD  4032  ssdif  4119  ssrin  4217  reupick  4304  disjss1  5092  copsexgw  5465  copsexg  5466  propeqop  5482  po3nr  5576  frss  5618  coss2  5836  ordsssuc2  6445  fununi  6611  dffv2  6974  oprabidw  7436  poseq  8157  extmptsuppeq  8187  onfununi  8355  oaass  8573  ssnnfi  9183  fiint  9338  fiintOLD  9339  fiss  9436  wemapsolem  9564  tcss  9758  ac6s  10498  reclem2pr  11062  qbtwnxr  13216  ico0  13408  icoshft  13490  2ffzeq  13666  clsslem  15003  r19.2uz  15370  isprm7  16727  prmdvdsncoprmbd  16746  infpn2  16933  prmgaplem4  17074  fthres2  17947  ablfacrplem  20048  rnglidlmmgm  21206  psdmul  22104  monmat2matmon  22762  neiss  23047  uptx  23563  txcn  23564  nrmr0reg  23687  cnpflfi  23937  cnextcn  24005  caussi  25249  ovolsslem  25437  tgtrisegint  28478  inagswap  28820  shorth  31276  ac6mapd  32603  mptssALT  32653  uzssico  32761  zarclsint  33903  ordtconnlem1  33955  omsmon  34330  omssubadd  34332  subgrtrl  35155  subgrcycl  35157  acycgrsubgr  35180  mclsax  35591  trisegint  36046  segcon2  36123  opnrebl2  36339  bj-19.42t  36791  poimirlem30  37674  itg2addnclem  37695  itg2addnclem2  37696  fdc1  37770  totbndss  37801  ablo4pnp  37904  keridl  38056  dib2dim  41262  dih2dimbALTN  41264  dvh1dim  41461  mapdpglem2  41692  pell14qrss1234  42879  pell1qrss14  42891  rmxycomplete  42941  lnr2i  43140  fzunt  43479  fzuntd  43480  fzunt1d  43481  fzuntgd  43482  rp-fakeanorass  43537  rfcnnnub  45060  or2expropbi  47063  2ffzoeq  47356  ich2exprop  47485  nnsum4primes4  47803  nnsum4primesprm  47805  nnsum4primesgbe  47807  nnsum4primesle9  47809  opnneir  48881