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  7448  poseq  8160  extmptsuppeq  8190  onfununi  8334  oaass  8552  ssnnfi  9168  fiint  9300  fiss  9398  wemapsolem  9526  elirrvOLD  9574  tcss  9725  ac6s  10490  reclem2pr  11061  qbtwnxr  13256  ico0  13448  icoshft  13530  2ffzeq  13708  clsslem  15061  r19.2uz  15443  isprm7  16805  prmdvdsncoprmbd  16824  infpn2  17011  prmgaplem4  17152  fthres2  18029  chndss  18710  ablfacrplem  20200  rnglidlmmgm  21448  psdmul  22400  monmat2matmon  23055  neiss  23340  uptx  23857  txcn  23858  nrmr0reg  23981  cnpflfi  24231  cnextcn  24299  caussi  25531  ovolsslem  25718  tgtrisegint  28849  inagswap  29247  subgrtrl  30181  subgrcycl  30272  shorth  31784  ac6mapd  33104  mptssALT  33155  uzssico  33263  zarclsint  34390  ordtconnlem1  34442  omsmon  34817  omssubadd  34819  r1filimi  35619  acycgrsubgr  35745  mclsax  36156  trisegint  36616  segcon2  36693  opnrebl2  36948  bj-19.42t  37506  bj-axreprepsep  37828  wl-dfcleq  38276  poimirlem30  38407  itg2addnclem  38428  itg2addnclem2  38429  fdc1  38504  totbndss  38535  ablo4pnp  38638  keridl  38790  dib2dim  42124  dih2dimbALTN  42126  dvh1dim  42323  mapdpglem2  42554  pell14qrss1234  43705  pell1qrss14  43717  rmxycomplete  43766  lnr2i  43965  fzunt  44303  fzuntd  44304  fzunt1d  44305  fzuntgd  44306  rp-fakeanorass  44361  rfcnnnub  45878  or2expropbi  47930  2ffzoeq  48224  ich2exprop  48379  nnsum4primes4  48713  nnsum4primesprm  48715  nnsum4primesgbe  48717  nnsum4primesle9  48719  opnneir  49841