Theorem anim1d 587

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

Syntax hints:   → wi 4   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  pm3.45  878  exdistrf  2332  2ax6elem  2448  mopick2  2539  ssrexf  3644  ssrexv  3646  ssdif  3723  ssrin  3816  reupick  3887  disjss1  4589  copsexg  4916  propeqop  4930  po3nr  5009  frss  5041  coss2  5238  ordsssuc2  5773  fununi  5922  dffv2  6228  extmptsuppeq  7264  onfununi  7383  oaass  7586  ssnnfi  8123  fiint  8181  fiss  8274  wemapsolem  8399  tcss  8564  ac6s  9250  reclem2pr  9814  qbtwnxr  11974  ico0  12163  icoshft  12236  2ffzeq  12401  clsslem  13657  r19.2uz  14025  isprm7  15344  infpn2  15541  prmgaplem4  15682  fthres2  16513  ablfacrplem  18385  monmat2matmon  20548  neiss  20823  uptx  21338  txcn  21339  nrmr0reg  21462  cnpflfi  21713  cnextcn  21781  caussi  23003  ovolsslem  23159  tgtrisegint  25294  inagswap  25630  clwwlknp  26754  shorth  28003  mptssALT  29317  ordtconnlem1  29752  omsmon  30141  omssubadd  30143  mclsax  31174  poseq  31451  nodenselem5  31548  trisegint  31777  segcon2  31854  opnrebl2  31958  poimirlem30  33071  itg2addnclem  33093  itg2addnclem2  33094  fdc1  33174  totbndss  33208  ablo4pnp  33311  keridl  33463  dib2dim  36012  dih2dimbALTN  36014  dvh1dim  36211  mapdpglem2  36442  pell14qrss1234  36900  pell1qrss14  36912  rmxycomplete  36962  lnr2i  37167  rp-fakeanorass  37339  rfcnnnub  38678  2ffzoeq  40635  nnsum4primes4  40966  nnsum4primesprm  40968  nnsum4primesgbe  40970  nnsum4primesle9  40972