Theorem anim1d 606

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

Syntax hints:   → wi 4   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  pm3.45  617  exdistrf  2468  2ax6elem  2583  mopick2  2720  ssrexf  3890  ssrexv  3892  ssdif  3972  ssrin  4062  reupick  4140  disjss1  4847  copsexg  5176  propeqop  5193  po3nr  5277  frss  5309  coss2  5511  ordsssuc2  6051  fununi  6197  dffv2  6518  extmptsuppeq  7583  onfununi  7704  oaass  7908  ssnnfi  8448  fiint  8506  fiss  8599  wemapsolem  8724  tcss  8897  ac6s  9621  reclem2pr  10185  qbtwnxr  12319  ico0  12509  icoshft  12585  2ffzeq  12755  clsslem  14102  r19.2uz  14468  isprm7  15791  infpn2  15988  prmgaplem4  16129  fthres2  16944  ablfacrplem  18818  monmat2matmon  20999  neiss  21284  uptx  21799  txcn  21800  nrmr0reg  21923  cnpflfi  22173  cnextcn  22241  caussi  23465  ovolsslem  23650  tgtrisegint  25811  inagswap  26148  shorth  28709  mptssALT  30022  uzssico  30093  ordtconnlem1  30515  omsmon  30905  omssubadd  30907  mclsax  32012  poseq  32292  trisegint  32674  segcon2  32751  opnrebl2  32854  poimirlem30  33983  itg2addnclem  34004  itg2addnclem2  34005  fdc1  34084  totbndss  34118  ablo4pnp  34221  keridl  34373  dib2dim  37318  dih2dimbALTN  37320  dvh1dim  37517  mapdpglem2  37748  pell14qrss1234  38264  pell1qrss14  38276  rmxycomplete  38325  lnr2i  38529  rp-fakeanorass  38700  rfcnnnub  40013  2ffzoeq  42226  nnsum4primes4  42507  nnsum4primesprm  42509  nnsum4primesgbe  42511  nnsum4primesle9  42513