Theorem anim1d 620

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 618	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  pm3.45  631  exdistrf  2477  2ax6elem  2500  mopick2  2663  ssrexf  4003  rabss2  4030  ssdif  4097  ssrin  4193  reupick  4281  disjss1  5072  copsexgwOLD  5458  copsexg  5459  propeqop  5475  po3nr  5568  frss  5609  coss2  5826  ordsssuc2  6435  fununi  6592  dffv2  6958  oprabidw  7423  poseq  8133  extmptsuppeq  8163  onfununi  8307  oaass  8525  ssnnfi  9134  fiint  9267  fiss  9367  wemapsolem  9495  elirrvOLD  9543  tcss  9694  ac6s  10438  reclem2pr  11003  qbtwnxr  13200  ico0  13392  icoshft  13474  2ffzeq  13651  clsslem  14994  r19.2uz  15362  isprm7  16726  prmdvdsncoprmbd  16745  infpn2  16932  prmgaplem4  17073  fthres2  17950  chndss  18631  ablfacrplem  20090  rnglidlmmgm  21295  psdmul  22211  monmat2matmon  22864  neiss  23149  uptx  23665  txcn  23666  nrmr0reg  23789  cnpflfi  24039  cnextcn  24107  caussi  25339  ovolsslem  25526  tgtrisegint  28645  inagswap  28987  shorth  31444  ac6mapd  32775  mptssALT  32826  uzssico  32936  zarclsint  34130  ordtconnlem1  34182  omsmon  34556  omssubadd  34558  r1filimi  35363  subgrtrl  35447  subgrcycl  35449  acycgrsubgr  35472  mclsax  35883  trisegint  36342  segcon2  36419  opnrebl2  36645  bj-19.42t  37204  bj-axreprepsep  37524  wl-dfcleq  37972  poimirlem30  38113  itg2addnclem  38134  itg2addnclem2  38135  fdc1  38209  totbndss  38240  ablo4pnp  38343  keridl  38495  dib2dim  41831  dih2dimbALTN  41833  dvh1dim  42030  mapdpglem2  42261  pell14qrss1234  43397  pell1qrss14  43409  rmxycomplete  43458  lnr2i  43657  fzunt  43995  fzuntd  43996  fzunt1d  43997  fzuntgd  43998  rp-fakeanorass  44053  rfcnnnub  45580  or2expropbi  47592  2ffzoeq  47886  ich2exprop  48041  nnsum4primes4  48375  nnsum4primesprm  48377  nnsum4primesgbe  48379  nnsum4primesle9  48381  opnneir  49492