Theorem anim1d 613

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 611	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 210  df-an 400

This theorem is referenced by:  pm3.45  624  exdistrf  2458  2ax6elem  2482  mopick2  2699  ssrexf  3979  ssrexv  3982  ssdif  4067  ssrin  4160  reupick  4239  disjss1  5001  copsexgw  5346  copsexg  5347  propeqop  5362  po3nr  5452  frss  5486  coss2  5691  ordsssuc2  6247  fununi  6399  dffv2  6733  oprabidw  7166  extmptsuppeq  7837  onfununi  7961  oaass  8170  ssnnfi  8721  fiint  8779  fiss  8872  wemapsolem  8998  tcss  9170  ac6s  9895  reclem2pr  10459  qbtwnxr  12581  ico0  12772  icoshft  12851  2ffzeq  13023  clsslem  14335  r19.2uz  14703  isprm7  16042  infpn2  16239  prmgaplem4  16380  fthres2  17194  ablfacrplem  19180  monmat2matmon  21429  neiss  21714  uptx  22230  txcn  22231  nrmr0reg  22354  cnpflfi  22604  cnextcn  22672  caussi  23901  ovolsslem  24088  tgtrisegint  26293  inagswap  26635  shorth  29078  mptssALT  30438  uzssico  30533  zarclsint  31225  ordtconnlem1  31277  omsmon  31666  omssubadd  31668  subgrtrl  32493  subgrcycl  32495  acycgrsubgr  32518  mclsax  32929  poseq  33208  trisegint  33602  segcon2  33679  opnrebl2  33782  bj-19.42t  34217  poimirlem30  35087  itg2addnclem  35108  itg2addnclem2  35109  fdc1  35184  totbndss  35215  ablo4pnp  35318  keridl  35470  dib2dim  38539  dih2dimbALTN  38541  dvh1dim  38738  mapdpglem2  38969  pell14qrss1234  39797  pell1qrss14  39809  rmxycomplete  39858  lnr2i  40060  rp-fakeanorass  40221  rfcnnnub  41665  or2expropbi  43626  2ffzoeq  43885  ich2exprop  43988  nnsum4primes4  44307  nnsum4primesprm  44309  nnsum4primesgbe  44311  nnsum4primesle9  44313