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  2637  ssrexf  4000  ssrexvOLD  4007  rabss2  4029  ssdif  4096  ssrin  4194  reupick  4281  disjss1  5071  copsexgw  5438  copsexg  5439  propeqop  5455  po3nr  5547  frss  5588  coss2  5805  ordsssuc2  6410  fununi  6567  dffv2  6929  oprabidw  7389  poseq  8100  extmptsuppeq  8130  onfununi  8273  oaass  8488  ssnnfi  9094  fiint  9227  fiss  9327  wemapsolem  9455  elirrv  9502  tcss  9651  ac6s  10394  reclem2pr  10959  qbtwnxr  13115  ico0  13307  icoshft  13389  2ffzeq  13565  clsslem  14907  r19.2uz  15275  isprm7  16635  prmdvdsncoprmbd  16654  infpn2  16841  prmgaplem4  16982  fthres2  17858  chndss  18539  ablfacrplem  19996  rnglidlmmgm  21200  psdmul  22109  monmat2matmon  22768  neiss  23053  uptx  23569  txcn  23570  nrmr0reg  23693  cnpflfi  23943  cnextcn  24011  caussi  25253  ovolsslem  25441  tgtrisegint  28571  inagswap  28913  shorth  31370  ac6mapd  32701  mptssALT  32753  uzssico  32864  zarclsint  34029  ordtconnlem1  34081  omsmon  34455  omssubadd  34457  r1filimi  35259  subgrtrl  35327  subgrcycl  35329  acycgrsubgr  35352  mclsax  35763  trisegint  36222  segcon2  36299  opnrebl2  36515  bj-19.42t  36974  poimirlem30  37847  itg2addnclem  37868  itg2addnclem2  37869  fdc1  37943  totbndss  37974  ablo4pnp  38077  keridl  38229  dib2dim  41499  dih2dimbALTN  41501  dvh1dim  41698  mapdpglem2  41929  pell14qrss1234  43094  pell1qrss14  43106  rmxycomplete  43155  lnr2i  43354  fzunt  43692  fzuntd  43693  fzunt1d  43694  fzuntgd  43695  rp-fakeanorass  43750  rfcnnnub  45277  or2expropbi  47276  2ffzoeq  47569  ich2exprop  47713  nnsum4primes4  48031  nnsum4primesprm  48033  nnsum4primesgbe  48035  nnsum4primesle9  48037  opnneir  49148