Theorem anim1d 617

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  pm3.45  628  exdistrf  2455  2ax6elem  2478  mopick2  2641  ssrexf  3988  rabss2  4015  ssdif  4081  ssrin  4177  reupick  4264  disjss1  5052  copsexgwOLD  5438  copsexg  5439  propeqop  5455  po3nr  5548  frss  5589  coss2  5805  ordsssuc2  6410  fununi  6567  dffv2  6929  oprabidw  7394  poseq  8105  extmptsuppeq  8135  onfununi  8278  oaass  8493  ssnnfi  9101  fiint  9234  fiss  9334  wemapsolem  9462  elirrvOLD  9510  tcss  9661  ac6s  10404  reclem2pr  10969  qbtwnxr  13150  ico0  13342  icoshft  13424  2ffzeq  13601  clsslem  14944  r19.2uz  15312  isprm7  16676  prmdvdsncoprmbd  16695  infpn2  16882  prmgaplem4  17023  fthres2  17899  chndss  18580  ablfacrplem  20040  rnglidlmmgm  21245  psdmul  22161  monmat2matmon  22814  neiss  23099  uptx  23615  txcn  23616  nrmr0reg  23739  cnpflfi  23989  cnextcn  24057  caussi  25289  ovolsslem  25476  tgtrisegint  28592  inagswap  28934  shorth  31391  ac6mapd  32722  mptssALT  32773  uzssico  32883  zarclsint  34063  ordtconnlem1  34115  omsmon  34489  omssubadd  34491  r1filimi  35291  subgrtrl  35368  subgrcycl  35370  acycgrsubgr  35393  mclsax  35804  trisegint  36263  segcon2  36340  opnrebl2  36556  bj-19.42t  37115  bj-axreprepsep  37435  wl-dfcleq  37883  poimirlem30  38024  itg2addnclem  38045  itg2addnclem2  38046  fdc1  38120  totbndss  38151  ablo4pnp  38254  keridl  38406  dib2dim  41742  dih2dimbALTN  41744  dvh1dim  41941  mapdpglem2  42172  pell14qrss1234  43308  pell1qrss14  43320  rmxycomplete  43369  lnr2i  43568  fzunt  43906  fzuntd  43907  fzunt1d  43908  fzuntgd  43909  rp-fakeanorass  43964  rfcnnnub  45491  or2expropbi  47504  2ffzoeq  47798  ich2exprop  47953  nnsum4primes4  48287  nnsum4primesprm  48289  nnsum4primesgbe  48291  nnsum4primesle9  48293  opnneir  49404