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  2446  2ax6elem  2469  mopick2  2631  ssrexf  4016  ssrexvOLD  4023  ssdif  4110  ssrin  4208  reupick  4295  disjss1  5083  copsexgw  5453  copsexg  5454  propeqop  5470  po3nr  5564  frss  5605  coss2  5823  ordsssuc2  6428  fununi  6594  dffv2  6959  oprabidw  7421  poseq  8140  extmptsuppeq  8170  onfununi  8313  oaass  8528  ssnnfi  9139  fiint  9284  fiintOLD  9285  fiss  9382  wemapsolem  9510  tcss  9704  ac6s  10444  reclem2pr  11008  qbtwnxr  13167  ico0  13359  icoshft  13441  2ffzeq  13617  clsslem  14957  r19.2uz  15325  isprm7  16685  prmdvdsncoprmbd  16704  infpn2  16891  prmgaplem4  17032  fthres2  17903  ablfacrplem  20004  rnglidlmmgm  21162  psdmul  22060  monmat2matmon  22718  neiss  23003  uptx  23519  txcn  23520  nrmr0reg  23643  cnpflfi  23893  cnextcn  23961  caussi  25204  ovolsslem  25392  tgtrisegint  28433  inagswap  28775  shorth  31231  ac6mapd  32556  mptssALT  32606  uzssico  32714  zarclsint  33869  ordtconnlem1  33921  omsmon  34296  omssubadd  34298  subgrtrl  35127  subgrcycl  35129  acycgrsubgr  35152  mclsax  35563  trisegint  36023  segcon2  36100  opnrebl2  36316  bj-19.42t  36768  poimirlem30  37651  itg2addnclem  37672  itg2addnclem2  37673  fdc1  37747  totbndss  37778  ablo4pnp  37881  keridl  38033  dib2dim  41244  dih2dimbALTN  41246  dvh1dim  41443  mapdpglem2  41674  pell14qrss1234  42851  pell1qrss14  42863  rmxycomplete  42913  lnr2i  43112  fzunt  43451  fzuntd  43452  fzunt1d  43453  fzuntgd  43454  rp-fakeanorass  43509  rfcnnnub  45037  or2expropbi  47039  2ffzoeq  47332  ich2exprop  47476  nnsum4primes4  47794  nnsum4primesprm  47796  nnsum4primesgbe  47798  nnsum4primesle9  47800  opnneir  48899