Theorem anim1d 622

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 25	. 2 ⊢ (𝜑 → (𝜃 → 𝜃))
3	1, 2	anim12d 620	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ∧ wa 400

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 401

This theorem is referenced by:  pm3.45  633  exdistrf  2479  2ax6elem  2502  mopick2  2665  ssrexf  4005  rabss2  4032  ssdif  4099  ssrin  4195  reupick  4283  disjss1  5083  copsexgwOLD  5475  copsexg  5476  propeqop  5492  po3nr  5586  frss  5627  coss2  5844  ordsssuc2  6456  fununi  6613  dffv2  6978  oprabidw  7443  poseq  8155  extmptsuppeq  8185  onfununi  8329  oaass  8547  ssnnfi  9155  fiint  9287  fiss  9385  wemapsolem  9513  elirrvOLD  9561  tcss  9712  ac6s  10469  reclem2pr  11034  qbtwnxr  13227  ico0  13419  icoshft  13501  2ffzeq  13679  clsslem  15023  r19.2uz  15405  isprm7  16768  prmdvdsncoprmbd  16787  infpn2  16974  prmgaplem4  17115  fthres2  17992  chndss  18673  ablfacrplem  20138  rnglidlmmgm  21360  psdmul  22310  monmat2matmon  22962  neiss  23247  uptx  23763  txcn  23764  nrmr0reg  23887  cnpflfi  24137  cnextcn  24205  caussi  25437  ovolsslem  25624  tgtrisegint  28749  inagswap  29139  shorth  31628  ac6mapd  32949  mptssALT  33000  uzssico  33110  zarclsint  34243  ordtconnlem1  34295  omsmon  34669  omssubadd  34671  r1filimi  35478  subgrtrl  35606  subgrcycl  35608  acycgrsubgr  35631  mclsax  36042  trisegint  36501  segcon2  36578  opnrebl2  36813  bj-19.42t  37371  bj-axreprepsep  37693  wl-dfcleq  38141  poimirlem30  38282  itg2addnclem  38303  itg2addnclem2  38304  fdc1  38378  totbndss  38409  ablo4pnp  38512  keridl  38664  dib2dim  41998  dih2dimbALTN  42000  dvh1dim  42197  mapdpglem2  42428  pell14qrss1234  43566  pell1qrss14  43578  rmxycomplete  43627  lnr2i  43826  fzunt  44164  fzuntd  44165  fzunt1d  44166  fzuntgd  44167  rp-fakeanorass  44222  rfcnnnub  45739  or2expropbi  47754  2ffzoeq  48048  ich2exprop  48203  nnsum4primes4  48537  nnsum4primesprm  48539  nnsum4primesgbe  48541  nnsum4primesle9  48543  opnneir  49668