Theorem anim1d 589

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

Syntax hints:   → wi 4   ∧ wa 383

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 385

This theorem is referenced by:  pm3.45  915  exdistrf  2473  2ax6elem  2586  mopick2  2678  ssrexf  3806  ssrexv  3808  ssdif  3888  ssrin  3981  reupick  4054  disjss1  4778  copsexg  5104  propeqop  5118  po3nr  5201  frss  5233  coss2  5434  ordsssuc2  5975  fununi  6125  dffv2  6433  extmptsuppeq  7487  onfununi  7607  oaass  7810  ssnnfi  8344  fiint  8402  fiss  8495  wemapsolem  8620  tcss  8793  ac6s  9498  reclem2pr  10062  qbtwnxr  12224  ico0  12414  icoshft  12487  2ffzeq  12654  clsslem  13924  r19.2uz  14290  isprm7  15622  infpn2  15819  prmgaplem4  15960  fthres2  16793  ablfacrplem  18664  monmat2matmon  20831  neiss  21115  uptx  21630  txcn  21631  nrmr0reg  21754  cnpflfi  22004  cnextcn  22072  caussi  23295  ovolsslem  23452  tgtrisegint  25593  inagswap  25929  shorth  28463  mptssALT  29783  uzssico  29855  ordtconnlem1  30279  omsmon  30669  omssubadd  30671  mclsax  31773  poseq  32059  trisegint  32441  segcon2  32518  opnrebl2  32622  poimirlem30  33752  itg2addnclem  33774  itg2addnclem2  33775  fdc1  33855  totbndss  33889  ablo4pnp  33992  keridl  34144  dib2dim  37034  dih2dimbALTN  37036  dvh1dim  37233  mapdpglem2  37464  pell14qrss1234  37922  pell1qrss14  37934  rmxycomplete  37984  lnr2i  38188  rp-fakeanorass  38360  rfcnnnub  39694  2ffzoeq  41848  nnsum4primes4  42187  nnsum4primesprm  42189  nnsum4primesgbe  42191  nnsum4primesle9  42193