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  2482  2ax6elem  2505  mopick2  2668  ssrexf  4007  rabss2  4034  ssdif  4101  ssrin  4197  reupick  4285  disjss1  5087  copsexgwOLD  5478  copsexg  5479  propeqop  5495  po3nr  5589  frss  5630  coss2  5847  ordsssuc2  6461  fununi  6618  dffv2  6983  oprabidw  7454  poseq  8163  extmptsuppeq  8193  onfununi  8337  oaass  8555  ssnnfi  9164  fiint  9296  fiss  9394  wemapsolem  9522  elirrvOLD  9570  tcss  9721  ac6s  10486  reclem2pr  11051  qbtwnxr  13244  ico0  13436  icoshft  13518  2ffzeq  13696  clsslem  15047  r19.2uz  15429  isprm7  16792  prmdvdsncoprmbd  16811  infpn2  16998  prmgaplem4  17139  fthres2  18016  chndss  18697  ablfacrplem  20168  rnglidlmmgm  21416  psdmul  22366  monmat2matmon  23018  neiss  23303  uptx  23819  txcn  23820  nrmr0reg  23943  cnpflfi  24193  cnextcn  24261  caussi  25493  ovolsslem  25680  tgtrisegint  28805  inagswap  29195  shorth  31684  ac6mapd  33005  mptssALT  33056  uzssico  33166  zarclsint  34293  ordtconnlem1  34345  omsmon  34720  omssubadd  34722  r1filimi  35522  subgrtrl  35646  subgrcycl  35648  acycgrsubgr  35671  mclsax  36082  trisegint  36541  segcon2  36618  opnrebl2  36873  bj-19.42t  37431  bj-axreprepsep  37753  wl-dfcleq  38201  poimirlem30  38342  itg2addnclem  38363  itg2addnclem2  38364  fdc1  38438  totbndss  38469  ablo4pnp  38572  keridl  38724  dib2dim  42058  dih2dimbALTN  42060  dvh1dim  42257  mapdpglem2  42488  pell14qrss1234  43624  pell1qrss14  43636  rmxycomplete  43685  lnr2i  43884  fzunt  44222  fzuntd  44223  fzunt1d  44224  fzuntgd  44225  rp-fakeanorass  44280  rfcnnnub  45797  or2expropbi  47812  2ffzoeq  48106  ich2exprop  48261  nnsum4primes4  48595  nnsum4primesprm  48597  nnsum4primesgbe  48599  nnsum4primesle9  48601  opnneir  49726