Theorem anim1d 623

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  pm3.45  634  exdistrf  2476  2ax6elem  2499  mopick2  2662  ssrexf  3975  rabss2  4002  ssdif  4080  ssrin  4138  reupick  4274  disjss1  5075  copsexgwOLD  5460  copsexg  5461  propeqop  5478  po3nr  5573  frss  5614  coss2  5833  ordsssuc2  6456  fununi  6615  dffv2  6980  oprabidw  7451  poseq  8177  extmptsuppeq  8208  onfununi  8352  oaass  8572  ssnnfi  9188  fiint  9321  fiss  9419  wemapsolem  9547  elirrvOLD  9595  tcss  9746  r1filimi  9906  ac6s  10565  reclem2pr  11136  qbtwnxr  13333  ico0  13525  icoshft  13607  2ffzeq  13786  clsslem  15142  r19.2uz  15524  isprm7  16889  prmdvdsncoprmbd  16908  infpn2  17096  prmgaplem4  17237  fthres2  18114  chndss  18795  ablfacrplem  20286  rnglidlmmgm  21538  psdmul  22492  monmat2matmon  23147  neiss  23432  uptx  23949  txcn  23950  nrmr0reg  24073  cnpflfi  24323  cnextcn  24391  caussi  25623  ovolsslem  25810  fltoprmlem1  27998  tgtrisegint  28967  inagswap  29365  subgrtrl  30299  subgrcycl  30390  shorth  31902  ac6mapd  33264  mptssALT  33315  uzssico  33422  zarclsint  34550  ordtconnlem1  34602  omsmon  34976  omssubadd  34978  acycgrsubgr  35999  mclsax  36420  trisegint  36885  segcon2  36962  opnrebl2  37201  bj-19.42t  37759  bj-axreprepsep  38083  wl-dfcleq  38530  poimirlem30  38661  itg2addnclem  38682  itg2addnclem2  38683  fdc1  38773  totbndss  38804  ablo4pnp  38907  keridl  39059  dib2dim  42393  dih2dimbALTN  42395  dvh1dim  42592  mapdpglem2  42823  pell14qrss1234  43956  pell1qrss14  43968  rmxycomplete  44017  lnr2i  44211  fzunt  44549  fzuntd  44550  fzunt1d  44551  fzuntgd  44552  rp-fakeanorass  44607  rfcnnnub  46146  or2expropbi  48197  2ffzoeq  48491  ich2exprop  48646  nnsum4primes4  48980  nnsum4primesprm  48982  nnsum4primesgbe  48984  nnsum4primesle9  48986  opnneir  50114